In this paper, we define an intuitionistic version of Computation Tree Logic. After explaining the semantic features of intuitionistic logic, we examine how these characteristics can be interesting for formal verification purposes. Subsequently, we define the syntax and semantics of our intuitionistic version of CTL and study some simple properties of the so obtained logic. We conclude by demonstrating that some fixed-point axioms of CTL are not valid in the intuitionistic version of CTL we have defined.

翻译：本文定义了直觉主义版本的计算树逻辑。在阐释直觉主义逻辑的语义特征后，我们探讨了这些特性如何对形式验证具有重要价值。随后，我们给出了直觉主义CTL的语法和语义定义，并研究了该逻辑的一些简单性质。最后，我们证明了CTL的某些不动点公理在我们定义的直觉主义CTL版本中并不成立。