{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:28:06Z","timestamp":1759638486216,"version":"3.40.3"},"publisher-location":"Cham","reference-count":8,"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_14","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"214-228","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Deciding $$\\mathsf {ATL^*}$$ Satisfiability by Tableaux"],"prefix":"10.1007","author":[{"given":"Am\u00e9lie","family":"David","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"5","key":"14_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 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-319-08587-6_21","volume-title":"Automated Reasoning","author":"S Cerrito","year":"2014","unstructured":"Cerrito, S., David, A., Goranko, V.: Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic ATL+. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 277\u2013291. Springer, Heidelberg (2014). http:\/\/arxiv.org\/abs\/1407.4645"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/978-3-319-08587-6_36","volume-title":"Automated Reasoning","author":"D Carral","year":"2014","unstructured":"Carral, D., Feier, C., Cuenca Grau, B., Hitzler, P., Horrocks, I.: $$\\cal EL$$-ifying ontologies. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 464\u2013479. Springer, Heidelberg (2014)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logics. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995\u20131072. MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"3","key":"14_CR5","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"EA Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf. Control 61(3), 175\u2013201 (1984)","journal-title":"Inf. Control"},{"issue":"1","key":"14_CR6","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. 11(1), 1\u201348 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: A faster tableau for CTL. In: Puppis, G., Villa, T. (eds.) Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2013, Borca di Cadore, Dolomites, Italy, 29\u201331th August 2013. EPTCS, vol. 119, pp. 50\u201363 (2013). http:\/\/dx.doi.org\/10.4204\/EPTCS.119.7","DOI":"10.4204\/EPTCS.119.7"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-540-70583-3_31","volume-title":"Automata, Languages and Programming","author":"S Schewe","year":"2008","unstructured":"Schewe, S.: ATL* satisfiability Is 2EXPTIME-complete. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 373\u2013385. Springer, Heidelberg (2008)"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T13:25:55Z","timestamp":1676467555000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_14","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"}}]}}