Skip to main content
Top

2018 | OriginalPaper | Chapter

MædMax: A Maximal Ordered Completion Tool

Authors : Sarah Winkler, Georg Moser

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
3
The Maxcomp version presented in [11] solves 91 KB examples within 60 s, too, but 98 problems in 600 s. For the other tools the numbers hardly change with a larger timeout. Maxcomp is not applicable to the other problem sets though.
 
Literature
3.
go back to reference Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Aït Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, Rewriting Techniques of Progress in Theoretical Computer Science, vol. 2, pp. 1–30. Academic Press, Cambridge (1989) Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Aït Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, Rewriting Techniques of Progress in Theoretical Computer Science, vol. 2, pp. 1–30. Academic Press, Cambridge (1989)
15.
go back to reference Sternagel, T.: Reliable confluence analysis of conditional term rewrite systems. Ph.D. thesis. University of Innsbruck (2017) Sternagel, T.: Reliable confluence analysis of conditional term rewrite systems. Ph.D. thesis. University of Innsbruck (2017)
18.
go back to reference Winkler, S.: A ground joinability criterion for ordered completion. In: Proceedings of 6th IWC, pp. 45–49 (2017) Winkler, S.: A ground joinability criterion for ordered completion. In: Proceedings of 6th IWC, pp. 45–49 (2017)
Metadata
Title
MædMax: A Maximal Ordered Completion Tool
Authors
Sarah Winkler
Georg Moser
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-319-94205-6_31

Premium Partner