The FaCT System

  • Ian Horrocks
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


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.


Theorem Prover Description Logic Propositional Modal Logic Tableau Algorithm Alternative Branch 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    F. Baader, M. Buchheit, and B. Hollunder. Cardinality restrictions on concepts. Artificial Intelligence, 88(1–2):195–213, 1996.zbMATHCrossRefGoogle Scholar
  2. 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. 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
  4. 4.
    F. Baader and B. Hollunder. Kris: Knowledge representation and inference system. SIGART Bulletin, 2(3):8–14, 1991.CrossRefGoogle Scholar
  5. 5.
    A. B. Baker. Intelligent Backtracking on Constraint Satisfaction Problems: Experimental and Theoretical Results. PhD thesis, University of Oregon, 1995.Google Scholar
  6. 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
  7. 7.
    M. Buchheit, F. M. Donini, and A. Schaerf. Decidable reasoning in terminological knowledge representation systems. Journal of Artificial Intelligence Research, 1:109–138, 1993.zbMATHMathSciNetGoogle Scholar
  8. 8.
    M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394–397, 1962.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 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
  10. 10.
    J. W. Freeman. Hard random 3-SAT problems and the Davis-Putnam procedure. Artificial Intelligence, 81:183–198, 1996.CrossRefMathSciNetGoogle Scholar
  11. 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. 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. 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. 14.
    I. Horrocks. Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester, 1997.Google Scholar
  15. 15.
    F. Oppacher and E. Suen. HARP: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69–100, 1988.CrossRefMathSciNetGoogle Scholar
  16. 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. 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
  18. 18.
    M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48:1–26, 1991.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Ian Horrocks
    • 1
  1. 1.Medical Informatics Group, Department of Computer ScienceUniversity of ManchesterManchesterUK

Personalised recommendations