Automated reasoning techniques as proof-search in sequent calculus

Mahfuza Farooque (1, 2)

1 PARSIFAL - Proof search and reasoning with logic specifications
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

This thesis designs a theoretical and general framework where proof-search can modularly interact with domain-specific procedure(s). This framework is a focussed sequent calculus for polarised classical logic, with quantifiers, and it is designed in the view of capturing various computer-aided reasoning techniques that exist in logic programing, goal-directed systems, proof-assistants, and automated provers. This thesis starts with a survey of focused sequent calculi for polarised classical logic, as a journey from Gentzen's original sequent calculus to Liang-Miller's LKF. It then introduces a new system LKp(T) which extends, with on-the-fly polarisation and calls to decision procedures, Liang-Miller's LKF. Key results of the meta-theory of the system are proved: the cut-elimination property, the property that changing the polarity of connectives does not change the provability of formulae, and finally, the logical completeness of LKp(T). While Gentzen's original rules offer a lot of non-determinism in proof-search, focusing provides a tight control on the breadth of the search space. Together with on-the-fly polarisation of literals, this equips the sequent calculus LKp(T) with features that are particularly appropriate for computer-aided reasoning: For instance, a widely-used technique for solving propositional satisfiability (SAT) problems (whether or not a formula over Boolean variables can be made true by choosing truth values for its variables) is the DPLL procedure. Satisfiability-modulo-Theories (SMT) problems generalise SAT problems by the presence of a background theory for which a decision procedure is known, and can be solved by correspondingly generalising DPLL into DPLL(T), which most SMT-solvers implement. This thesis investigates how each of the steps of DPLL(T) can be emulated as the standard steps of proof-search in LKp(T): the gradual and goal-directed construction of a proof-tree. This allows the DPLL(T) algorithm to be applied up-to-a-point, where a switch to another technique can be made (depending on the newly generated goals). This differs from previous work where an SMT-technique is called until it finishes. The proof-search control that is provided by focusing and on-the-fly polarisation allows us to derive a stronger result than the mere simulation of DPLL(T): the proofs in LKp(T) that are the images of those DPLL(T) runs concluding that a formula is unsatisfiable, can be characterised by a simple criterion only involving the way formulae are placed into the focus of sequents (the device implementing focusing). From this criterion we directly get a simple proof-search strategy that is bi-similar to DPLL(T) runs: that which performs the depth-first completion of incomplete proof-trees (starting with the leftmost open leaf), using any inference steps satisfying the given criterion on polarities and focusing. That way, we ensure that bottom-up proof-search in LKp(T) can be as efficient as the DPLL(T) procedure. 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.

Mots clés: automated reasoning; proof-search; sequent calculus

Domaines: Logique en informatique [cs.LO]

Mahfuza Farooque. Automated reasoning techniques as proof-search in sequent calculus. 2013. ⟨hal-00939124⟩