MadMax
| swMATH ID: | 28631 |
| Software Authors: | Winkler, Sarah; Moser, Georg |
| Description: | Mædmax: a maximal ordered completion tool. The equational reasoning tool MædMax implements maximal ordered completion. This new approach extends the maxSMT-based method for standard completion developed by Klein and Hirokawa (2011) to ordered completion and equational theorem proving. MædMax incorporates powerful ground completeness checks and supports certification of its proofs by an Isabelle-based certifier. It also provides an order generation mode which can be used to synthesize term orderings for other tools. Experiments show the potential of our approach. |
| Homepage: | https://link.springer.com/chapter/10.1007/978-3-319-94205-6_31 |
| Related Software: | TPTP; Twee; VAMPIRE; E Theorem Prover; iProver; Waldmeister; Nagoya Termination Tool; GitHub; NaTT; Tyrolean; z3; ConCon; AGES; Prover9; Mace4; Isabelle/HOL; LCF; Jukebox; SPASS |
| Cited in: | 7 Documents |
Standard Articles
| 1 Publication describing the Software, including 1 Publication in zbMATH | Year |
|---|---|
|
MædMax: a maximal ordered completion tool. Zbl 1511.68333 Winkler, Sarah; Moser, Georg |
2018
|
all
top 5
Cited by 10 Authors
| 2 | Duarte, André |
| 2 | Korovin, Konstantin |
| 2 | Winkler, Sarah |
| 1 | Gutiérrez, Raúl |
| 1 | Hirokawa, Nao |
| 1 | Lucas, Salvador |
| 1 | Moser, Georg |
| 1 | Saito, Teppei |
| 1 | Smallbone, Nicholas |
| 1 | Sternagel, Christian |
Cited in 0 Serials
Cited in 2 Fields
| 7 | Computer science (68-XX) |
| 1 | Mathematical logic and foundations (03-XX) |
