Extracting Proofs from Tabled Proof Search

Dale Miller 1, 2 Alwen Tiu 3
1 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
3 School of Computer Engineering
NTU - School of Computer Engineering [Singapore]
Abstract : We consider the problem of model checking specifications involving co-inductive definitions such as are available for bisimulation. A proof search approach to model checking with such specifications often involves state exploration. We consider four different tabling strategies that can minimize such exploration significantly. In general, tabling involves storing previously proved subgoals and reusing (instead of reproving) them in proof search. In the case of co-inductive proof search, tables allow a limited form of loop checking, which is often necessary for, say, checking bisimulation of non-terminating processes. We enhance the notion of tabled proof search by allowing a limited deduction from tabled entries when performing table lookup. The main problem with this enhanced tabling method is that it is generally unsound when co-inductive definitions are involved and when tabled entries contain unproved entries. We design a proof system with tables and show that by managing tabled entries carefully, one would still be able to obtain a sound proof system. That is, we show how one can extract a post-fixed point from a tabled proof for a co-inductive goal. We then apply this idea to the technique of bisimulation ''up-to'' commonly used in process algebra.
Type de document :
Pré-publication, Document de travail
2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00863561
Contributeur : Dale Miller <>
Soumis le : jeudi 19 septembre 2013 - 10:56:05
Dernière modification le : jeudi 12 avril 2018 - 01:48:52
Document(s) archivé(s) le : jeudi 6 avril 2017 - 23:47:15

Fichier

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

Identifiants

  • HAL Id : hal-00863561, version 1

Collections

Citation

Dale Miller, Alwen Tiu. Extracting Proofs from Tabled Proof Search. 2013. 〈hal-00863561〉

Partager

Métriques

Consultations de la notice

334

Téléchargements de fichiers

87