Abstract: This paper makes an extension from the intuitionistic linear time logic of Patrick Maier to computation tree logic, proposes an intuitionistic computation tree logic based on the set constructed by total and non-total tree, and considers safety and livenss in this intuitionistic computation tree logic. This paper also compares the expressive power between classical computation tree logic and intuitionistic computation tree logic, explores some properties of safety and liveness in intuitionistic computation tree logic under disjunction and conjunction, and discusses the relationship between intuitionistic computation tree logic and classical computation tree logic. Besides, this paper builds the decomposition theorem for formulas of intuitionistic computation tree logic.

Key words: intuitionistic, computation tree logic, safety, liveness, decomposition theorem

摘要： 将Patrick Maier关于直觉主义线性时序逻辑的研究扩展到计算树逻辑中，基于完全树和非完全树构成的集合提出了一种直觉主义解释的计算树逻辑，并在此逻辑框架中研究了安全性和活性及其相关性质。比较了经典计算树逻辑与直觉主义计算树逻辑的表达能力，探究了直觉主义计算树逻辑中安全性和活性在并、交等操作下的封闭性以及与经典计算树逻辑中安全性和活性的关系，并为直觉主义计算树逻辑公式建立了分解定理。

关键词: 直觉主义, 计算树逻辑, 安全性, 活性, 分解定理