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