@article{Zhang+Hustadt+Dixon@ToCL2014,
 author    = {Lan Zhang and Ullrich Hustadt and Clare Dixon},
 title     = {A Resolution Calculus for Branching-Time Temporal Logic {CTL}},
 journal   = {ACM Transactions on Computational Logic},
 year      = {2014},
 month     = feb,
 volume    = {15},
 number    = {1},
 pages     = {10:1-38},
 url       = {http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf},
 abstract  = {The branching-time temporal logic CTL is useful for
 specifying systems that change over time and involve quantification
 over possible futures. Here we present a resolution calculus for CTL
 that involves the trans- lation of formulae to a normal form and the
 application of a number of resolution rules. We use indices in the
 normal form to represent particular paths and the application of the
 resolution rules is restricted dependent on an ordering and selection
 function to reduce the search space. We show that the translation
 preserves satisfiability, the calculus is sound, complete and
 terminating and consider the complexity of the calculus.}
}

{"_id":"bKLJZzhZeQcG9Cwgr","bibbaseid":"zhang-hustadt-dixon-aresolutioncalculusforbranchingtimetemporallogicctl-2014","author_short":["Zhang, L.","Hustadt, U.","Dixon, C."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Lan"],"propositions":[],"lastnames":["Zhang"],"suffixes":[]},{"firstnames":["Ullrich"],"propositions":[],"lastnames":["Hustadt"],"suffixes":[]},{"firstnames":["Clare"],"propositions":[],"lastnames":["Dixon"],"suffixes":[]}],"title":"A Resolution Calculus for Branching-Time Temporal Logic CTL","journal":"ACM Transactions on Computational Logic","year":"2014","month":"February","volume":"15","number":"1","pages":"10:1-38","url":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf","abstract":"The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the trans- lation of formulae to a normal form and the application of a number of resolution rules. We use indices in the normal form to represent particular paths and the application of the resolution rules is restricted dependent on an ordering and selection function to reduce the search space. We show that the translation preserves satisfiability, the calculus is sound, complete and terminating and consider the complexity of the calculus.","bibtex":"@article{Zhang+Hustadt+Dixon@ToCL2014,\n author = {Lan Zhang and Ullrich Hustadt and Clare Dixon},\n title = {A Resolution Calculus for Branching-Time Temporal Logic {CTL}},\n journal = {ACM Transactions on Computational Logic},\n year = {2014},\n month = feb,\n volume = {15},\n number = {1},\n pages = {10:1-38},\n url = {http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf},\n abstract = {The branching-time temporal logic CTL is useful for\n specifying systems that change over time and involve quantification\n over possible futures. Here we present a resolution calculus for CTL\n that involves the trans- lation of formulae to a normal form and the\n application of a number of resolution rules. We use indices in the\n normal form to represent particular paths and the application of the\n resolution rules is restricted dependent on an ordering and selection\n function to reduce the search space. We show that the translation\n preserves satisfiability, the calculus is sound, complete and\n terminating and consider the complexity of the calculus.}\n}\n\n\n\n","author_short":["Zhang, L.","Hustadt, U.","Dixon, C."],"key":"Zhang+Hustadt+Dixon@ToCL2014","id":"Zhang+Hustadt+Dixon@ToCL2014","bibbaseid":"zhang-hustadt-dixon-aresolutioncalculusforbranchingtimetemporallogicctl-2014","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["resolution","calculus","branching","time","temporal","logic","ctl","zhang","hustadt","dixon"],"title":"A Resolution Calculus for Branching-Time Temporal Logic CTL","year":2014}