Skip to Main content Skip to Navigation

Automated Reasoning Techniques as Proof-search in Sequent Calculus

Mahfuza Farooque 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Computer-aided reasoning plays a great role in computer science and mathematical logic, from logic programing to automated reasoning, via interactive proof assistants, etc. The general aim of this thesis is to design a general framework where various techniques of Computer-aided reasoning can be implemented, so that they can collaborate, be generalised, and implemented in a safe and trusted way. The framework I propose is a sequent calculus called LKp(T), which generalises an older calculus of the literature to the presence of an arbitrary background theory for which we have a decision procedure, like linear arithmetic. The thesis develops the meta-theory of LKp(T), such as its logical completeness. We then show how it specifies a proof-search procedure that can emulate a well-known technique from the field of Satisfiability-modulo-Theories, namely DPLL(T). Finally, clause and connection tableaux are other widely used techniques of automated reasoning, of a rather different nature from that of DPLL. This thesis also described how such tableaux techniques can be described as bottom-up proof-search in LKp(T). The simulation is given for both propositional and first-order logic, opening up new perspectives of generalisation and collaboration between tableaux techniques and DPLL, even in presence of a background theory.
Document type :
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download
Contributor : Stéphane Graham-Lengrand <>
Submitted on : Wednesday, March 19, 2014 - 8:23:17 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Thursday, June 19, 2014 - 1:18:10 PM


  • HAL Id : pastel-00961344, version 1



Mahfuza Farooque. Automated Reasoning Techniques as Proof-search in Sequent Calculus. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. ⟨pastel-00961344⟩



Record views


Files downloads