Skip to main content
SpringerLink
Log in

Fair Derivations in Monodic Temporal Reasoning

  • Conference paper
Automated Deduction – CADE-22 (CADE 2009)

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

Included in the following conference series:

Abstract

Ordered fine-grained resolution with selection is a sound and complete resolution-based calculus for monodic first-order temporal logic. The inference rules of the calculus are based on standard resolution between different types of temporal clauses on one hand and inference rules with semi-decidable applicability conditions that handle eventualities on the other hand. In this paper we illustrate how the combination of these two different types of inference rules can lead to unfair derivations in practice. We also present an inference procedure that allows us to construct fair derivations and prove its refutational completeness. We conclude with some experimental results obtained with the implementation of the new procedure in the theorem prover TSPASS.

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. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 19–99. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  2. Behdenna, A., Dixon, C., Fisher, M.: Deductive verification of simple foraging robotic behaviours (under review)

    Google Scholar 

  3. Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 397–411. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. ACM Transactions On Computational Logic 7(1), 108–150 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  5. Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, pp. 995–1072 (1990)

    Google Scholar 

  6. Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic 2(1), 12–56 (2001)

    Article  MathSciNet  Google Scholar 

  7. Gago, M.C.F., Fisher, M., Dixon, C.: Algorithms for guiding clausal temporal resolution. In: Jarke, M., Koehler, J., Lakemeyer, G. (eds.) KI 2002. LNCS, vol. 2479, pp. 235–252. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable fragments of first-order temporal logics. Annals of Pure and Applied Logic 106, 85–134 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  9. Hustadt, U., Konev, B., Riazanov, A., Voronkov, A.: TeMP: A temporal monodic prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 326–330. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Hustadt, U., Konev, B., Schmidt, R.A.: Deciding monodic fragments by temporal resolution. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 204–218. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.: Towards the implementation of first-order temporal resolution: the expanding domain case. In: Proc. TIME-ICTL 2003, pp. 72–82. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  12. Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.: Mechanising first-order temporal resolution. Information and Computation 199(1-2), 55–86 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  13. Ludwig, M., Hustadt, U.: Implementing a fair monodic temporal logic prover. AI Communications (to appear)

    Google Scholar 

  14. Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: System description: SPASS version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 514–520. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Wolter, F., Zakharyaschev, M.: Axiomatizing the monodic fragment of first-order temporal logic. Annals of Pure and Applied logic 118, 133–145 (2002)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Liverpool, United Kingdom

    Michel Ludwig & Ullrich Hustadt

Authors
  1. Michel Ludwig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ullrich Hustadt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, The University of Manchester, Manchester, UK

    Renate A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ludwig, M., Hustadt, U. (2009). Fair Derivations in Monodic Temporal Reasoning. In: Schmidt, R.A. (eds) Automated Deduction – CADE-22. CADE 2009. Lecture Notes in Computer Science(), vol 5663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02959-2_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02959-2_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02958-5

  • Online ISBN: 978-3-642-02959-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation