MiG

Higher-Order Aspects and Context in SUMO

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

TitelHigher-Order Aspects and Context in SUMO
VerfasserC. Benzmüller, A. Pease
ThemaExpressive ontologies; Context, Classical higher-order logic, Boolean extensionality, Quantified multimodal logic, Automated theorem proving
Datum2012
Kennungdoi: 10.1016/j.websem. 2011.11.088
Quelle/n
Erschienen inWeb 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
Spracheeng
ArtText
Größe oder Längepp 104-117
Rechtehttps://s100.copyright.com/AppDispatchServlet?publisherName=ELS&contentID=S1570826811000990&orderBeanReset=true