Detecting inconsistencies in large first-order knowledge bases

Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationAutomated Deduction
Subtitle of host publicationCADE 26 - 26th International Conference on Automated Deduction, Proceedings
EditorsLeonardo de Moura
PublisherSpringer Verlag
Number of pages16
ISBN (Print)9783319630458
StatePublished - 2017
Event26th International Conference on Automated Deduction, CADE-26 2017 - Gothenburg, Sweden
Duration: Aug 6 2017Aug 11 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10395 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other26th International Conference on Automated Deduction, CADE-26 2017

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Detecting inconsistencies in large first-order knowledge bases'. Together they form a unique fingerprint.

Cite this