Waldmeister is a theorem prover for unit equational logic. Its proof procedure is unfailing Knuth-Bendix completion [BDP89]. Waldmeister’s main advantage is that efficiency has been reached in terms of time as well as of space. Within that scope, a complete proof object is constructed at run-time. Read more about the implementation.

References in zbMATH (referenced in 46 articles , 3 standard articles )

Showing results 21 to 40 of 46.
Sorted by year (citations)
  1. Baader, Franz; Beckert, Bernhard; Nipkow, Tobias: Deduktion: von der Theorie zur Anwendung (2010) ioport
  2. Bensaid, Hicham; Caferra, Ricardo; Peltier, Nicolas: Perfect discrimination graphs: indexing terms with integer exponents (2010)
  3. ten Cate, Balder; Litak, Tadeusz; Marx, Maarten: Complete axiomatizations for XPath fragments (2010)
  4. Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Optimizing (\textmkb_\textTT) (2010)
  5. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
  6. Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
  7. 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)
  8. Löchner, Bernd: Things to know when implementing KBO (2006)
  9. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with (\Omega)MEGA (2006)
  10. Stump, Aaron; Löchner, Bernd: Knuth-Bendix completion of theories of commuting group endomorphisms (2006)
  11. Veroff, R.; Spinks, M.: Axiomatizing the skew Boolean propositional calculus (2006)
  12. Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
  13. Miller, Swaha; Plaisted, David A.: The space efficiency of OSHL (2005)
  14. Riazanov, Alexandre; Voronkov, Andrei: Efficient instance retrieval with standard and relational path indexing (2005)
  15. Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
  16. Avenhaus, J.; Hillenbrand, Th.; Löchner, B.: On using ground joinable equations in equational theorem proving (2003)
  17. Dahn, Ingo (ed.); Vigneron, Laurent (ed.): FTP’2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP’03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12--14, 2003 (2003)
  18. Gaillourdet, Jean-Marie; Hillenbrand, Thomas; Löchner, Bernd; Spies, Hendrik: The new WALDMEISTER loop at work. (2003) ioport
  19. Hillenbrand, Thomas: Citius altius fortius: lessons learned from the theorem prover Waldmeister (2003)
  20. Kutsia, Temur: Equational prover of THEOREMA (2003)

Further publications can be found at: http://www.waldmeister.org/references.htm