Efficient reasoning in equational theories

Abstract

Problems in many theories axiomatised by unit equalities (UEQ), such as groups, loops, lattices, and other algebraic structures, are notoriously difficult for automated theorem provers to solve. Consequently, there has been considerable effort over decades in developing techniques to handle these theories, notably in the context of Knuth-Bendix completion and derivatives. The superposition calculus is a generalisation of completion to full first-order logic; however it does not carry over all the refinements that were developed for it, and is therefore not a strict generalisation. This means that (i) as of today, even state of the art superposition provers, while more general, are outperformed in UEQ by provers based on completion, and (ii) the sophisticated techniques developed for completion are not available in any problem which is not in UEQ. In particular, this includes key simplifications such as ground joinability, which have been known for more than 30 years; however previous completeness proofs rely on proof orderings and proof reductions, which are not easily extensible to general clauses together with redundancy elimination. In this work we introduce a novel notion of redundancy of clauses and inferences, and a proof of refutational completeness of the superposition calculus wrt this notion of redundancy. Then, we use it to derive a plethora of simplification rules and redundancy criteria, including an extension of ground joinability, which elegantly generalises this simplification from equational completion (in UEQ) to superposition (over arbitrary clauses); and an extension of the connectedness critical pair criterion to superposition. We also study the theory of associative-commutative operators in particular, including deriving a stronger notion of normalisation modulo this theory, and showing where demodulation modulo AC can be applied while preserving refutational completeness. Implementing these techniques efficiently is itself a non-trivial task, therefore we have proposed novel algorithms for tackling two key issues: the test for ground joinability of two terms, and the scheduling of simplifications in a given-clause loop. We have implemented most of the techniques described herein in a theorem prover, iProver, including the aforementioned novel algorithms, and evaluated over the TPTP library with encouraging results.

Date of Award	31 Dec 2023
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Konstantin Korovin (Supervisor) & Renate Schmidt (Supervisor)