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 ISBN

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
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
CountryUnited States
Period30/10/182/11/18

Fingerprint

Ontology
Visual languages
Specifications

Cite this

Shams, Z., Jamnik, M., Stapleton, G., & Sato, Y. (2018). iCon: A Diagrammatic Theorem Prover for Ontologies. In Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018) (pp. 204-208). California: The AAAI Press.
Shams, Zohreh ; Jamnik, Mateja ; Stapleton, Gemmelia ; Sato, Yuri. / iCon : A Diagrammatic Theorem Prover for Ontologies. Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018). California : The AAAI Press, 2018. pp. 204-208
@inproceedings{cc0e470003a6467182692b9f875d85fe,
title = "iCon: A Diagrammatic Theorem Prover for Ontologies",
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.",
author = "Zohreh Shams and Mateja Jamnik and Gemmelia Stapleton and Yuri Sato",
year = "2018",
month = "9",
day = "24",
language = "English",
pages = "204--208",
booktitle = "Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018)",
publisher = "The AAAI Press",

}

Shams, Z, Jamnik, M, Stapleton, G & Sato, Y 2018, iCon: A Diagrammatic Theorem Prover for Ontologies. in Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018). The AAAI Press, California, pp. 204-208, Sixteenth International Conference on Principles of Knowledge Representation and Reasoning, United States, 30/10/18.

iCon : A Diagrammatic Theorem Prover for Ontologies. / Shams, Zohreh; Jamnik, Mateja; Stapleton, Gemmelia; Sato, Yuri.

Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018). California : The AAAI Press, 2018. p. 204-208.

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBN

TY - GEN

T1 - iCon

T2 - A Diagrammatic Theorem Prover for Ontologies

AU - Shams, Zohreh

AU - Jamnik, Mateja

AU - Stapleton, Gemmelia

AU - Sato, Yuri

PY - 2018/9/24

Y1 - 2018/9/24

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

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

UR - http://www.kr.org/index.php?page=proclist

M3 - Conference contribution with ISSN or ISBN

SP - 204

EP - 208

BT - Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018)

PB - The AAAI Press

CY - California

ER -

Shams Z, Jamnik M, Stapleton G, Sato Y. iCon: A Diagrammatic Theorem Prover for Ontologies. In Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018). California: The AAAI Press. 2018. p. 204-208