Automated Natural Deduction for Propositional Linear-Time Temporal Logic

We present a proof searching technique for the natural 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.

• Type: Conference
• Year: 2007
• Where: TIME
• Authors: Alexander Bolotov, Oleg Grigoriev, Vasilyi Shangin
• Keywords: Linear-time Temporal Logic, Logical Reasoning, Natural Deduction Calculus, Proof Searching Technique, TIME 2007