Abstract
The structural subsumption algorithm is restricted to a quite inexpressive language. Simple Tableaux based algorithms generally fails to provide short proofs. On the other hand, the latter has a useful property, it returns a counter-model from an unsuccessful proof. A counter-model, that is, an interpretation that falsifies the premise, is a quite useful object to a knowledge-base engineer. In this chapter we compare our \(\mathrm{ SC} _{\mathcal{ ALC} }\) system with the structural subsumption algorithm and the Tableaux algorithm for \(\mathcal{ ALC} \).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Baader, F.: The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 The Author(s)
About this chapter
Cite this chapter
Rademaker, A. (2012). Comparing \(\mathrm{ SC} _{\mathcal{ ALC} }\) with Other \(\mathcal{ ALC} \) Deduction Systems. In: A Proof Theory for Description Logics. SpringerBriefs in Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-4002-3_4
Download citation
DOI: https://doi.org/10.1007/978-1-4471-4002-3_4
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-4471-4001-6
Online ISBN: 978-1-4471-4002-3
eBook Packages: Computer ScienceComputer Science (R0)