@inproceedings{11a82821fe3542498638b47928fa15a3,
title = "Disproving using the inverse method by iterative refinement of finite approximations",
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.",
author = "Taus Rock-Nannestad and Kaustuv Chaudhuri",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2015 ; Conference date: 21-09-2015 Through 24-09-2015",
year = "2015",
month = jan,
day = "1",
doi = "10.1007/978-3-319-24312-2\_11",
language = "English",
isbn = "9783319243115",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "153--168",
editor = "\{de Nivelle\}, Hans",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Proceedings",
}