@inproceedings{Zhang+Hustadt+Dixon@CADE2009,
author = {Lan Zhang and Ullrich Hustadt and Clare Dixon},
title = {A Refined Resolution Calculus for {CTL}},
pages = {245-260},
bibsource = {DBLP, http://dblp.uni-trier.de},
editor = {Renate A. Schmidt},
booktitle = {Proceedings of the 22nd International Conference
on Automated Deduction (CADE-22),
Montreal, Canada, August 2-7, 2009},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5663},
year = {2009},
isbn = {978-3-642-02958-5},
url = {http://dx.doi.org/10.1007/978-3-642-02959-2_20},
abstract = {In this paper, we present a refined resolution-based
calculus for Computation Tree Logic (CTL). The calculus requires a
polynomial time computable transformation of an arbitrary CTL formula
to an equi-satisfiable clausal normal form formulated in an extension
of CTL with indexed existential path quantifiers. The calculus itself
consists of a set of resolution rules which can be used as the basis
for an EXPTIME decision procedure for the satisfiability problem of
CTL. We prove soundness and completeness of the calculus. In addition,
we introduce CTL-RP, our implementation of the calculus as well as
some experimental results.}
}