Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Bolotov, Alexander; Grigoriev, Oleg; Shangin, Vasilyi
Publisher: IEEE
Languages: English
Types: Part of book or chapter of book
Subjects: UOW3

Classified by OpenAIRE into

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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [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 http://prover.philos.msu.ru.
    • [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.
    • [11] S. Jaskowski. On the rules of suppositions in formal logic. In Polish Logic 1920-1939, pages 232-258. Oxford Univ. Press, 1967.
    • [12] O. Lichtenstein and A. Pnueli. Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL, 8(1), 2000.
    • [13] V. Makarov. Automatic theorem-proving in intuitionistic propositional logic. In Modern Logic: Theory, History and Applications. Proceedings of the 5th Russian Conference, StPetersburg, 1998. (In Russian).
    • [14] F. Pfenning. Logical frameworks. In J. A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, chapter XXI, pages 1063-1147. Elsevier, 2001.
    • [15] W. Quine. On natural deduction. Journal of Symbolic Logic, 15:93-102, 1950.
    • [16] C. Renteria and E. Haeusler. Natural deduction for CTL. Bulletin of the Section of Logic, Polish Acad. of Sci., 31(4):231-240, 2002.
    • [17] A. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh, 1994.
    • [18] M. Wooldridge. Reasoning about Rational Agents. MIT Press, 2000.
  • No related research data.
  • No similar publications.

Share - Bookmark

Download from

Cite this article