@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.} 
}

{"_id":"RGdBPYprY2X2fWaEL","bibbaseid":"zhang-hustadt-dixon-arefinedresolutioncalculusforctl-2009","author_short":["Zhang, L.","Hustadt, U.","Dixon, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Lan"],"propositions":[],"lastnames":["Zhang"],"suffixes":[]},{"firstnames":["Ullrich"],"propositions":[],"lastnames":["Hustadt"],"suffixes":[]},{"firstnames":["Clare"],"propositions":[],"lastnames":["Dixon"],"suffixes":[]}],"title":"A Refined Resolution Calculus for CTL","pages":"245-260","bibsource":"DBLP, http://dblp.uni-trier.de","editor":[{"firstnames":["Renate","A."],"propositions":[],"lastnames":["Schmidt"],"suffixes":[]}],"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.","bibtex":"@inproceedings{Zhang+Hustadt+Dixon@CADE2009,\n author = {Lan Zhang and Ullrich Hustadt and Clare Dixon},\n title = {A Refined Resolution Calculus for {CTL}},\n pages = {245-260},\n bibsource = {DBLP, http://dblp.uni-trier.de},\n editor = {Renate A. Schmidt},\n booktitle = {Proceedings of the 22nd International Conference\n on Automated Deduction (CADE-22),\n\t Montreal, Canada, August 2-7, 2009},\n publisher = {Springer},\n series = {Lecture Notes in Computer Science},\n volume = {5663},\n year = {2009},\n isbn = {978-3-642-02958-5},\n url = {http://dx.doi.org/10.1007/978-3-642-02959-2_20},\n abstract = {In this paper, we present a refined resolution-based\n calculus for Computation Tree Logic (CTL). The calculus requires a\n polynomial time computable transformation of an arbitrary CTL formula\n to an equi-satisfiable clausal normal form formulated in an extension\n of CTL with indexed existential path quantifiers. The calculus itself\n consists of a set of resolution rules which can be used as the basis\n for an EXPTIME decision procedure for the satisfiability problem of\n CTL. We prove soundness and completeness of the calculus. In addition,\n we introduce CTL-RP, our implementation of the calculus as well as\n some experimental results.} \n}\n\n","author_short":["Zhang, L.","Hustadt, U.","Dixon, C."],"editor_short":["Schmidt, R. A."],"key":"Zhang+Hustadt+Dixon@CADE2009","id":"Zhang+Hustadt+Dixon@CADE2009","bibbaseid":"zhang-hustadt-dixon-arefinedresolutioncalculusforctl-2009","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/978-3-642-02959-2_20"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["refined","resolution","calculus","ctl","zhang","hustadt","dixon"],"title":"A Refined Resolution Calculus for CTL","year":2009}