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 44 articles , 3 standard articles )

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

1 2 3 next

  1. Araújo, João; Kinyon, Michael; Robert, Yves: Varieties of regular semigroups with uniquely defined inversion (2019)
  2. Kinyon, Michael: Proof simplification and automated theorem proving (2019)
  3. Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)
  4. McCabe-Dansted, John C.; Reynolds, Mark: Rewrite rules for (\mathrmCTL^\ast) (2017)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  6. Höfner, Peter; Möller, Bernhard: Extended feature algebra (2016)
  7. Santocanale, Luigi: Relational lattices via duality (2016)
  8. Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
  9. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  10. Burel, Guillaume; Cruanes, Simon: Detection of first order axiomatic theories (2013)
  11. Foster, Simon; Woodcock, Jim: Unifying theories of programming in Isabelle (2013)
  12. Schulz, Stephan: Simple and efficient clause subsumption with feature vector indexing (2013)
  13. Armstrong, Alasdair; Foster, Simon; Struth, Georg: Dependently typed programming based on automated theorem proving (2012)
  14. Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \textitdescenteinfinie -- a manifesto (2012)
  15. Zenil, Hector: Computer runtimes and the length of proofs. With an algorithmic probabilistic application to waiting times in automatic theorem proving (2012)
  16. Dang, H.-H.; Höfner, P.; Möller, B.: Algebraic separation logic (2011)
  17. Desharnais, Jules; Struth, Georg: Internal axioms for domain semirings (2011)
  18. Kovács, Laura; Moser, Georg; Voronkov, Andrei: On transfinite Knuth-Bendix orders (2011)
  19. Baader, Franz; Beckert, Bernhard; Nipkow, Tobias: Deduktion: von der Theorie zur Anwendung (2010) ioport
  20. Bensaid, Hicham; Caferra, Ricardo; Peltier, Nicolas: Perfect discrimination graphs: indexing terms with integer exponents (2010)

1 2 3 next


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