iCon: A Diagrammatic Theorem Prover for Ontologies

Concept diagrams form a visual language that is aimed at non-experts for the specification of ontologies and reasoning about them. Empirical evidence suggests that they are more accessible to ontology users than symbolic notations typically used (e.g., DL, OWL). Here, we report on iCon, an interactive theorem prover for concept diagrams that allows 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 formally verified and guaranteed to be correct.