Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computational Logic

CL 2000: Computational Logic — CL 2000 pp 523–537Cite as

On an ω-Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL

  • Conference paper
  • First Online:

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

Abstract

A new deduction-based procedure is presented for non-Horn, so-called DR-sequents with repetitions of a restricted first-order linear temporal logic with temporal operators “next” and “always”. The main part of the proposed deductive procedure is automatic generation of the inductive hypothesis. The proposed deductive procedure consists of three separate decidable deductive procedures replacing the infinitary omega-type rule for the operator “always”. These three decidable parts cannot be joined. Therefore the proposed deductive procedure (by analogy with ω-completeness) is only ω-decidable. The specific shape of DR-sequents allows us in all the three parts of the proposed deductive procedure to construct: (1) a deduction tree in some linear form, i.e., with one ”temporal” branch; (2) length-preserving derivations, i.e., the lengths of generated sequents are the same.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi M.: The power of temporal proofs. Theoretical Comp. Sci. 64 (1989) 35–84.

    Article  MathSciNet  Google Scholar 

  2. Fisher M.: A normal form for temporal logics and its applications in theorem proving and execution. Journal of Logic and Computation 7(4) (1997).

    Google Scholar 

  3. Fisher M., Wooldridge M.: On the formal specification and verification of multi-agent systems. Intern. Journal of Cooperative Information Systems 6(1) (1997) 37–65.

    Article  Google Scholar 

  4. Hodkinson I., Wolter F., Zakharyaschev M.: Decidable fragments of first-order temporal logics. (To appear in: Annals of Pure and Applied Logic).

    Google Scholar 

  5. Kawai H.: Sequential calculus for a first-order infinitary temporal logic. Zeitchr. fur Math. Logic und Grundlagen der Math. 33 (1987) 423–452.

    Article  MATH  MathSciNet  Google Scholar 

  6. Pliuškevičius R.: The saturated tableaux for a linear miniscoped Horn-like temporal logic. Journal of Automated Reasoning 13 (1994) 51–67.

    Google Scholar 

  7. Pliuškevičius R.: Replacement of induction by similarity saturation in a first-order linear temporal logic. Journal of Applied Non-Classical Logics 8(1–2) (1998) 141–169.

    MathSciNet  MATH  Google Scholar 

  8. Pliuškevičius R.: Infinitary calculus for a restricted first-order linear temporal logic without contraction of quantified formulas. Lithuanian Mathematical Journal 39(3) (1999) 378–397.

    MathSciNet  Google Scholar 

  9. Pliuškevičius R.: An effective deductive procedure for a restricted first-order linear temporal logic. (Submitted to Annals of Pure and Applied Logic).

    Google Scholar 

  10. Szalas A.: Concerning the semantic consequence relation in first-order temporal logic. Theoretical Comput. Sci. 47 (1986) 329–334.

    Article  MATH  MathSciNet  Google Scholar 

  11. Szalas A.: A complete axiomatic characterization of first-order temporal logic of linear time. Theoretical Comput. Sci. 54 (1987) 199–214.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics and Informatics, Akademijos 4, Vilnius, 2600, Lithuania

    Regimantas Pliuškevičius

Authors
  1. Regimantas Pliuškevičius
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. The Australian National University, Australia

    John Lloyd

  2. Simon Fraser University, Canada

    Veronica Dahl

  3. Universität Koblenz, Germany

    Ulrich Furbach

  4. The University of Birmingham, UK

    Manfred Kerber

  5. University of Manchester, UK

    Kung-Kiu Lau

  6. The Pennsylvania State University, USA

    Catuscia Palamidessi

  7. Universidade Nova de Lisboa, Portugal

    Luís Moniz Pereira

  8. The Hebrew University of Jerusalem, Israel

    Yehoshua Sagiv

  9. The University of Melbourne, Australia

    Peter J. Stuckey

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pliuškevičius, R. (2000). On an ω-Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL. In: Lloyd, J., et al. Computational Logic — CL 2000. CL 2000. Lecture Notes in Computer Science(), vol 1861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44957-4_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-44957-4_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67797-0

  • Online ISBN: 978-3-540-44957-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation