Linking Focusing and Automated Theorem Proving
Axe & tâche scientifique DigiCosme : SciLex
Coordinateurs :Guillaume Burel, SAMOVAR – Kaustuv Chaudhuri, LIX – Dale Miller, LIX
Nom & Prénom du Candidat : en cours de recrutement
Adresse mail :
Laboratoire gestionnaire: SAMOVAR
Adossé à l’action DigiCosme :GT UPSCaLe
Durée & Dates de la mission : 1 an – mars 2017
Contexte : One of the elements that explain the huge improvement of automated theorem provers in the recent years relies on the use of proof search methods in which the proof search space is very restricted. However, such restrictions should not compromise completeness of the proof search method: given a valid formula, the method should eventually find a proof. These restrictions therefore generally relies on fundamental results. Among techniques used for restricting the proof search space, one can cite, on one hand, ordering and selection in methods based on Robinson’s resolution; and, on the other hand, focusing in sequent calculi, which lead to tableaux and inverse methods. Ordering and selection techniques are mainly used in for first-order classical logic, in automated theorem provers implementing a resolution-like calculus. Focused search strategies, on the other hand, are used in automated theorem provers for linear, intuitionistic, or modal logics. Although these techniques seem unrelated, recent works build bridges between them.
Focusing is also used at the heart of the ProofCert project, which aims at providing a universal framework for checking and combining proofs. In particular, ProofCert should be able to gracefully import proofs found by automated theorem provers using selection techniques.
Objectif :
The overall objective of this postdoc proposal is the study of the fruitful links between focusing and automated theorem proving. More precisely, the postdoc fellow should study the following directions:
- High impact strategies such as ordering and selection are designed for classical resolution, and are missing in non-classical forward search strategies such as the inverse method. Since focusing is easily adapted to such non-classical logics and since it has provided an explanation for these classical strategies, it may be possible to transfer the benefits of ordering and selection to non-classical logics via focusing.
- The meta-theory of focusing is notoriously complex and is an ideal candidate for rigorous formalization in formal reasoning systems such as Coq or Abella. However, it is a challenge to build a good reusable framework for formalizing focusing in a variety of logics. One promising direction is to use synthetic techniques.
- Focusing with selection is not complete in general. Indeed, it depends on how literals are selected in formulas. Most of the completeness results, either on the resolution side or on the sequent calculus side, are built upon model constructions. It should therefore be studied how these proofs can be ported to the framework of focusing with selection, and how they are related. These may lead to new proof of completeness in other logics, therefore feeding Objective 1.