Abstract
FaCT: The tests were performed using FaCT version 1.2. FaCT is a description logic classifier whose description language is a superset of K4(m) and whose subsumption reasoning uses a sound and complete tableaux algorithm. FaCT employs a wide range of optimisations, in particular a form of dependency directed backtracking called backjumping which can significantly reduce the size of the search space [5]. The FaCT algorithm does not support KT and S4 explicitly, but FaCT includes a preprocessing and encoding optimisation which is also able to apply the standard embedding of KT and S4 in K and K4 respectively: the time taken for preprocessing and embedding is included in the results. Programming language: Common Lisp (compiled).
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
Preview
Unable to display preview. Download preview PDF.
References
F. Baader, E. Franconi, B. Hollunder, B. Nebel, and H.-J. Profitlich. An empirical analysis of optimization techniques for terminological representation systems. In B. Nebel, C. Rich, and W. Swartout, editors, Principals of Knowledge Representation and Reasoning: Proceedings of the Third International Conference (KR’92), pages 270–281. Morgan-Kaufmann, 1992. Also available as DFKI RR-93-03.
F. Baader and B. Hollunder. A terminological knowledge representation system with complete inference algorithms. In Processing declarative knowledge: International workshop PDK’91, number 567 in Lecture Notes in Artificial Intelligence, pages 67–86, Berlin, 1991. Springer-Verlag.
P. Bresciani, E. Franconi, and S. Tessaris. Implementing and testing expressive description logics: a preliminary report. In Gerard Ellis, Robert A. Levinson, Andrew Fall, and Veronica Dahl, editors, Knowledge Retrieval, Use and Storage for Efficiency: Proceedings of the First International KRUSE Symposium, pages 28–39, 1995.
F. Giunchiglia and R. Sebastiani. A SAT-based decision procedure for ALC. In L. C. Aiello, J. Doyle, and S. Shapiro, editors, Principals of Knowledge Representation and Reasoning: Proceedings of the Fifth International Conference (KR’96), pages 304–314. Morgan Kaufmann, November 1996.
I. Horrocks. Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Horrocks, I., Patel-Schneider, P.F. (1998). FaCT and DLP. In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_5
Download citation
DOI: https://doi.org/10.1007/3-540-69778-0_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64406-4
Online ISBN: 978-3-540-69778-7
eBook Packages: Springer Book Archive