@inproceedings{0a4419b961874dbea80a9fa4afd9d288,
title = "Detecting inconsistencies in large first-order knowledge bases",
abstract = "Large formalizations carry the risk of inconsistency, and hence may lead to instances of spurious reasoning. This paper describes a new approach and tool that automatically probes large first-order axiomatizations for inconsistency, by selecting subsets of the axioms centered on certain function and predicate symbols, and handling the subsets to a first-order theorem prover to test for unsatisfiability. The tool has been applied to several large axiomatizations, inconsistencies have been found, inconsistent cores extracted, and semi-automatic analysis of the inconsistent cores has helped to pinpoint the axioms that appear to be the underlying cause of inconsistency.",
author = "Stephan Schulz and Geoff Sutcliffe and Josef Urban and Adam Pease",
note = "Funding Information: J. Urban—Supported by the ERC Consolidator grant no. 649043 AI4REASON. Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 26th International Conference on Automated Deduction, CADE-26 2017 ; Conference date: 06-08-2017 Through 11-08-2017",
year = "2017",
doi = "10.1007/978-3-319-63046-5_19",
language = "English (US)",
isbn = "9783319630458",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "310--325",
editor = "{de Moura}, Leonardo",
booktitle = "Automated Deduction",
}