Skip to main content
SpringerLink
Log in
Book cover

International Conference on Knowledge-Based and Intelligent Information and Engineering Systems

KES 2010: Knowledge-Based and Intelligent Information and Engineering Systems pp 224–233Cite as

Reasoning and Inference Rules in Basic Linear Temporal Logic \(\mathcal{BLTL}\)

  • Conference paper

  • 1575 Accesses

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

Abstract

Our paper studies a formalization of reasoning in basic linear temporal logic \(\mathcal{BLTL}\) in terms of admissible inference rules. The paper contains necessary preliminary information and description of new evolved technique allowing by a sequence of mathematical lemmas to get our main result. Main result is found explicit basis for rules admissible in \(\mathcal{BLTL}\) (which, in particular, allows to compute admissible rules).

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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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. Artemov, S., Iemhoff, R.: The basic intuitionistic logic of proofs. Journal of Symbolic Logic 72(2), 439–451 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  2. Blok, W., Pigozzi, D.: Algebraizable logics. Mem. Amer. Math. Soc., vol. 396. AMS, Providence (1989)

    Google Scholar 

  3. Barringer, H., Fisher, M., Gabbay, D., Gough, G.: Advances in Temporal Logic. Applied logic series, vol. 16. Kluwer Academic Publishers, Dordrecht (1999)

    Google Scholar 

  4. van Benthem, J.: The Logic of Time. Kluwer, Dordrecht (1991)

    MATH  Google Scholar 

  5. Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at ltl model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)

    Google Scholar 

  6. Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  7. Friedman, H.: One hundred and two problems in mathematical logic. Journal of Symbolic Logic 40(3), 113–130 (1975)

    MathSciNet  MATH  Google Scholar 

  8. Fritz, C.: Constructing büchi automata from linear temporal logic using simulation relations for alternating büchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 163–173. ACM, New York (1980), doi: http://doi.acm.org/10.1145/567446.567462

    Chapter  Google Scholar 

  10. Goldblatt, R.: Logics of time and computation. Center for the Study of Language and Information, Stanford (1987)

    MATH  Google Scholar 

  11. Goranko, V., Passy, S.: Using the universal modality: Gains and questions. Journal of Logic and Computation 2, 5–30 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  12. Ghilardi, S.: Unification in intuitionistic logic. J. Symb. Log. 64(2), 859–880 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  13. Ghilardi, S.: Unification through projectivity. J. Log. Comput. 7(6), 733–752 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  14. Ghilardi, S.: Best solving modal equations. Ann. Pure Appl. Logic 102(3), 183–198 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  15. Ghilardi, S.: A resolution/tableaux algorithm for projective approximations in ipc. Logic Journal of the IGPL 10(3), 229–243 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  16. Ghilardi, S.: Unification, finite duality and projectivity in varieties of heyting algebras. Ann. Pure Appl. Logic 127(1-3), 99–115 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Harrop, R.: Concerning formulas of the types \(a\to b\vee c,\ a \to \exists x b(x)\). Journal of Symbolic Logic 25(1), 27–32 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  18. Iemhoff, R.: On the admissible rules of intuitionistic propositional logic. J. Symb. Log. 66(1), 281–294 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  19. Iemhoff, R.: Intermediate logics and visser’s rules. Notre Dame Journal of Formal Logic 46(1), 65–81 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  20. Iemhoff, R., Metcalfe, G.: Proof theory for admissible rules. Ann. Pure Appl. Logic 159(1-2), 171–186 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  21. Iemhoff, R., Metcalfe, G.: Hypersequent systems for the admissible rules of modal and intermediate logics. In: Artëmov, S.N., Nerode, A. (eds.) LFCS. LNCS, vol. 5407, pp. 230–245. Springer, Heidelberg (2009)

    Google Scholar 

  22. Jerábek, E.: Independent bases of admissible rules. Logic Journal of the IGPL 16(3), 249–267 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  23. Jeřábek, E.: Admissible rules of modal logics. J. Log. and Comput. 15(4), 411–431 (2005), doi: http://dx.doi.org/10.1093/logcom/exi029

    Article  MATH  Google Scholar 

  24. Jerábek, E.: Complexity of admissible rules. Arch. Math. Log. 46(2), 73–92 (2007)

    Article  MATH  Google Scholar 

  25. Jeřábek, E.: Admissible rules of Łukasiewicz logic. Journal of Logic and Computation (accepted)

    Google Scholar 

  26. Jeřábek, E.: Bases of admissible rules of Łukasiewicz logic. Journal of Logic and Computation (accepted)

    Google Scholar 

  27. Kröger, F.: Temporal logic of programs. Springer, New York (1987)

    MATH  Google Scholar 

  28. Kröger, F., Merz, S.: Temporal Logic and State Systems, Texts in Theoretical Computer Science. EATCS Series. Springer, Heidelberg (2008)

    Google Scholar 

  29. Kapron, B.: Modal sequents and definability. Journal of Symbolic Logic 52(3), 756–765 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  30. Lange, M.: A quick axiomatisation of ltl with past. Math. Log. Q. 51(1), 83–88 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  31. Lorenzen, P.: Einfuerung in Operative Logik und Mathematik. Springer, Heidelberg (1955)

    Google Scholar 

  32. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)

    Google Scholar 

  33. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)

    Google Scholar 

  34. Metcalfe, G.: Proof theory for Casari’s comparative logics. J. Log. Comput. 16(4), 405–422 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  35. Metcalfe, G., Olivetti, N.: Proof systems for a gödel modal logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 265–279. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  36. Mints, G.: Derivability of admissible rules. Journal of Soviet Mathematics 6(4), 417–421 (1976)

    Article  MATH  Google Scholar 

  37. Rybakov, V.: A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic. Algebra and Logica 23(5), 369–384 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  38. Rybakov, V.: Rules of inference with parameters for intuitionistic logic. Journal of Symbolic Logic 57(3), 912–923 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  39. Rybakov, V.: Admissible Logical Inference Rules. Studies in Logic and the Foundations of Mathematics, vol. 136. Elsevier Sci. Publ./North-Holland (1997)

    Google Scholar 

  40. Rybakov, V.: The bases for admissible rules of logics s4 and int. Algebra and Logic 24, 55–68 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  41. Rybakov, V.: Construction of an explicit basis for rules admissible in modal system S4. Mathematical Logic Quarterly 47(4), 441–451 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  42. Rybakov, V.: Logical consecutions in discrete linear temporal logic. Journal of Symbolic Logic 70(4), 1137–1149 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  43. Rybakov, V.V.: Multi-modal and temporal logics with universal formula - reduction of admissibility to validity and unification. J. Log. Comput. 18(4), 509–519 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  44. Rybakov, V.V.: Linear temporal logic with until and next, logical consecutions. Ann. Pure Appl. Logic 155(1), 32–45 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  45. Rozière, P.: Admissible and derivable rules in intuitionistic logic. Mathematical Structures in Computer Science 3(2), 129–136 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  46. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  47. Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Banff Higher Order Workshop, pp. 238–266 (1995), http://citeseer.ist.psu.edu/vardi96automatatheoretic.html

  48. Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing and Mathematics, Manchester Metropolitan University, John Dalton Building, Chester Street, Manchester, M1 5GD, U.K.

    S. Babenyshev & V. Rybakov

  2. Institute of Mathematics, Siberian Federal University, 79 Svobodny Prospect, Krasnoyarsk, 660041, Russia

    S. Babenyshev & V. Rybakov

Authors
  1. S. Babenyshev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. V. Rybakov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Engineering, The Parade, Cardiff University, CF24 3AA, Cardiff, UK

    Rossitza Setchi

  2. Dept. of Computer Science and Software Engineering, BUckingham Building, Lion Terrace, University of Portsmouth, PO1 3HE, Portsmouth, UK

    Ivan Jordanov

  3. KES International, 145-157 St. John Street, EC1V 4PY, London, UK

    Robert J. Howlett

  4. School of Electrical and Information Engineering, University of South Australia, Adelaide, Mawson Lakes Campus, 5095, SA, Australia

    Lakhmi C. Jain

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Babenyshev, S., Rybakov, V. (2010). Reasoning and Inference Rules in Basic Linear Temporal Logic \(\mathcal{BLTL}\) . In: Setchi, R., Jordanov, I., Howlett, R.J., Jain, L.C. (eds) Knowledge-Based and Intelligent Information and Engineering Systems. KES 2010. Lecture Notes in Computer Science(), vol 6277. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15390-7_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15390-7_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15389-1

  • Online ISBN: 978-3-642-15390-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation