@ARTICLE{Zhang+Hustadt+Dixon@AIC2010,
 AUTHOR  = {Zhang, Lan and Hustadt, Ullrich and Dixon, Clare},
 TITLE   = {{CTL-RP}: A computation tree logic resolution prover},
 JOURNAL = {AI Communications},
 VOLUME  = {23},
 NUMBER  = {2--3},
 PAGES   = {111-136},
 YEAR    = {2010},
 URL      = {http://iospress.metapress.com/content/x125544601352537/fulltext.pdf},
 ABSTRACT = {In this paper, we present a resolution-based calculus RCTL<sup>>,S</sup> for Computation Tree Logic (CTL) 
as well as an implementation of that calculus in the theorem prover CTL-RP. The calculus RCTL<sup>>,S</sup> 
requires a transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated
in an extension of CTL with indexed path formulae. The calculus itself consists of a set of resolution rules 
which can be used for an EXPTIME decision procedure for the satisfiability problem of CTL. We give a formal
semantics for the clausal normal form, provide proof sketches for the soundness and completeness of the 
resolution rules, discuss the complexity of the decision procedure based on RCTL<sup>>,S</sup>, and present 
an approach to implementing the calculus RCTL<sup>>,S</sup> using first-order techniques. Finally, we give 
a comparison between CTL-RP and a tableau theorem prover for CTL.}
}