2026-07-24T05:02:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10510 2024-03-06T10:46:06Z ddc:004 open_access

Extending Maximal Completion (Invited Talk) Winkler, Sarah automated reasoning completion theorem proving Maximal completion (Klein and Hirokawa 2011) is an elegantly simple yet powerful variant of Knuth-Bendix completion. This paper extends the approach to ordered completion and theorem proving as well as normalized completion. An implementation of the different procedures is described, and its practicality is demonstrated by various examples. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sarah Winkler 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.3 urn:nbn:de:0030-drops-105102 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.3 eng https://creativecommons.org/licenses/by/3.0/legalcode