Abstract
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.
Cite
CITATION STYLE
Winkler, S., & Moser, G. (2018). MædMax: A Maximal Ordered Completion Tool. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 472–480). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
