直觉主义计算树逻辑中的安全性和活性
来源：计算机科学与探索杂志2016年第2期北京时间：
作者：鲍秋霜，张晋津
单位：1. 南京航空航天大学 计算机科学与技术学院，南京 2100162. 南京审计学院 计算机科学与技术系，南京 211815
摘要：将Patrick Maier关于直觉主义线性时序逻辑的研究扩展到计算树逻辑中，基于完全树和非完全树构成的集合提出了一种直觉主义解释的计算树逻辑，并在此逻辑框架中研究了安全性和活性及其相关性质。比较了经典计算树逻辑与直觉主义计算树逻辑的表达能力，探究了直觉主义计算树逻辑中安全性和活性在并、交等操作下的封闭性以及与经典计算树逻辑中安全性和活性的关系，并为直觉主义计算树逻辑公式建立了分解定理。
关键词：直觉主义,计算树逻辑,安全性,活性,分解定理
