Waldmeister

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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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

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

1 2 3 next

  1. Goertzel, Zarathustra A.; Chvalovský, Karel; Jakubův, Jan; Olšák, Miroslav; Urban, Josef: Fast and slow enigmas and parental guidance (2021)
  2. Sutcliffe, Geoff; Desharnais, Martin: The CADE-28 automated theorem proving system competition -- CASC-28 (2021)
  3. Araújo, João; Kinyon, Michael; Robert, Yves: Varieties of regular semigroups with uniquely defined inversion (2019)
  4. Kinyon, Michael: Proof simplification and automated theorem proving (2019)
  5. Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)
  6. McCabe-Dansted, John C.; Reynolds, Mark: Rewrite rules for (\mathrmCTL^\ast) (2017)
  7. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  8. Höfner, Peter; Möller, Bernhard: Extended feature algebra (2016)
  9. Santocanale, Luigi: Relational lattices via duality (2016)
  10. Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
  11. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  12. Burel, Guillaume; Cruanes, Simon: Detection of first order axiomatic theories (2013)
  13. Foster, Simon; Woodcock, Jim: Unifying theories of programming in Isabelle (2013)
  14. Schulz, Stephan: Simple and efficient clause subsumption with feature vector indexing (2013)
  15. Armstrong, Alasdair; Foster, Simon; Struth, Georg: Dependently typed programming based on automated theorem proving (2012)
  16. Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \textitdescenteinfinie -- a manifesto (2012)
  17. Zenil, Hector: Computer runtimes and the length of proofs. With an algorithmic probabilistic application to waiting times in automatic theorem proving (2012)
  18. Dang, H.-H.; Höfner, P.; Möller, B.: Algebraic separation logic (2011)
  19. Desharnais, Jules; Struth, Georg: Internal axioms for domain semirings (2011)
  20. Kovács, Laura; Moser, Georg; Voronkov, Andrei: On transfinite Knuth-Bendix orders (2011)

1 2 3 next


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