Stéphane Graham-Lengrand (LIX)

Psyche 2.0: a platform for proof-search modulo theories, with quantifiers

Abstract: Psyche is a modular proof-search engine designed for either interactive or automated theorem proving, aiming at both versatility and trust: It offers an API to support user-defined reasoning techniques, while guaranteeing correctness of the final output. For this it adopts a kernel-plugin architecture that extends the LCF paradigm to guarantee, using private types, not only soundness but also completeness of the proof-search answer. A new division of labour is organised between the LCF kernel and its programmed plugins, based on a focused sequent calculus for polarised logic. This calculus generalises tableaux-like proof-search and logic programming, with backtracking mechanisms for the exploration of the search space. Psyche features the ability to call decision procedures such as those used in Sat-Modulo-Theories solvers. We therefore illustrate Psyche by using it for SMT-solving, but we also discuss how Psyche 2.0 handles quantifiers in presence of a theory.