{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:30:09Z","timestamp":1743139809680,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319488684"},{"type":"electronic","value":"9783319488691"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48869-1_13","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T03:41:52Z","timestamp":1478490112000},"page":"166-180","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Resolution in Solving Graph Problems"],"prefix":"10.1007","author":[{"given":"Kailiang","family":"Ji","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"13_CR1","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). doi:\n                    10.1007\/978-3-642-15205-4_15"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 6803, pp. 162\u2013176. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-22438-6_14"},{"key":"13_CR3","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 (1999)"},{"issue":"1","key":"13_CR4","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/0890-5401(90)90043-H","volume":"85","author":"B Courcelle","year":"1990","unstructured":"Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12\u201375 (1990)","journal-title":"Inf. Comput."},{"key":"13_CR5","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. IAICT, vol. 323, pp. 182\u2013196. Springer, Heidelberg (2010). doi:\n                    10.1007\/978-3-642-15240-5_14"},{"key":"13_CR6","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":"13_CR7","unstructured":"Dowek, G., Jiang, Y.: Axiomatizing Truth in a Finite Model (2013). \n                    https:\/\/hal.inria.fr\/hal-00919469\/document"},{"key":"13_CR8","unstructured":"Navarro-P\u00e9rez, J.A.: Encoding and solving problems in effectively propositional logic. Ph.D. thesis, The University of Manchester (2007)"},{"issue":"4","key":"13_CR9","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1145\/321662.321678","volume":"18","author":"R Reiter","year":"1971","unstructured":"Reiter, R.: Two results on ordering for resolution with merging and linear format. J. ACM (JACM) 18(4), 630\u2013646 (1971)","journal-title":"J. ACM (JACM)"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"189","DOI":"10.2307\/2272384","volume":"39","author":"JA Robinson","year":"1974","unstructured":"Robinson, J.A.: Automatic deduction with hyper-resolution. J. Symbolic Logic 39(1), 189\u2013190 (1974)","journal-title":"J. Symbolic Logic"},{"issue":"1","key":"13_CR11","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM (JACM) 12(1), 23\u201341 (1965)","journal-title":"J. ACM (JACM)"},{"issue":"11","key":"13_CR12","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1145\/355611.362538","volume":"16","author":"JR Slagle","year":"1973","unstructured":"Slagle, J.R., Norton, L.M.: Experiment with an automatic theorem-prover having partial ordering inference rules. Commun. ACM 16(11), 682\u2013688 (1973)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48869-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T22:23:27Z","timestamp":1558477407000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48869-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319488684","9783319488691"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48869-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}