nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Locating Things in Space and Time: Verification of the SUMO Upper-Level Ontology

verfasst von : Lydia Silva Muñoz, Michael Grüninger

Erschienen in: Knowledge Engineering and Knowledge Management

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Upper-level ontologies provide an account of the most basic, domain independent entities, such as time, space, objects and processes. They are intended to be broadly reused, among others, during ontology engineering tasks, such as ontology building and integration. Ontology verification is the process by which a theory is checked to rule out its unintended models, and possibly characterize missing intended ones. In this paper, we translate into first-order logic, modularize, and verify the subtheory of location of entities in space and time of the Suggested Upper Merged Ontology (SUMO). As a result, we propose the addition of some axioms that rule out unintended models in SUMO, the correction of others, and make available a modularized version of SUMO characterization of location of entities in time and space represented in standard first-order logic.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Word Tagging with Foundational Ontology Classes: Extending the WordNet-DOLCE Mapping to Verbs

Nächstes Kapitel Detecting Meaningful Compounds in Complex Class Labels

We assume that an ontology is a set of sentences called axioms closed under logical entailment that state the properties that characterize the behaviour of a set of symbols representing constants, relations and functions, called the signature of the ontology.

http://suo.ieee.org/SUO/KIF/suo-kif.html.

http://logic.stanford.edu/kif/kif.html.

Available at colore.oor.net/ontologies/sumo/modules.

A theory ${T'}$ is a conservative extension of a theory T if every theorem of T is a theorem of ${T'}$, and every theorem of ${T'}$ in the signature of T is also a theorem of T.

Axiom (4) is a consequence of axiom (2).

SUMO also defines predicates properPart, overlapsPartially, and characterizes function symbols MereologicalProductFn and MereologicalDifferenceFn.

Sentences (37) and (38) result from the translation into standard first-order logic of SUMO higher-order sentence $(\forall x,y,t) (WhereFn(x,t)=y)\leftrightarrow holdsDuring(t,exactlyLocated(x,y))$.

Category SelfConnectedObject is defined in axiom (23).

Proof available at: colore.oor.net/ontologies/sumo/location/proofs.

Only objects of category Vehicle participating as an instrument of a Translocation process have their location related to the objects declared as the origin and destination of the process respectively at the time where the process begins and ends by means of a higher-order construct, which represents a change of location for objects of category Vehicle.

Axiom (56) follows from the fact that Object and Process are disjoint categories.

Proof available at: colore.oor.net/ontologies/sumo/location/proofs.

Predicates path, origin, and destination are characterized in SUMO as antisymmetric relations whose first and second arguments are respectively individuals of Process and Object.

We have found that the following SUO-KIF axiom of SUMO, intended to further characterize predicate origin, is syntactically incorrect and incomprehensible. We assume that it is a typo.

$$\begin{aligned} \begin{aligned} \small&\mathtt {(=> (origin ?PROCESS ?OBJ)}\\&\mathtt {(eventLocated (WhereFn ?PROCESS (BeginFn (WhenFn ?PROCESS)))}\\&\mathtt {(WhereFn ?OBJ (BeginFn (WhenFn ?OBJ)))))} \end{aligned} \end{aligned}$$

The instantiation of the following schema for each binary predicate rel of SUMO also contributes to characterizing the temporal overlap of related entities: $(\forall x,y,t) holdsDuring(t,rel(x,y)) \wedge Physical(x) \wedge Physical(y)\rightarrow time(x,t) \wedge time(y,t)$.

Axiom (61) results from the translation into first-order logic of SUO-KIF sentence $(\forall x,y,rel) (BinaryPredicate(rel) \wedge SpatialRelation(rel) \wedge rel(x,y))\rightarrow overlapsTemporally(WhenFn(x),WhenFn(y))$.

Axiom (63) results from the translation into first-order logic of SUO-KIF sentence $(\forall x,rel,p) (CaseRole(rel) \wedge Object(x) \wedge rel(p,x))\rightarrow ((\exists t) overlapsSpatially(WhereFn(p,t),x))$.

Benzmüller, C., Pease, A.: Higher-order aspects and context in SUMO. J. Web Sem. 12, 104–117 (2012)CrossRef

Casati, R., Varzi, A.C.: Parts and Places: The Structures of Spatial Representation. A Bradford book. MIT Press, Cambridge (1999)

Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, Cambridge (1972)MATH

Euzenat, J., Shvaiko, P.: Ontology Matching, 2nd edn. Springer, Heidelberg (DE) (2013)CrossRefMATH

Grüninger, M., Hahmann, T., Hashemi, A., Ong, D.: Ontology verification with repositories. In: Formal Ontology in Information Systems, Proceedings of the Sixth International Conference, FOIS 2010, Toronto, Canada, 11–14 May 2010, pp. 317–330 (2010)

Guarino, N.: Formal ontology and information systems. In: Formal Ontology in Information Systems - Proceedings of FOIS 1998, Trento, Italy, 6–8 June 1998, pp. 3–15. IOS Press, Amsterdam (1998)

McCune, W.: Prover9 and Mace4 (2005–2010). http://www.cs.unm.edu/~mccune/prover9/

Silva Muñoz, L., Grüninger, M.: Verifying and mapping the mereotopology of upper-level ontologies. In: Knowledge Engineering and Ontology Development (KEOD), Proceedings of the 8th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management (IC3K), 9–11 November 2016, Porto, Portugal (2016)

Niles, I., Pease, A.: Linking lexicons and ontologies: mapping WordNet to the suggested upper merged ontology. In: Proceedings of the 2003 International Conference on Information and Knowledge Engineering (IKE 2003), Las Vegas, Nevada (2003)

10.

Niles, I., Pease, A.: Towards a standard upper ontology. In: FOIS 2001: Proceedings of the International Conference on Formal Ontology in Information Systems, pp. 2–9. ACM, New York (2001)

11.

Silva Muñoz, L., Grüninger, M.: Mapping and verification of the time ontology in SUMO. In: Formal Ontology in Information Systems - Proceedings of the 9th International Conference, FOIS, 6–9 July 2016, Annecy, France (2016)

12.

Achille Varzi, C.: Handbook of spatial logics, chapter spatial reasoning, ontology: parts, wholes, and locations. In: Aiello, M., Pratt-Hartmann, I., Van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 945–1038. Springer, Dordrecht (2007)CrossRef

Titel: Locating Things in Space and Time: Verification of the SUMO Upper-Level Ontology
verfasst von: Lydia Silva Muñoz
Michael Grüninger
Verlag: Springer International Publishing
Buch: Knowledge Engineering and Knowledge Management
Print ISBN: 978-3-319-49003-8

Electronic ISBN: 978-3-319-49004-5

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-49004-5_39

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"