The FaCT System | SpringerLink
Skip to main content
Springer Nature Link
Log in

The FaCT System

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1397))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. F. Baader, M. Buchheit, and B. Hollunder. Cardinality restrictions on concepts. Artificial Intelligence, 88(1–2):195–213, 1996.

    Article  MATH  Google Scholar 

  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 

  4. F. Baader and B. Hollunder. Kris: Knowledge representation and inference system. SIGART Bulletin, 2(3):8–14, 1991.

    Article  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 

  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.

    MATH  MathSciNet  Google Scholar 

  8. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394–397, 1962.

    Article  MATH  MathSciNet  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 

  10. J. W. Freeman. Hard random 3-SAT problems and the Davis-Putnam procedure. Artificial Intelligence, 81:183–198, 1996.

    Article  MathSciNet  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 

  15. F. Oppacher and E. Suen. HARP: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69–100, 1988.

    Article  MathSciNet  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 

  18. M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48:1–26, 1991.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Medical Informatics Group, Department of Computer Science, University of Manchester, Manchester, M13 9PL, UK

    Ian Horrocks

Authors
  1. Ian Horrocks
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000 LE, Tilburg, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Horrocks, I. (1998). The FaCT System. 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_30

Download citation

  • DOI: https://doi.org/10.1007/3-540-69778-0_30

  • 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

Publish with us

Policies and ethics

Search

Navigation