|Chapter title||Automating natural deduction for linear-time temporal logic|
|Authors||Bolotov, A., Grigoriev, O. and Shangin, V.|
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.
|Book title||14th International Symposium on Temporal Representation and Reasoning (TIME'07)), 28-30 June 2007, Alicante, Spain|
|Place of publication||Los Alamitos, USA|
|Digital Object Identifier (DOI)||https://doi.org/10.1109/TIME.2007.41|
|Web address (URL)||http://doi.ieeecomputersociety.org/10.1109/TIME.2007.41|