Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity

TLDR

Theories with simplifiers, commutativity, and associativity are common in key domains such as number theory and set theory. The paper proposes an approach to embed these concepts into resolution-based theorem provers to achieve faster, more efficient, and refutation-complete inference. The method introduces new inference rules and a natural notation to encode simplifiers, commutativity, and associativity, including axioms for identities, inverses, and zero multiplication. The authors demonstrate that commutativity can be added via a simple unification modification, while simplifiers and associativity require more complex extensions that can be combined for C‑linear refutation completeness or other ordered theories, and discuss their use in practical theorem‑proving software.

Abstract

To prove really difficult theorems, resolution principle programs need to make better inferences and to make them faster. An approach is presented for taking advantage of the structure of some special theories. These are theories with simplifiers, commutativity, and associativity, which are valuable concepts to build in, since they so frequently occur in important theories, for example, number theory (plus and times) and set theory (union and intersection). The object of the approach is to build in such concepts in a (refutation) complete, valid, efficient (in time) manner by means of a “natural” notation and/or new inference rules. Some of the many simplifiers that can be built in are axioms for (left and right) identities, inverses, and multiplication by zero. As for results, commutativity is built in by a straightforward modification to the unification (matching) algorithm. The results for simplifiers and associativity are more complicated. These theoretical results can be combined with one another and/or extended to either C -linear refutation completeness or theories with partial ordering, total ordering, or sets. How these results can serve as the basis of practical computer programs is discussed.