Repository logo
 

Icon: A diagrammatic theorem prover for ontologies

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Stapleton, G 
Sato, Y 

Abstract

Concept diagrams form a visual language that is aimed at non-experts for the specification of ontologies and reason- ing about them. Empirical evidence suggests that they are more accessible to ontology users than symbolic notations typically used for ontologies (e.g., DL, OWL). Here, we re- port on iCon, a theorem prover for concept diagrams that al- lows reasoning about ontologies diagrammatically. The input to iCon is a theorem that needs proving to establish how an entailment, in an ontology that needs debugging, is caused by a minimal set of axioms. Such a minimal set of axioms is called an entailment justification. Carrying out inference in iCon provides a diagrammatic proof (i.e., explanation) that shows how the axioms in an entailment justification give rise to the entailment under investigation. iCon proofs are for- mally verified and guaranteed to be correct.

Description

Keywords

Journal Title

Principles of Knowledge Representation and Reasoning: Proceedings of the 16th International Conference, KR 2018

Conference Name

International Conference on Principles of Knowledge Representation and Reasoning

Journal ISSN

2334-1033

Volume Title

Publisher

AAAI Press
Sponsorship
Leverhulme Trust (RPG-2016-082)
Zohreh