Automating natural deduction for linear-time temporal logic

Part of book or chapter of book English OPEN
Bolotov, Alexander ; Grigoriev, Oleg ; Shangin, Vasilyi
  • Publisher: IEEE
  • Related identifiers: doi: 10.1109/TIME.2007.41
  • Subject: UOW3

We present a proof searching technique for the natural\ud deduction calculus for the propositional linear-time temporal logic and prove its correctness. This opens the prospect to apply our technique as an automated reasoning tool in a number of emerging computer science applications and in a deliberative decision making framework across various AI applications.
  • References (18)
    18 references, page 1 of 2

    [1] D. Basin, S. Matthews, and L. Vigano` . Natural deduction for non-classical logics. Studia Logica, 60(1):119-160, 1998.

    [2] A. Bolotov, A. Basukoski, O. Grigoriev, and V. Shangin. Natural deduction calculus for linear-time temporal logic. In Joint European Conference on Artificial Intelligence (JELIA-2006), pages 56-68, 2006.

    [3] A. Bolotov, V. Bocharov, A. Gorchakov, V. Makarov, and V. Shangin. Let Computer Prove It. Logic and Computer. Nauka, Moscow, 2004. (In Russian), Implementation of the proof search technique for classical propositional logic available on-line at

    [4] A. Bolotov, V. Bocharov, A. Gorchakov, and V. Shangin. Automated first order natural deduction. In Proceedings of IICAI, pages 1292-1311, 2005.

    [5] A. Bolotov, O. Grigoriev, and V. Shangin. Natural deduction calculus for computation tree logic. In IEEE John Vincent Atanasoff Symposium on Modern Computing, pages 175-183, 2006.

    [6] E. Clarke, S. Jha, and W. R. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, pages 87-96, June 1998.

    [7] M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions on Computational Logic (TOCL), 1(2):12-56, 2001.

    [8] F. Fitch. Symbolic Logic. NY: Roland Press, 1952.

    [9] D. Gabbay, A. Phueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proceedings of 7th ACM Symposium on Principles of Programming Languages, pages 163-173, Las Vegas, Nevada, 1980.

    [10] A. Indrzejczak. A labelled natural deduction system for linear temporal logic. Studia Logica, 75(3):345- 376, 2004.

  • Metrics
    No metrics available
Share - Bookmark