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

4 Scopus citations

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.

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
Pages310-325
Number of pages16
ISBN (Print)9783319630458
DOIs
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

Other

Other26th International Conference on Automated Deduction, CADE-26 2017
CountrySweden
CityGothenburg
Period8/6/178/11/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Schulz, S., Sutcliffe, G., Urban, J., & Pease, A. (2017). Detecting inconsistencies in large first-order knowledge bases. In L. de Moura (Ed.), Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings (pp. 310-325). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10395 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-319-63046-5_19