|Chapter title||Natural deduction calculus for computation tree logic|
|Authors||Bolotov, A., Grigoriev, O. and Shangin, V.|
The authors present a natural deduction calculus for the computation tree logic, CTL, defined with the full set of classical and temporal logic operators. The system extends the natural deduction construction of the linear-time temporal logic. This opens the prospect to apply our technique as an automatic reasoning tool in a deliberative decision making framework across various applications in AI and computer science, where the branching-time setting is required.
|Keywords||Decision making, inference mechanisms, process algebra, temporal logic, artificial intelligence, automatic reasoning tool, branching-time setting, classical logic operators, computation tree logic, computer science, decision making, natural deduction calculus, temporal logic operators|
|Book title||IEEE John Vincent Atanasoff 2006 International Symposium on Modern Computing (JVA'06)|
|Place of publication||Los Alamitos, USA|
|Digital Object Identifier (DOI)||https://doi.org/10.1109/JVA.2006.34|