Automated deduction techniques for subsumption checking in concept languages

摘要

Mechanical theorem provers are becoming increasingly more powerful, and we believe that it is time to re-examine whether certain tasks that have formerly been accomplished by other means, can now be performed by a theorem prover. One such task is subsumption determination in knowledge representation systems. Terminological Knowledge Representation Systems (or Concept Languages) provide a means for expressing knowledge in the form of concepts and roles. Checking subsumptions between concepts is an important reasoning faculty offered by these systems. In this paper, we examine the subsumption checking performance of a first-order theorem prover coupled with a finite-model finder. This is a complete reasoning system, as concept languages have the finite-model property. We show that this is an efficient reasoning system by means of tests used by [5] to compare concept languages systems.