The FaCT System
- 245 Downloads
FaCT is a Description Logic classifier which has been implemented as a test-bed for a highly optimised tableaux satisfiability (subsumption) testing algorithm. The correspondence between modal and description logics also allows FaCT to be used as a theorem prover for the propositional modal logics K, KT, K4 and S4. Empirical tests have demonstrated the effectiveness of the optimised implementation and, in particular, of the dependency directed backtracking optimisation.
KeywordsTheorem Prover Description Logic Propositional Modal Logic Tableau Algorithm Alternative Branch
Unable to display preview. Download preview PDF.
- 2.F. Baader, E. Franconi, B. Hollunder, B. Nebel, and H.-J. Profitlich. An empirical analysis of optimization techniques for terminological representation systems or: Making KRIS get a move on. 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.Google Scholar
- 3.F. Baader, H.-J. Heinsohn, B. Hollunder, J. Muller, B. Nebel, W. Nutt, and H.-J. Profitlich. Terminological knowledge representation: A proposal for a terminological logic. Technical Memo TM-90-04, Deutsches Forschungszentrum für Künstliche Intelligenz GmbH (DFKI), 1991.Google Scholar
- 5.A. B. Baker. Intelligent Backtracking on Constraint Satisfaction Problems: Experimental and Theoretical Results. PhD thesis, University of Oregon, 1995.Google Scholar
- 6.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.Google Scholar
- 9.J. W. Freeman. Improvements to propositional satisfiability search algorithms. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, USA, 1995.Google Scholar
- 11.F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures—the case study of modal K. In Michael McRobbie and John Slaney, editors, Proceedings of the Thirteenth International Conference on Automated Deduction (CADE-13), number 1104 in Lecture Notes in Artificial Intelligence, pages 583–597. Springer, 1996.Google Scholar
- 12.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.Google Scholar
- 13.A. Heuerding and S. Schwendimann. A benchmark method for the propositional modal logics k, kt, s4. Technical report IAM-96-015, University of Bern, Switzerland, October 1996.Google Scholar
- 14.I. Horrocks. Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester, 1997.Google Scholar
- 16.U. Sattler. A concept language extended with different kinds of transitive roles. In G. Görz and S. Hölldobler, editors, 20. Deutsche Jahrestagung für Künstliche Intelligenz, number 1137 in Lecture Notes in Artificial Intelligence, pages 333–345. Springer Verlag, 1996.Google Scholar
- 17.K. Schild. A correspondence theory for terminological logics: Preliminary report. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), pages 466–471, 1991.Google Scholar