Icon: A diagrammatic theorem prover for ontologies
View / Open Files
Publication Date
2018Journal 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
ISBN
9781577358039
Publisher
AAAI Press
Pages
204-208
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Shams, Z., Jamnik, M., Stapleton, G., & Sato, Y. (2018). Icon: A diagrammatic theorem prover for ontologies. Principles of Knowledge Representation and Reasoning: Proceedings of the 16th International Conference, KR 2018, 204-208. https://doi.org/10.17863/CAM.35154
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.
Sponsorship
Zohreh
Funder references
Leverhulme Trust (RPG-2016-082)
Identifiers
External DOI: https://doi.org/10.17863/CAM.35154
This record's URL: https://www.repository.cam.ac.uk/handle/1810/287839
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.