DL Reasoner vs. First-Order Prover.
Published 1 January 2003
Dmitry Tsarkov, Ian Horrocks
Citations36
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This work compares the performance of a DL reasoner with a FO prover on reasoning problems encountered during the classification of realistic knowledge bases.
Abstract
We compare the performance of a DL reasoner with a FO prover on reasoning problems encountered during the classification of realistic knowledge bases.
Keywords
Computer Science
Cambridge University Press eBooksThe Description Logic Handbook
6,212 Citations2007Franz Baader, Franz Baader +17 more
A correspondence theory for terminological logics: preliminary report
466 Citations1991Klaus Schild
It is proved that universal implications can be expressed within TSC, and it is shown that features correspond to deterministic programs in dynamic logic preserves decidability, although violates its finite model property.
AI CommunicationsThe design and implementation of VAMPIRE
417 Citations2002Alexandre Riazanov, Андрей Воронков
This article describes VAMPIRE: a high-performance theorem prover for first-order logic and focuses on the design of the system and some key implementation features.
Using an Expressive Description Logic: FaCT or Fiction?
396 Citations1998Ian Horrocks
This paper describes a sound and complete tableaux subsumption testing algorithm for a relatively expressive Description Logic which, in spite of the logic’s worst case complexity, has been shown to perform well in realistic applications.
Artificial IntelligenceOn the relative expressiveness of description logics and predicate logics
362 Citations1996Alex Borgida
It is shown that the descriptions built using the constructors usually considered in the DL literature are characterized exactly as the predicates definable by formulas in \ tL3, the subset of first-order predicate calculus with monadic and dyadic predicates which allows only three variable symbols.
SciDok (Saarland University and State Library)An empirical analysis of optimization techniques for terminological representation systems : or: 'Making KRIS get a move on'
180 Citations1993Franz Baader, Bernhard Hollunder +3 more
Different methods of optimizing the classification process of terminological representation systems are considered, and their effect on three different types of test data is evaluated.
PubMedGoals for concept representation in the GALEN project.
125 Citations1993Alan Rector, W. A. Nowlan +1 more
The GALEN project aims to develop language independent concept representation systems as the foundations for the next generation of multilingual coding systems, which should provide the flexibility required to cope with the diversity amongst medical applications, whilst ensuring the coherence necessary for integration and re-use of terminologies.
Journal of Automated ReasoningSETHEO and E-SETHEO - The CADE-13 Systems
82 Citations1997Max Moser, Ortrun Ibens +5 more
An overview of the theoretical background, the system architecture, and the performance of both model elimination theorem prover SETHEO and its equational extension E-SETHEO are presented.
Lecture notes in computer scienceMSPASS: Modal Reasoning by Translation and First-Order Resolution
74 Citations2000Ullrich Hustadt, Renate A. Schmidt
Themspass is an extension of the first-order theorem prover spass, which can be used as a modal logic theoremProver, a theorem Prover for description logics and a theorem provers for the relational calculus.
The Generation of DAML+OIL.
29 Citations2001Ian Horrocks, Peter F. Patel‐Schneider
daml+oil is a new description logic developed for use within the DAML project and as a submission to the upcoming W3C semantic web ontology working group, closely based on the oil.