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, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Didier Galmiche and Dominique Larchey-Wendling. 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), Sep 2013, Nancy, France. Springer-Verlag, 8123, pp.149--156, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00906789
Contributeur : Stéphane Graham-Lengrand <>
Soumis le : mercredi 20 novembre 2013 - 12:51:03
Dernière modification le : jeudi 12 avril 2018 - 01:45:50
Document(s) archivé(s) le : vendredi 21 février 2014 - 04:28:19

Fichier

Psyche.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00906789, version 1

Collections

Citation

Stéphane Graham-Lengrand. Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. Didier Galmiche and Dominique Larchey-Wendling. 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), Sep 2013, Nancy, France. Springer-Verlag, 8123, pp.149--156, 2013, Lecture Notes in Computer Science. 〈hal-00906789〉

Partager

Métriques

Consultations de la notice

195

Téléchargements de fichiers

107