{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:52:04Z","timestamp":1725796324293},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089690"},{"type":"electronic","value":"9783319089706"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08970-6_15","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T07:13:26Z","timestamp":1403939606000},"page":"226-241","source":"Crossref","is-referenced-by-count":4,"title":["Completeness and Decidability Results for CTL in Coq"],"prefix":"10.1007","author":[{"given":"Christian","family":"Doczkal","sequence":"first","affiliation":[]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)","key":"15_CR1"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1016\/j.jlap.2008.02.004","volume":"76","author":"K. Br\u00fcnnler","year":"2008","unstructured":"Br\u00fcnnler, K., Lange, M.: Cut-free sequent systems for temporal logic. J. Log. Algebr. Program.\u00a076(2), 216\u2013225 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-35308-6_18","volume-title":"Certified Programs and Proofs","author":"C. Doczkal","year":"2012","unstructured":"Doczkal, C., Smolka, G.: Constructive completeness for modal logic with transitive closure. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 224\u2013239. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Sematics (B), vol. B, pp. 995\u20131072. Elsevier (1990)","key":"15_CR5","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Programming"},{"issue":"1","key":"15_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. System Sci.\u00a030(1), 1\u201324 (1985)","journal-title":"J. Comput. System Sci."},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-74591-4_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Gonthier","year":"2007","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A modular formalisation of finite group theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 86\u2013101. Springer, Heidelberg (2007)"},{"unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Research Report RR-6455, INRIA (2008), \n \n http:\/\/hal.inria.fr\/inria-00258384\/en\/","key":"15_CR9"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-14203-1_21","volume-title":"Automated Reasoning","author":"M. Kaminski","year":"2010","unstructured":"Kaminski, M., Smolka, G.: Terminating tableaux for hybrid logic with eventualities. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 240\u2013254. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.: First-Order Logic. Springer (1968)","key":"15_CR11","DOI":"10.1007\/978-3-642-86718-7"},{"unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. Journal of Formalized Reasoning 2(1) (2009)","key":"15_CR12"},{"unstructured":"The Coq Development Team, \n \n http:\/\/coq.inria.fr","key":"15_CR13"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08970-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:09:25Z","timestamp":1558919365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08970-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089690","9783319089706"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08970-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}