×

Reasoning support for expressive ontology languages using a theorem prover. (English) Zbl 1177.68179

Dix, Jürgen (ed.) et al., Foundations of information and knowledge systems. 4th international symposium, FoIKS 2006, Budapest, Hungary, February 14–17, 2006. Proceedings. Berlin: Springer (ISBN 3-540-31782-1/pbk). Lecture Notes in Computer Science 3861, 201-218 (2006).
Summary: It is claimed in [D. Tsarkov, A. Riazanov, S. Bechhofer and I. Horrocks, “Using Vampire to reason with OWL”, Lect. Notes Comput. Sci. 3298, 471–485 (2004)] that first-order theorem provers are not efficient for reasoning with ontologies based on description logics compared to specialised description logic reasoners. However, the development of more expressive ontology languages requires the use of theorem provers able to reason with full first-order logic and even its extensions. So far, theorem provers have extensively been used for running experiments over TPTP containing mainly problems with relatively small axiomatisations. A question arises whether such theorem provers can be used to reason in real time with large axiomatisations used in expressive ontologies such as SUMO. In this paper we answer this question affirmatively by showing that a carefully engineered theorem prover can answer queries to ontologies having over 15,000 first-order axioms with equality. Ontologies used in our experiments are based on the language KIF, whose expressive power goes far beyond the description logic based languages currently used in the Semantic Web.
For the entire collection see [Zbl 1098.68002].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T30 Knowledge representation
PDFBibTeX XMLCite
Full Text: DOI