Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations

Taus Brock-Nannestad 1 Kaustuv Chaudhuri 1
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
Abstract : In first-order logic, forward search using a complete strategy such as the inverse method can get stuck deriving larger and larger consequence sets when the goal query is unprovable. This is the case even in trivial theories where backward search strategies such as tableaux methods will fail finitely. We propose a general mechanism for bounding the consequence sets by means of finite approximations of infinite types. If the inverse method also implements forward subsumption and globalization, then the search space under this approximation is finite. We therefore obtain a type-directed iterative refinement algorithm for disproving queries. The method has been implemented for intuitionistic first-order logic, and we discuss its performance on a variety of problems.
Type de document :
Communication dans un congrès
Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wrocław, Poland. 〈http://tableaux2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24312-2_11〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01222592
Contributeur : Kaustuv Chaudhuri <>
Soumis le : vendredi 30 octobre 2015 - 11:31:02
Dernière modification le : jeudi 10 mai 2018 - 02:06:56
Document(s) archivé(s) le : dimanche 31 janvier 2016 - 11:02:28

Fichiers

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

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Citation

Taus Brock-Nannestad, Kaustuv Chaudhuri. Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations. Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wrocław, Poland. 〈http://tableaux2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24312-2_11〉. 〈hal-01222592〉

Partager

Métriques

Consultations de la notice

463

Téléchargements de fichiers

70