Skip to Main content Skip to Navigation
Conference papers

Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture

Stéphane Graham-Lengrand 1, 2 
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Psyche is a modular proof-search engine designed for either interactive or automated theorem proving, and aiming at two things: a high level of confidence about the output of the theorem proving process and the ability to apply and combine a wide range of techniques. It ad- dresses the first aim by adopting and extending the LCF architecture to guarantee, using private types, not only the correctness but also the com- pleteness of proof search. It addresses the second by offering a much more appropriate API than just the primitives corresponding to the inference rules of the logic in natural deduction: it uses instead a focused sequent calculus for polarised classical logic. Finally, 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Stéphane Graham-Lengrand Connect in order to contact the contributor
Submitted on : Wednesday, November 20, 2013 - 12:51:03 PM
Last modification on : Thursday, January 20, 2022 - 5:30:44 PM
Long-term archiving on: : Friday, February 21, 2014 - 4:28:19 AM


Files produced by the author(s)


  • HAL Id : hal-00906789, version 1



Stéphane Graham-Lengrand. Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), Sep 2013, Nancy, France. pp.149--156. ⟨hal-00906789⟩



Record views


Files downloads