Sciweavers

Share
FOIKS
2006
Springer

Reasoning Support for Expressive Ontology Languages Using a Theorem Prover

11 years 5 months ago
Reasoning Support for Expressive Ontology Languages Using a Theorem Prover
It is claimed in [45] 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 ...
Ian Horrocks, Andrei Voronkov
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FOIKS
Authors Ian Horrocks, Andrei Voronkov
Comments (0)
books