Skip to Main content Skip to Navigation
Conference papers

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
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01222592
Contributor : Kaustuv Chaudhuri <>
Submitted on : Friday, October 30, 2015 - 11:31:02 AM
Last modification on : Friday, April 30, 2021 - 10:02:41 AM
Long-term archiving on: : Sunday, January 31, 2016 - 11:02:28 AM

Files

disproving.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License

Identifiers

Collections

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. ⟨10.1007/978-3-319-24312-2_11⟩. ⟨hal-01222592⟩

Share

Metrics

Record views

738

Files downloads

308