Abstract
We present a natural deduction calculus for the propositional linear-time temporal logic and prove its correctness. The system extends the natural deduction construction of the classical propositional logic. This will open the prospect to apply our technique as an automatic reasoning tool in a deliberative decision making framework across various AI applications.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Ganzinger, H.: A theory of resolution. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2. Elsevier, Amsterdam (2001)
Bolotov, A., Bocharov, V., Gorchakov, A., Makarov, V., Shangin, V.: Let Computer Prove It. In: Logic and Computer, Nauka, Moscow (2004) (in Russian)
Bolotov, A., Bocharov, V., Gorchakov, A., Shangin, V.: Automated first order natural deduction. In: Proceedings of IICAI, pp. 1292–1311 (2005)
Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic (TOCL) 1(2), 12–56 (2001)
Fitch, F.: Symbolic Logic. Roland Press, New York (1952)
Fitting, M.: First-Order Logic and Automated Theorem-Proving. Springer, Berlin (1996)
Gabbay, D., Phueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of 7th ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, pp. 163–173 (1980)
Gentzen, G.: Investigation into logical deduction. In: The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1969)
Jaskowski, S.: On the rules of suppositions in formal logic. In: Polish Logic 1920-1939, pp. 232–258. Oxford University Press, Oxford (1967)
Makarov, V.: Automatic theorem-proving in intuitionistic propositional logic. In: Modern Logic: Theory, History and Applications. Proceedings of the 5th Russian Conference, St Petersburg (1998) (in Russian)
Marchignoli, D.: Natural Deduction Systems for Temporal Logic. PhD thesis, Department of Informatics, Unviersity of Pisa (2002)
Pfenning, F.: Logical frameworks. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. XXI, pp. 1063–1147. Elsevier, Amsterdam (2001)
Polakow, J., Pfenning, F.: Natural deduction for intuitionistic non-commutative linear logic. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 295–309. Springer, Heidelberg (1999)
Quine, W.: On natural deduction. Journal of Symbolic Logic 15, 93–102 (1950)
Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh (1994)
Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bolotov, A., Basukoski, A., Grigoriev, O., Shangin, V. (2006). Natural Deduction Calculus for Linear-Time Temporal Logic. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds) Logics in Artificial Intelligence. JELIA 2006. Lecture Notes in Computer Science(), vol 4160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11853886_7
Download citation
DOI: https://doi.org/10.1007/11853886_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-39625-3
Online ISBN: 978-3-540-39627-7
eBook Packages: Computer ScienceComputer Science (R0)