Springe direkt zu Inhalt

Higher-Order Aspects and Context in SUMO

Christoph Benzmüller, A. Pease – 2012

This article addresses the automation of higher-order aspects in expressive ontologies such as the Suggested Upper Merged Ontology SUMO. Evidence is provided that modern higher-order automated theorem provers like LEO-II can be fruitfully employed for the task. A particular focus is on embedded formulas (formulas as terms), which are used in SUMO, for example, for modeling temporal, epistemic, or doxastic contexts. This modeling is partly in conflict with SUMO’s assumption of a bivalent, classical semantics and it may hence lead to counterintuitive reasoning results with automated theorem provers in practice. A solution is proposed that maps SUMO to quantified multimodal logic which is in turn modeled as a fragment of classical higher-order logic. This way automated higher-order theorem provers can be safely applied for reasoning about modal contexts in SUMO. Our findings are of wider relevance as they analogously apply to other expressive ontologies and knowledge representation formalisms.

Titel
Higher-Order Aspects and Context in SUMO
Verfasser
Christoph Benzmüller, A. Pease
Schlagwörter
Expressive ontologies; Context, Classical higher-order logic, Boolean extensionality, Quantified multimodal logic, Automated theorem proving
Datum
2012
Kennung
doi: 10.1016/j.websem. 2011.11.088
Quelle/n
Erschienen in
Web Semantics: Science, Services and Agents on the World Wide Web (Special Issue on Reasoning with Context in the Semantic Web) 12-13, ISSN 1570-8268, Elsevier
Sprache
eng
Art
Text
Größe oder Länge
pp 104-117
Rechte
https://s100.copyright.com/AppDispatchServlet?publisherName=ELS&contentID=S1570826811000990&orderBeanReset=true