Redundancy, Rewriting, and Induction

Abstract

This thesis addresses challenges and presents advancements in first-order theorem proving with equality in the framework of saturation-based theorem proving with the superposition calculus.To achieve efficiency in first-order reasoning, saturation-based theorem proving relies heavily on the concept of redundancy. The main aim of the thesis is to improve this concept and redundancy detection. This endeavor is complementedby rewriting techniques that are indispensable in equality reasoning. Beyond first-order logic, the thesis also aims to progress inductive reasoning, where both redundancy and rewriting are used to address several challenges. Our theoretical advancements are demonstrated in practice using the saturation-based theorem prover Vampire.The first two parts of the thesis improve the notion of redundancy in saturation-based theorem proving. In the first part, we introduce a generalization of standard redundancy in saturation, called partial redundancy. The second part exploits properties of term rewriting to reduce the search space of superposition reasoning with so-called reducibility constraints. We prove the refutational completeness of the superposition calculus with partial redundancy and reducibility constraints, respectively. We also show novel ways to detect redundancies in superposition reasoning. In the third part of the thesis, we utilize term rewriting to synthesize lemmasfor inductive reasoning in saturation. Despite weakening the restrictions of superposition reasoning, we maintain efficiency by applying ideas from redundancyin first-order reasoning to this domain. The fourth and last part of the thesis introduces a general indexing data structure, called term ordering diagram, to solve a challenge in redundancy detection related to simplification orders.