{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:19:43Z","timestamp":1725567583749},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_14","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T12:51:59Z","timestamp":1286196719000},"page":"187-201","source":"Crossref","is-referenced-by-count":3,"title":["On the Complexity of the Bernays-Sch\u00f6nfinkel Class with Datalog"],"prefix":"10.1007","author":[{"given":"Witold","family":"Charatonik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Witkowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-540-69738-1_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2007","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis of single-parent heaps. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 91\u2013105. Springer, Heidelberg (2007)"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-642-00596-1_30","volume-title":"Programming Languages and Systems","author":"K. Bansal","year":"2009","unstructured":"Bansal, K., Brochenin, R., Lozes, E.: Beyond shapes: Lists with ordered data. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 425\u2013439. Springer, Heidelberg (2009)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A. Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. LNCS, vol.\u00a05710, pp. 178\u2013195. Springer, Heidelberg (2009)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/11538363_28","volume-title":"Computer Science Logic","author":"W. Charatonik","year":"2005","unstructured":"Charatonik, W., Georgieva, L., Maier, P.: Bounded model checking of pointer programs. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 397\u2013412. Springer, Heidelberg (2005)"},{"key":"14_CR5","unstructured":"Charatonik, W., Witkowski, P.: On the complexity of the Bernays-Sch\u00f6nfinkel class with datalog. Full version, http:\/\/www.ii.uni.wroc.pl\/~pwit\/BSD-full.pdf"},{"key":"14_CR6","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/3-540-13331-3_48","volume-title":"Proceedings of the Symposium \u201dRekursive Kombinatorik\u201d on Logic and Machines: Decision Problems and Complexity","author":"M. F\u00fcrer","year":"1984","unstructured":"F\u00fcrer, M.: The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In: Proceedings of the Symposium \u201dRekursive Kombinatorik\u201d on Logic and Machines: Decision Problems and Complexity, London, UK, pp. 312\u2013319. Springer, London (1984)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BFb0023464","volume-title":"STACS 97","author":"E. Gr\u00e4del","year":"1997","unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 249\u2013260. Springer, Heidelberg (1997)"},{"key":"14_CR8","first-page":"306","volume-title":"LICS 1997: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science","author":"E. Graedel","year":"1997","unstructured":"Graedel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: LICS 1997: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, p. 306. IEEE Computer Society, Los Alamitos (1997)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pp. 267\u2013281 (1982)","DOI":"10.1145\/800070.802201"},{"key":"14_CR11","first-page":"171","volume-title":"POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"S. Lahiri","year":"2008","unstructured":"Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 171\u2013182. ACM Press, New York (2008)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The general vector addition system reachability problem by presburger inductive invariants. In: LICS 2009: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, pp. 4\u201313 (2009)","DOI":"10.1109\/LICS.2009.10"},{"key":"14_CR13","unstructured":"Lipton, R.J.: The Reachability Problem Requires Exponential Space, Technical Report 62, Yale University, Department of Computer Science (January 1976)"},{"issue":"3","key":"14_CR14","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"E.W. Mayr","year":"1984","unstructured":"Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput.\u00a013(3), 441\u2013460 (1984)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"14_CR15","doi-asserted-by":"publisher","first-page":"292","DOI":"10.2307\/2318455","volume":"80","author":"B.O. Nas","year":"1973","unstructured":"Nas, B.O.: Reachability problems in vector addition systems. The American Mathematical Monthly\u00a080(3), 292\u2013295 (1973)","journal-title":"The American Mathematical Monthly"},{"key":"14_CR16","first-page":"318","volume-title":"LICS 1997: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science","author":"L. Pacholski","year":"1997","unstructured":"Pacholski, L., Szwast, W., Tendera, L.: Complexity of two-variable logic with counting. In: LICS 1997: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, p. 318. IEEE Computer Society, Los Alamitos (1997)"},{"issue":"4","key":"14_CR17","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1137\/S0097539797323005","volume":"29","author":"L. Pacholski","year":"2000","unstructured":"Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first-order two-variable logic with counting. SIAM J. Comput.\u00a029(4), 1083\u20131117 (2000)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"14_CR18","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10849-005-5791-1","volume":"14","author":"I. Pratt-Hartmann","year":"2005","unstructured":"Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. J. of Logic, Lang. and Inf.\u00a014(3), 369\u2013395 (2005)","journal-title":"J. of Logic, Lang. and Inf."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. Journal of Logic and Algebraic Programming\u00a073(1-2), 111\u2013142 (2007)","DOI":"10.1016\/j.jlap.2006.12.001"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T06:01:58Z","timestamp":1559714518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}