Detecting Inconsistencies in Large First-Order Knowledge Bases
 
                   Stephan Schulz
                   Geoff Sutcliffe
                   Josef Urban
                   Adam Pease

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.