Extensions de la Superposition pour l'Arithmétique Linéaire Entière, l'Induction Structurelle, et bien plus encore

The central concept of theorem designates a claimbacked by an irrefutable argument that follows formal rules, called a proof.Proving theorems is very useful in both Computer Science and Mathematics.However, many theorems are too boring and tedious for human experts(for instance, theorems generated to ensure that software abides bysome specification); hence the decades-long effort in automated theorem proving,the field dedicated to writing programs that find proofs.Superposition is a very competitive technique for proving theoremsin the language of first-order logic with equality over uninterpreted functions(in a nutshell, being able to replace equals by equals in any expression).Even then, Superposition falls short for many problems thatrequire theory-specific reasoning or inductive proofs.In this thesis, we aim at developing new extensions to Superposition.Our claim is that Superposition lends itself very well to being graftedadditional 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 ofautomated 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 encodedefficiently into first-order logic with arithmetic.Then, we define an extension of Superposition that is able to reasonby structural induction (natural numbers, lists, binary trees, etc.)Inductive reasoning is pervasive in Mathematics and Computer Science butits integration into general purpose first-order provers has not beenstudied much.Last, we present a theory detection system that, given a signature-agnosticdescription of algebraic theories, detects their presence in sets of formulas.This system is akin to the way a mathematician who studies a new objectdiscovers 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 libraryand a theorem prover, Zipperposition, both written in OCamland released under a free software license.