Abstract

The equational reasoning tool MaedMax 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.

BibTeX

@inproceedings{SWGM-IJCAR18,
  author    = "Sarah Winkler and Georg Moser",
  title     = "MaedMax: A Maximal Ordered Completion Tool",
  booktitle = "Proceedings of the 9th International Joint Conference on Automated Reasoning",
  editor    = "Didier Galmiche, Stephan Schulz, and Roberto Sebastiani",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 10900,
  pages     = "472--480",
  year      = 2018,
  doi       = "10.1007/978-3-319-94205-6_31"
}