zbMATH — the first resource for mathematics

Detecting inconsistencies in large first-order knowledge bases. (English) Zbl 06778411
de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-63045-8/pbk; 978-3-319-63046-5/ebook). Lecture Notes in Computer Science 10395. Lecture Notes in Artificial Intelligence, 310-325 (2017).
Summary: 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.
For the entire collection see [Zbl 1369.68037].

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI