Detecting inconsistencies in large first-order knowledge bases

Stephan Schulz; Geoff Sutcliffe; Josef Urban; Adam Pease

doi:10.1007/978-3-319-63046-5_19

Detecting inconsistencies in large first-order knowledge bases

Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Automated Deduction
Subtitle of host publication	CADE 26 - 26th International Conference on Automated Deduction, Proceedings
Editors	Leonardo de Moura
Publisher	Springer Verlag
Pages	310-325
Number of pages	16
ISBN (Print)	9783319630458
DOIs	https://doi.org/10.1007/978-3-319-63046-5_19
State	Published - 2017
Event	26th International Conference on Automated Deduction, CADE-26 2017 - Gothenburg, Sweden Duration: Aug 6 2017 → Aug 11 2017

Publication series

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

Other

Other	26th International Conference on Automated Deduction, CADE-26 2017
Country	Sweden
City	Gothenburg
Period	8/6/17 → 8/11/17

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-63046-5_19

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

Detecting inconsistencies in large first-order knowledge bases. / Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam.

Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings. ed. / Leonardo de Moura. Springer Verlag, 2017. p. 310-325 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10395 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10395 LNAI, Springer Verlag, pp. 310-325, 26th International Conference on Automated Deduction, CADE-26 2017, Gothenburg, Sweden, 8/6/17. https://doi.org/10.1007/978-3-319-63046-5_19

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

Schulz, Stephan ; Sutcliffe, Geoff ; Urban, Josef ; Pease, Adam. / Detecting inconsistencies in large first-order knowledge bases. Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings. editor / Leonardo de Moura. Springer Verlag, 2017. pp. 310-325 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0a4419b961874dbea80a9fa4afd9d288,

title = "Detecting inconsistencies in large first-order knowledge bases",

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.",

author = "Stephan Schulz and Geoff Sutcliffe and Josef Urban and Adam Pease",

year = "2017",

doi = "10.1007/978-3-319-63046-5_19",

language = "English (US)",

isbn = "9783319630458",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "310--325",

editor = "{de Moura}, Leonardo",

booktitle = "Automated Deduction",

note = "26th International Conference on Automated Deduction, CADE-26 2017 ; Conference date: 06-08-2017 Through 11-08-2017",

}

TY - GEN

T1 - Detecting inconsistencies in large first-order knowledge bases

AU - Schulz, Stephan

AU - Sutcliffe, Geoff

AU - Urban, Josef

AU - Pease, Adam

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85026727806&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85026727806&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-63046-5_19

DO - 10.1007/978-3-319-63046-5_19

M3 - Conference contribution

AN - SCOPUS:85026727806

SN - 9783319630458

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 310

EP - 325

BT - Automated Deduction

A2 - de Moura, Leonardo

PB - Springer Verlag

T2 - 26th International Conference on Automated Deduction, CADE-26 2017

Y2 - 6 August 2017 through 11 August 2017

ER -