Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __                                  
			  / _`  _   /  /  o           
			 /   ) __) /  /  / /  / /\/| 
			(___/ (_/ (_ (_ / (__/ /   |  
                                                
			  I N R I A - Rocquencourt
                      Salle de réunion du bâtiment 11

                             JEUDI 19 juin, 10h30

                          -------------------------
                          Stéphane Graham-Lengrand
                          -------------------------

                                     LIX

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

             [Veuillez noter le jour inhabituel: JEUDI 19 juin.]

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.
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 (quantifier-free), but we also
discuss how to extend Psyche to handle quantifiers, especially the use
of meta-variables in presence of backtracking and a background theory.