CTL-RP: A computation tree logic resolution prover
Lan Zhang, Ullrich Hustadt, Clare Dixon · AI Communications · 2010
In this paper, we present a resolution-based calculus RCTL >,S for Computation Tree Logic (CTL) as well as an implementation of that calculus in the theorem prover CTL-RP. The calculus RCTL >,S requires a transformation of an arbitrary CTL form