{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:23:07Z","timestamp":1725531787665},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642012082"},{"type":"electronic","value":"9783642012099"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-01209-9_25","type":"book-chapter","created":{"date-parts":[[2009,5,4]],"date-time":"2009-05-04T16:58:23Z","timestamp":1241456303000},"page":"273-283","source":"Crossref","is-referenced-by-count":0,"title":["A Proof System for Projection Temporal Logic"],"prefix":"10.1007","author":[{"given":"Zhenhua","family":"Duan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinfeng","family":"Shu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Bledsoe, W., Loveland, D.: Automating Theorem Proving: After 25 Years. Amer Mathematical Society, USA (1984)","DOI":"10.1090\/conm\/029"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E., Emerson, E.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs, 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"25_CR3","unstructured":"Duan, Z.: An Extended Interval Temporal Logic and A Framing Technique for Interval Temporal Logic Programming. Ph.D Thesis, University of Newcastle Upon Tyne (May 1996)"},{"issue":"1","key":"25_CR4","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z. Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inf. 45(1), 43\u201378 (2008)","journal-title":"Acta Inf."},{"issue":"1","key":"25_CR5","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z. Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31\u201361 (2008)","journal-title":"Sci. Comput. Program."},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-540-88194-0_12","volume-title":"ICFEM 2008","author":"Z. Duan","year":"2008","unstructured":"Duan, Z., Tian, C.: A Unified Model Checking Approach with Projection Temporal Logic. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 167\u2013186. Springer, Heidelberg (2008)"},{"key":"25_CR7","first-page":"36","volume-title":"Proc. 10th LICS","author":"B. Dutertre","year":"1995","unstructured":"Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proc. 10th LICS, pp. 36\u201343. IEEE Computer Society, Los Alamitos (1995)"},{"issue":"2","key":"25_CR8","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1093\/logcom\/14.2.215","volume":"14","author":"D.P. Guelev","year":"2004","unstructured":"Guelev, D.P.: A Complete Proof System for First-order Interval Temporal Logic with Projection. Journal of Logic and Computation\u00a014(2), 215\u2013249 (2004)","journal-title":"Journal of Logic and Computation"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: A Complete Proof Systems for QPTL. In: LICS 1995, pp. 2\u201312 (1995)","DOI":"10.1109\/LICS.1995.523239"},{"key":"25_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publisher, Dordrecht (1993)"},{"key":"25_CR11","volume-title":"Executing temporal logic programs","author":"B. Moszkowski","year":"1986","unstructured":"Moszkowski, B.: Executing temporal logic programs. Cambridge University Press, Cambridge (1986)"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.: A complete axiomatization of interval temporal logic with infinite time. In: LICS 2000, pp. 241\u2013252 (2000)","DOI":"10.1109\/LICS.2000.855773"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-76650-6_15","volume-title":"Formal Methods and Software Engineering","author":"C. Tian","year":"2007","unstructured":"Tian, C., Duan, Z.: Model Checking Propositional Projection Temporal Logic Based on SPIN. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol.\u00a04789, pp. 246\u2013265. Springer, Heidelberg (2007)"}],"container-title":["Studies in Computational Intelligence","Computer and Information Science 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-01209-9_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T09:58:56Z","timestamp":1619776736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-01209-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642012082","9783642012099"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-01209-9_25","relation":{},"ISSN":["1860-949X","1860-9503"],"issn-type":[{"type":"print","value":"1860-949X"},{"type":"electronic","value":"1860-9503"}],"subject":[],"published":{"date-parts":[[2009]]}}}