Thursday 10 September 2015, 15:00, Ecole Polytechnique, amphi Cauchy: Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, PhD defense of Simon Cruanes.
Jury:
Abstract:
In this thesis, we aim at developing new extensions to Superposition, a proof technique for first-order logic with equality. Our claim is that Superposition lends itself very well to being grafted additional inference rules and reasoning mechanisms.
First, we develop a Superposition-based calculus for integer linear arithmetic. Linear Integer Arithmetic is a widely studied and used theory in other areas of automated deduction, in particular SMT (Satisfiability Modulo Theory). This theory might also prove useful for problems that have a discrete, totally ordered structure, such as temporal logic, and that might be encoded efficiently into first-order logic with arithmetic.
Then, we define an extension of Superposition that is able to reason by structural induction (natural numbers, lists, binary trees, etc.) Inductive reasoning is pervasive in Mathematics and Computer Science but its integration into general purpose first-order provers has not been studied much.
Last, we present a theory detection system that, given a signature-agnostic description of algebraic theories, detects their presence in sets of formulas. This system is akin to the way a mathematician who studies a new object discovers that this object belong to some known structure, such as groups, allowing her to leverage the large body of knowledge on this specific theory.
A large implementation effort was also carried out in this thesis; all the contributions presented above have been implemented in a library and a theorem prover, Zipperposition, both written in OCaml and released under a free software license.