{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:32:55Z","timestamp":1742995975806,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_20","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"295-310","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["CTL Model Checking in Deduction Modulo"],"prefix":"10.1007","author":[{"given":"Kailiang","family":"Ji","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15205-4_15","volume-title":"Computer Science Logic","author":"G Burel","year":"2010","unstructured":"Burel, G.: Embedding deduction modulo into a prover. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 155\u2013169. Springer, Heidelberg (2010)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22438-6_14","volume-title":"Automated Deduction \u2013 CADE-23","author":"G Burel","year":"2011","unstructured":"Burel, G.: Experimenting with deduction modulo. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 162\u2013176. Springer, Heidelberg (2011)"},{"key":"20_CR4","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA, USA (1999)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-45221-5_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Delahaye","year":"2013","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon modulo: when Achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 274\u2013290. Springer, Heidelberg (2013)"},{"key":"20_CR6","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-15240-5_14","volume-title":"Theoretical Computer Science","author":"G Dowek","year":"2010","unstructured":"Dowek, G.: Polarized resolution modulo. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol. 323, pp. 182\u2013196. Springer, Heidelberg (2010)"},{"key":"20_CR7","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. reasoning 31, 33\u201372 (2003)","journal-title":"J. Autom. reasoning"},{"key":"20_CR8","unstructured":"Dowek, G., Jiang, Y.: A Logical Approach to CTL (2013). http:\/\/hal.inria.fr\/docs\/00\/91\/94\/67\/PDF\/ctl.pdf (manuscript)"},{"key":"20_CR9","unstructured":"Dowek, G., Jiang, Y.: Axiomatizing Truth in a Finite Model (2013). https:\/\/who.rocq.inria.fr\/Gilles.Dowek\/Publi\/classes.pdf (manuscript)"},{"key":"20_CR10","unstructured":"Ji, K.: CTL Model Checking in Deduction Modulo. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25, 2015. LNCS, vol. 9195, pp. xx\u2013yy (2015). https:\/\/drive.google.com\/file\/d\/0B0CYADxmoWB5UGJsV2UzNnVqVHM\/view?usp=sharing (fullpaper)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"20_CR12","series-title":"LNCS","first-page":"84","volume-title":"CAV 1995","author":"S Rajan","year":"1995","unstructured":"Rajan, S., Shankar, N., Srivas, M.: An Integration of Model Checking with Automated Proof Checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 84\u201397. Springer, Berlin Heidelberg (1995)"},{"key":"20_CR13","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, New York (1996)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-10373-5_15","volume-title":"Formal Methods and Software Engineering","author":"W Zhang","year":"2009","unstructured":"Zhang, W.: Bounded semantics of CTL and SAT-based verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 286\u2013305. Springer, Heidelberg (2009)"},{"key":"20_CR15","unstructured":"Zhang, W.: VERDS Modeling Language (2012). http:\/\/lcs.ios.ac.cn\/~zwh\/verds\/index.html"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/978-3-319-08587-6_16","volume-title":"Automated Reasoning","author":"W Zhang","year":"2014","unstructured":"Zhang, W.: QBF encoding of temporal properties and QBF-based verification. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 224\u2013239. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T17:32:30Z","timestamp":1675272750000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}