Repository logo

Icon: A diagrammatic theorem prover for ontologies

Accepted version


Conference Object

Change log


Stapleton, G 
Sato, Y 


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.



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


Volume Title


AAAI Press
Leverhulme Trust (RPG-2016-082)