[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Prefixed Resolution: A Resolution Method for Modal and Description Logics

  • Conference paper
  • First Online:
Automated Deduction — CADE-16 (CADE 1999)

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

Included in the following conference series:

Abstract

We provide a resolution-based proof procedure for modal and description logics that improves on previous proposals in a number of important ways. First, it avoids translations into large undecidable logics, and works directly on modal or description logic formulas instead. Second, by using labeled formulas it avoids the complexities of earlier propositional resolution-based methods for modal logic. Third, it provides a method for manipulating so-called assertional information in the description logic setting. And fourth, we believe that it combines ideas from the method of prefixes used in tableaux and resolution in such a way that some of the heuristics and optimizations devised in either field are applicable.

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. Y. Auffray, P. Enjalbert, and J. Hebrard. Strategies for modal resolution: results and problems. Journal of Automated Reasoning, 6(1):1–38, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  2. F. Baader, B. Hollunder, B. Nebel, H. Profitlich, and E. Franconi. An empirical analysis of optimization techniques for terminological representation systems or: Making KRIS get a move on. Journal of Applied Intelligence, 4:109–132, 1994.

    Article  Google Scholar 

  3. P. Blackburn. Internalizing labeled deduction. Technical Report CLAUS-Report 102, Computerlinguistik, Universität des Saarlandes, 1998.

    Google Scholar 

  4. P. Blackburn and M. Tzakova. Hybridizing concept languages. Annals of Mathematics and Artificial Intelligence, 24:23–49, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  5. R. Brachman and H. Levesque. The tractability of subsumption in frame-based description languages. In AAAI-84, pages 34–37, 1984.

    Google Scholar 

  6. R. Brachman and J. Schmolze. An overview of the KL-ONE knowledge representation system. Cognitive Science, 9(2):171–216, 1985.

    Article  Google Scholar 

  7. D. Calvanese, G. De Giacomo, and M. Lenzerini. Conjunctive query containment in description logics with n-ary relations. In Proc. of DL-97, pages 5–9, June 1997.

    Google Scholar 

  8. H. de Nivelle. Ordering refinements of resolution. PhD thesis, Technische Universiteit Delft, Delft. The Netherlands, October 1994.

    Google Scholar 

  9. H. de Nivelle and M. de Rijke. Resolution decides the guarded fragment. Submitted for journal publication, 1998.

    Google Scholar 

  10. M. de Rijke. Restricted description languages. Unpublished, 1998.

    Google Scholar 

  11. F. Donini, M. Lenzerini, D. Nardi, and A. Schaerf. Deduction in concept languages: from subsumption to instance checking. Journal of Logic and Computation, 4(4):423–452, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  12. P. Enjalbert and L. Fariñas del Cerro. Modal resolution in clausal form. Theoretical Computer Science, 65(1):1–33, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  13. L. Fariñas del Cerro. A simple deduction method for modal logic. Information Processing Letters, 14:49–51, April 1982.

    Article  MATH  MathSciNet  Google Scholar 

  14. C. Fermüller, A. Leitsch, T. Tammet, and N. Zamov. Resolution methods for the decision problem. Springer-Verlag, Berlin, 1993. LNAI.

    MATH  Google Scholar 

  15. I. Horrocks and P. Patel-Schneider. Optimising description logic subsumption. Submitted to the Journal of Logic and Computation, 1998.

    Google Scholar 

  16. U. Hustadt and R. Schmidt. Issues of decidability for description logics. Unpublished, 1998.

    Google Scholar 

  17. G. Mints. Resolution calculi for modal logics. American Mathematical Society Translations, 143:1–14, 1989.

    Google Scholar 

  18. K. Schild. A correspondence theory for terminological logics. In Proc. of the 12th IJCAI, pages 466–471, 1991.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  20. T. Tammet. Using resolution for extending KL-ONE-type languages. In Proc. of the 4th CIKM. ACM Press, November 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ILLC, University of Amsterdam, Plantage Muidergracht, 24 1018, TV Amsterdam, The Netherlands

    Carlos Areces, Hans de Nivelle & Maarten de Rijke

Authors
  1. Carlos Areces
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hans de Nivelle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maarten de Rijke
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Areces, C., de Nivelle, H., de Rijke, M. (1999). Prefixed Resolution: A Resolution Method for Modal and Description Logics. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-48660-7_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66222-8

  • Online ISBN: 978-3-540-48660-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics