Title :
Automated Natural Deduction for Propositional Linear-Time Temporal Logic
Author :
Bolotov, Alexander ; Grigoriev, Oleg ; Shangin, Vasilyi
Author_Institution :
Univ. of Westminster, Harrow
Abstract :
We present a proof searching technique for the natural deduction calculus for the prepositional 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.
Keywords :
temporal logic; temporal reasoning; theorem proving; AI application; automated natural deduction; automated reasoning; computer science application; deliberative decision making framework; natural deduction calculus; prepositional linear-time temporal logic; proof searching technique; Application software; Artificial intelligence; Automation; Calculus; Computer science; Decision making; Logic; Neodymium; Protocols; Security;
Conference_Titel :
Temporal Representation and Reasoning, 14th International Symposium on
Conference_Location :
Alicante
Print_ISBN :
978-0-7695-2836-6
DOI :
10.1109/TIME.2007.41
