학술논문
Natural Deduction Calculus for Computation Tree Logic
Document Type
Conference
Author
Source
IEEE John Vincent Atanasoff 2006 International Symposium on Modern Computing (JVA'06) Modern Computing, 2006. JVA '06. IEEE John Vincent Atanasoff 2006 International Symposium on. :175-183 Oct, 2006
Subject
Language
Abstract
We 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.