Proof-search control in interaction with domain-specific methods – PSI

Interactive proof assistants provide a very expressive logical formalism, rich enough to allow extremely precise descriptions of complex objects like the meta theory of a programming language [LCH07], a model of C compiler [Ler06], or the proof of the Four Color Theorem [Gon08]. This description includes logical statements of the properties required by the objects of interest but also their formal proofs, checked by the merciless proof-checker of the system, which should be a small hence trusted piece of code. These systems provide the highest formal guarantee, for instance, of the correctness of the specification of a code. Proof-search is a central issue in such a formalisation of mathematics. It is also a common aspect of automated reasoning and high-level programming paradigms such as Logic programming. In this process, proof-search is central and we want it to be as automated as possible. Indeed, proof-search is a common aspect of formal mathematics and automated reasoning, as well as high-level programming paradigms such as Logic programming. It is thus tempting to design a unique logical framework where a generic notion of proof-search could serve each of the above purposes. However specific applications commonly involve specific logics or theories, typically linear arithmetic. Whether or not such a logical framework can express these at all, it is unlikely that its generic proof-search mechanisms can replace the methods that are specific to a logic or theory. Either because this specific domain lies outwith the reach of generic proof-search or simply because generic proof-search is less efficient therein than a purpose-made procedure (typically a decision procedure). But to enlarge the scope where a specific method applies, one can combine both generic proof search mechanisms with specific methods. This is similar to Satisfiability Modulo Theories (SMT) [NOT06] and to the CLP(X) scheme [JM94] for Constraint Logic Programming: to have efficient solvers for dedicated theories within a general purpose engine. In the case of CLP(X), the general-purpose engine is a typical logic programming kernel while in the case of SMT it is a SAT solver. This smart extension of SAT solver opened a prolific area of research becoming quickly crucial in many verification applications [JHS05, LMC03, VB03]. In the SMT architecture, a central process organises the dialogue between the two components: 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 w.r.t. the theory. This idea thus requires some level of interaction between the two if only for the purpose of reducing a problem into the scope of a specific-method. Such a reduction can be simple and appear as a kind of pre-processing. But even in this case it is interesting to implement such a pre-processing and the call to the domain-specific method in a modular way. Or it can be more complex, and some substantial work (e.g. first-order logic) is actually done by generic proof-search mechanisms. In fact, if over the last fifteen years, new features (polarisation, focusing, etc) have emerged to enhance the proof-search mechanisms at the heart of logic programming, their design has so far been guided by the objective of completing a proof. But here we would like to be guided by the more general objective of reaching the scope where a domain-specific method can be applied. Our starting point is thus to look at both proof theory and logic programming computational paradigm to see how far we can go in extending the SMT architecture to more expressive logics while having control on the proof search.