# Reasoning about Intuitionistic Computation Tree Logic

arXiv: https://arxiv.org/abs/2310.02355 · HTML: https://mlsanity.com/paper/2310.02355/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 1 of its 16 references that are in the map.
- First posted on arXiv 3 Oct 2023.

## Builds on (most cited first, 1 of 1)

- [Intuitionistic Linear Temporal Logics](https://mlsanity.com/paper/1912.12893/) (2019)

## Abstract (arXiv)

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.