iCon: A Diagrammatic Theorem Prover for Ontologies

Zohreh Shams, Mateja Jamnik, Gemmelia Stapleton, Yuri Sato

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBNpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018)
Place of PublicationCalifornia
PublisherThe AAAI Press
Pages204-208
Number of pages5
ISBN (Print)9781577358039
Publication statusPublished - 24 Sep 2018
EventSixteenth International Conference on Principles of Knowledge Representation and Reasoning - Arizona State University, United States
Duration: 30 Oct 20182 Nov 2018

Conference

ConferenceSixteenth International Conference on Principles of Knowledge Representation and Reasoning
Country/TerritoryUnited States
Period30/10/182/11/18

Fingerprint

Dive into the research topics of 'iCon: A Diagrammatic Theorem Prover for Ontologies'. Together they form a unique fingerprint.

Cite this