Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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
Contributor : Kaustuv Chaudhuri Connect in order to contact the contributor
Submitted on : Friday, October 30, 2015 - 11:31:02 AM
Last modification on : Wednesday, February 2, 2022 - 3:55:17 PM
Long-term archiving on: : Sunday, January 31, 2016 - 11:02:28 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License



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⟩



Record views


Files downloads