{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:08:43Z","timestamp":1748664523541,"version":"3.41.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_12","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"169-184","source":"Crossref","is-referenced-by-count":2,"title":["Ordered Resolution for Coalition Logic"],"prefix":"10.1007","author":[{"given":"Ullrich","family":"Hustadt","sequence":"first","affiliation":[]},{"given":"Paul","family":"Gainer","sequence":"additional","affiliation":[]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[]},{"given":"Cl\u00e1udia","family":"Nalon","sequence":"additional","affiliation":[]},{"given":"Lan","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"issue":"5","key":"12_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM\u00a049(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"12_CR2","unstructured":"Areces, C., Gennari, R., Heguiabehere, J., de Rijke, M.: Tree-Based heuristic in modal theorem proving. In: Proc. ECAI 2000. IOS Press (2000)"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-010-9167-0","volume":"46","author":"C. Areces","year":"2011","unstructured":"Areces, C., Gor\u00edn, D.: Resolution with order and selection for hybrid logics. J. of Automated Reasoning\u00a046, 1\u201342 (2011), doi:10.1007\/s10817-010-9167-0","journal-title":"J. of Automated Reasoning"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 19\u201399. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"12_CR5","unstructured":"Borgo, S.: Coalitions in action logic. In: Proc. IJCAI 2007, pp. 1822\u20131827 (2007)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-40537-2_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. David","year":"2013","unstructured":"David, A.: TATL: Implementation of ATL tableau-based decision procedure. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol.\u00a08123, pp. 97\u2013103. Springer, Heidelberg (2013)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"van Drimmelen, G.: Satisfiability in alternating-time temporal logic. In: Proc. LICS 2003, pp. 208\u2013207. IEEE (2003)","DOI":"10.1109\/LICS.2003.1210060"},{"key":"12_CR8","unstructured":"Gainer, P., Hustadt, U., Dixon, C.: CLProver++ (2015), http:\/\/cgi.csc.liv.ac.uk\/~ullrich\/CLProver++\/"},{"key":"12_CR9","unstructured":"Goranko, V.: Coalition games and alternating temporal logics. In: Proc. TARK 2001, pp. 259\u2013272. Morgan Kaufmann (2001)"},{"issue":"1","key":"12_CR10","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.tcs.2005.07.043","volume":"353","author":"V. Goranko","year":"2006","unstructured":"Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theor. Comput. Sci.\u00a0353(1), 93\u2013117 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"12_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1614431.1614434","volume":"11","author":"V. Goranko","year":"2009","unstructured":"Goranko, V., Shkatov, D.: Tableau-based decision procedures for logics of strategic ability in multiagent systems. ACM Trans. Comput. Log.\u00a011(1), 1\u201351 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR12","unstructured":"Hansen, H.H.: Tableau games for coalition logic and alternating-time temporal logic \u2013 theory and implementation. Master\u2019s thesis, University of Amsterdam, The Netherlands, October 2004"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.A.: Computational modal logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 181\u2013245. Elsevier (2006)","DOI":"10.1016\/S1570-2464(07)80007-3"},{"key":"12_CR14","unstructured":"Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Baaz, M., Makowsky, J., Voronkov, A. (eds.) Collegium Logicum, pp. 65\u201379. Kurt G\u00f6del Society (2004)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L. Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"issue":"4","key":"12_CR16","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1093\/logcom\/ext074","volume":"24","author":"C. Nalon","year":"2014","unstructured":"Nalon, C., Zhang, L., Dixon, C., Hustadt, U.: A resolution-based calculus for coalition logic. J. Logic Comput.\u00a024(4), 883\u2013917 (2014)","journal-title":"J. Logic Comput."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Nalon, C., Zhang, L., Dixon, C., Hustadt, U.: A resolution prover for coalition logic. In: Proc. SR2014. Electron. Proc. Theor. Comput. Sci., vol. 146, pp. 65\u201373 (2014)","DOI":"10.4204\/EPTCS.146.9"},{"key":"12_CR18","unstructured":"Pauly, M.: Logic for Social Software. Ph.D. thesis, University of Amsterdam, The Netherlands (2001)"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.\u00a02, 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-36675-8_3","volume-title":"Automated Reasoning and Mathematics","author":"S. Schulz","year":"2013","unstructured":"Schulz, S.: Simple and efficient clause subsumption with feature vector indexing. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol.\u00a07788, pp. 45\u201367. Springer, Heidelberg (2013)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 735\u2013743. Springer, Heidelberg (2013)"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-time temporal logic with explicit strategies. In: Proc. TARK 2007, pp. 269\u2013278. ACM (2007)","DOI":"10.1145\/1324249.1324285"},{"issue":"6","key":"12_CR23","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1093\/logcom\/exl009","volume":"16","author":"D. Walther","year":"2006","unstructured":"Walther, D., Lutz, C., Wolter, F., Wooldridge, M.: ATL satisfiability is indeed ExpTime-complete. J. Logic Comput.\u00a016(6), 765\u2013787 (2006)","journal-title":"J. Logic Comput."},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Zhang, L., Hustadt, U., Dixon, C.: A resolution calculus for branching-time temporal logic CTL. ACM Trans. Comput. Log. 15(1), 10:1\u201310:38 (2014)","DOI":"10.1145\/2529993"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T14:54:45Z","timestamp":1748616885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}