Bliksem

Bliksem is a first-order, resolution based theorem prover, which is written in C. It has grown out of a series of benchmark tests that I carried out in december 1998. The benchmark tests compared various datastructures for representating terms, using the operations of unification and matching. The main outcome of these tests was that the most common datastructure (deep terms with arguments lists which are used in E, Spass and Otter) can sometimes be dramatically slower (app. 5 times) than flatterms. Flatterms are not harder to implement than deep terms with argument lists and use less memory. In that time, there existed only one prover using flatterms (Waldmeister), and this prover could handle only unit equality. Therefore it seemed a good idea to implement a full first-order prover using flatterms.


References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
  2. Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Combined reasoning by automated cooperation (2008)
  3. Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
  4. Buchberger, Bruno; Crǎciun, Adrian; Jebelean, Tudor; Kovács, Laura; Kutsia, Temur; Nakagawa, Koji; Piroi, Florina; Popov, Nikolaj; Robu, Judit; Rosenkranz, Markus; Windsteiger, Wolfgang: \textitTheorema: Towards computer-aided mathematical theory exploration (2006)
  5. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with (\Omega)MEGA (2006)
  6. Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
  7. Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
  8. Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
  9. de Nivelle, Hans; de Rijke, Maarten: Deciding the guarded fragments by resolution (2003)
  10. Riazanov, Alexandre; Voronkov, Andrei: Limited resource strategy in resolution theorem proving (2003)
  11. Bezem, Marc; Hendriks, Dimitri; de Nivelle, Hans: Automated proof construction in type theory using resolution (2002)
  12. Areces, Carlos; de Rijke, Maarten; de Nivelle, Hans: Resolution in modal, description and hybrid logic (2001)
  13. Bezem, Marc; Hendriks, Dimitri; de Nivelle, Hans: Automated proof construction in type theory using resolution (2000)
  14. de Nivelle, Hans; Schmidt, Renate A.; Hustadt, Ullrich: Resolution-based methods for modal logics (2000)
  15. Melis, E.; Siekmann, J.: Knowledge-based proof planning (1999)