@inproceedings{8130ad56028f493294e41b562979ac9b,
title = "A refined resolution calculus for CTL",
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.",
author = "L. Zhang and U. Hustadt and C. Dixon",
year = "2009",
doi = "10.1007/978-3-642-02959-2_20",
language = "English",
isbn = "978-3-642-02958-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "245--260",
booktitle = "Automated Deduction – CADE-22",
address = "United States",
note = "22nd International Conference on Automated Deduction, CADE-22 ; Conference date: 02-08-2009 Through 07-08-2009",
}