Skip to main content
SpringerLink
Log in

A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic

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

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

Abstract

The clausal resolution method for propositional linear-time temporal logics is well known and provides the basis for a number of temporal provers. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules. In this paper, we show how the normal form can be radically simplified and, consequently, how a simplified clausal resolution method can be defined for this important variety of logic.

Work supported by both EPSRC (grant GR/L87491) and the University of Liverpool (RDF).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Artale and E. Franconi. Temporal description logics. In Handbook of Temporal Reasoning in Artificial Intelligence. To appear.

    Google Scholar 

  2. E. Clarke, O. Grumberg and D. A. Peled. Model Checking. MIT Press, 2000.

    Google Scholar 

  3. A. Degtyarev and M. Fisher. Propositional temporal resolution revisited. In Proc. of 7th UK Workshop on Automated Reasoning (ARW), London, July 2000.

    Google Scholar 

  4. A. Degtyarev and M. Fisher. An Extension of Propositional Temporal Resolution. In Proc. UK Workshop on Automated Reasoning (ARW), York, March 2001.

    Google Scholar 

  5. A. Degtyarev and M. Fisher. Towards First-Order Temporal Resolution. In Proc. KI 2001, volume 2174 of LNCS. Springer Verlag, 2001.

    Google Scholar 

  6. R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning About Knowledge. MIT Press, 1996.

    Google Scholar 

  7. M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions on Computation Logic, 2(1), January 2001.

    Google Scholar 

  8. M. Fisher. A resolution method for temporal logic. In Proc. 12th Int. Joint Conf. on Artificial Intelligence (IJCAI). Morgan Kaufman, 1991.

    Google Scholar 

  9. M. Fisher. An introduction to executable temporal logics. Knowledge Engineering Review, 11:43–56, 1996.

    Article  Google Scholar 

  10. G. J. Holzmann. The Model Checker Spin. IEEE Trans. on Software Engineering, 23(5):279–295, May 1997. Special Issue on Formal Methods in Software Practice.

    Google Scholar 

  11. U. Hustadt and R. Schmidt. Scientific Benchmarking with Temporal Logic Decision Procedures Proc. Int. Conf. on Principles of Knowledge Representation & Reasoning, 2002.

    Google Scholar 

  12. U. Hustadt and R. Schmidt. Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers In Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Italy, 2001.

    Google Scholar 

  13. O. Kupferman and M. Vardi. Synthesis with incomplete informatio. In Advances in Temporal Logic. pp. 109–128. Kluwer, 2000.

    Google Scholar 

  14. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1992.

    Google Scholar 

  15. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symp. Princip. Prog. Lang., pp. 179–190, 1989.

    Google Scholar 

  16. A. S. Rao and M. P. Georgeff. Decision procedures for BDI logics. Journal of Logic and Computation, 8(3):293–342, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  17. M. P. Shanahan. Solving the Frame Problem. MIT Press, 1997.

    Google Scholar 

  18. A. Tansel, editor. Temporal Databases: theory, design, and implementation. Benjamin/Cummings, 1993.

    Google Scholar 

  19. G. Tseitin. On the complexity of derivations in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, 1968.

    Google Scholar 

  20. F. Wolter and M. Zakharyaschev. Temporalizing description logics. In Frontiers of Combining Systems II, pp. 379–401. Research Studies Press LTD, England, 2000.

    Google Scholar 

Download references

Author information

Author notes

  1. Boris Konev

    Present address: Steklov Institute of Mathematics at St.Petersburg, USA

Authors and Affiliations

  1. Logic and Computation Group, Department of Computer Science, University of Liverpool, Liverpool, L69 7ZF, UK

    Anatoli Degtyarev, Michael Fisher & Boris Konev

Authors
  1. Anatoli Degtyarev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Fisher
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Boris Konev
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Abteilung Wisssenbasierte Systeme 184/3, Technische Univesität Wien, Favoritenstr. 9-11, 1040, Vienna, Austria

    Uwe Egly

  2. Institut für Computersprachen AG Theoretische Informatik und Logik 185.2, Technische Universität Wien, Favoritenstr. 9-11, 1040, Vienna, Austria

    Chritian G. Fermüller

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Degtyarev, A., Fisher, M., Konev, B. (2002). A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. In: Egly, U., Fermüller, C.G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2002. Lecture Notes in Computer Science(), vol 2381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45616-3_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-45616-3_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43929-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation