Focused Inductive Theorem Proving

David Baelde 1 Dale Miller 2, 3 Zachary Snow 4
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Focused proof systems provide means for reducing and structuring the non-determinism involved in searching for sequent calculus proofs. We present a focused proof system for a first-order logic with inductive and co-inductive definitions in which the introduction rules are partitioned into an asynchronous phase and a synchronous phase. These focused proofs allow us to naturally see proof search as being organized around interleaving intervals of computation and more general deduction. For example, entire Prolog-like computations can be captured using a single synchronous phase and many model-checking queries can be captured using an asynchronous phase followed by a synchronous phase. Leveraging these ideas, we have developed an interactive proof assistant, called Tac, for this logic. We describe its high-level design and illustrate how it is capable of automatically proving many theorems using induction and coinduction. Since the automatic proof procedure is structured using focused proofs, its behavior is often rather easy to anticipate and modify. We illustrate the strength of Tac with several examples of proved theorems, some achieved entirely automatically and others achieved with user guidance.
Type de document :
Communication dans un congrès
IJCAR 2010 - International Joint Conference on Automated Deduction, 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 17:50:46
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 11 avril 2013 - 04:08:12


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00772592, version 1



David Baelde, Dale Miller, Zachary Snow. Focused Inductive Theorem Proving. IJCAR 2010 - International Joint Conference on Automated Deduction, 2010, Edinburgh, United Kingdom. 2010. 〈hal-00772592〉



Consultations de la notice


Téléchargements de fichiers