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.
Cite
CITATION STYLE
Schulz, S., Sutcliffe, G., Urban, J., & Pease, A. (2017). Detecting inconsistencies in large first-order knowledge bases. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10395 LNAI, pp. 310–325). Springer Verlag. https://doi.org/10.1007/978-3-319-63046-5_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
