From SAT-Modulo-Theory to Hereditary-Harrop-Modulo-Theory

Supervision : Germain Faure(1) + Stéphane Lengrand(2)
(1) LIX, Ecole Polytechnique Germain.Faure@LIX.Polytechnique.fr
(2) LIX, Ecole Polytechnique Lengrand@LIX.Polytechnique.fr
Keywords: SAT-problems, Proof-search, Logic Programming, Domain-specific theories and tools.

Background

The Satisfiability Modulo Theories (SMT) architecture, has recently proved to be a smart extension of SAT-solving techniques, and opened a prolific area of research. It combines propositional resolution methods with decision procedures specific to some theories like linear arithmetics. More precisely, it connects a SAT solver (handling the purely logical structure of a formula to be solved) to a decision procedure which checks the consistency of the models proposed by the SAT solver.

In the SMT architecture, a central process organises the dialogue between the two components: namely it feeds the SAT solver with the purely logical structure of the problem, ignoring what atomic formulae are, then retrieves (if it exists) a proposed satisfiability model and checks with the domain-specific tools the consistency of the model with respect to the theory. In case the domain-specific tool refutes the proposed model, some feedback is recorded as new knowledge (learning a lemma) and is re-injected into a new (and refined) call to the SAT solver, so that the previously proposed model cannot be generated again. These learning techniques are at the heart of SMT solvers by significantly reducing the search space.

But efficient proof search is not the attribute of bare propositional logic handled by SAT solvers: For instance the ProLog programming language performs automated proof-search techniques on Horn clauses, and extending proof search to even more expressive logics is still an open and active line of research. However, this line has not yet been concerned with the interaction with domain-specific methods. Nonetheless, improving the efficiency of proof-search mechanisms by plugging-in methods specific to a particular class of problems is greatly desirable.

Objectives

In this internship we propose to mimic the successful interaction that takes place in the SMT paradigm [2], in a slightly different logical setting whose mechanism is closer to a proof-search paradigm than SAT resolution is. For such a setting, we propose the traditional (goal-directed and backchaining) proof-search mechanism on Hereditary Harrop Formulae (HHF) [1], which is an enhanced computational paradigm of Logic Programming, as featured in the lambda-ProLog language.

This choice is motivated firstly by the fact that such a proof-search mechanism can be seen as a form of resolution mechanism, on which SAT solvers are based. We thus have confidence in the possibility of adapting the SMT approach to this new setting (although strictly speaking, it is not clear to what extent knowing the internal mechanisms of the SAT solver is required to organise the SMT-dialogue).

It is secondly motivated by the fact that, in contrast to SAT, this setting already features a notion of proof (maybe even proof object), which is one of the main components of the rest of our project. This raises the question of what the output of our logical mechanism is that can be passed onto the domain-specific tool, and how the notion of proof appears in this output. This might be slightly more sophisticated than in the case of a SAT solver.

Also, the nature of the feedback given by the domain-specific tool regarding proofs or proof objects is also raised. Indeed if in the end we have a positive answer resulting from the interaction, the question remains of whether and how we get a notion of (proof-related) certificate for that answer.

In summary, the object of this task is
-to understand, in light of SMT, the interface that could be used for the interaction between proof-search on HHF and a domain-specific tool,
-to what extent the interaction constrains us in organising such proof-search,
-how the notion of proof is communicated within the dialogue and as the result of it.

When such questions are satisfyingly answered, a prototype implementing these ideas could be considered.

Practical questions

Supervision of this internship will be at the LIX laboratory, Ecole Polytechnique, by Germain Faure and Stéphane Lengrand. For this internship please contact Germain Faure or Stéphane Lengrand; addresses are above.

A light version of this internship is available for L3 or M1 students. It will concentrate on HHF with a simple and specific language for atomic propositions, and on implementing a small tool in which HHF proof-search mechanisms will interact with a specific tool for this language.

References