{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:31:37Z","timestamp":1759638697109},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642390708"},{"type":"electronic","value":"9783642390715"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39071-5_15","type":"book-chapter","created":{"date-parts":[[2013,6,23]],"date-time":"2013-06-23T21:23:17Z","timestamp":1372022597000},"page":"192-207","source":"Crossref","is-referenced-by-count":9,"title":["Experiments with Reduction Finding"],"prefix":"10.1007","author":[{"given":"Charles","family":"Jordan","sequence":"first","affiliation":[]},{"given":"\u0141ukasz","family":"Kaiser","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1137\/S0097539794270236","volume":"26","author":"E. Allender","year":"1997","unstructured":"Allender, E., Balc\u00e1zar, J.L., Immerman, N.: A first-order isomorphism theorem. SIAM J. Comput.\u00a026(2), 539\u2013556 (1997)","journal-title":"SIAM J. Comput."},{"issue":"5","key":"15_CR2","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-642-15025-8_10","volume-title":"Fields of Logic and Computation","author":"M. Crouch","year":"2010","unstructured":"Crouch, M., Immerman, N., Moss, J.E.B.: Finding reductions automatically. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol.\u00a06300, pp. 181\u2013200. Springer, Heidelberg (2010)"},{"issue":"3-4","key":"15_CR4","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01536399","volume":"15","author":"T. Eiter","year":"1995","unstructured":"Eiter, T., Gottlob, G.: On the computational cost of disjunctive logic programming: Propositional case. Annals of Mathematics and Artificial Intelligence\u00a015(3-4), 289\u2013323 (1995)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"15_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11546207_19","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"W. Faber","year":"2005","unstructured":"Faber, W., Ricca, F.: Solving hard ASP programs efficiently. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol.\u00a03662, pp. 240\u2013252. Springer, Heidelberg (2005)"},{"key":"15_CR6","unstructured":"Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. In: Complexity of Computation, SIAM-AMS Proceedings, vol.\u00a07, pp. 43\u201373. Amer. Mathematical Soc. (1974)"},{"issue":"5","key":"15_CR7","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/S0019-9958(67)91165-5","volume":"10","author":"E. Gold","year":"1967","unstructured":"Gold, E.: Language identification in the limit. Inform. Control\u00a010(5), 447\u2013474 (1967)","journal-title":"Inform. Control"},{"key":"15_CR8","unstructured":"Gr\u00e4del, E., Kolaitis, P.G., Libkin, L., Marx, M., Spencer, J., Vardi, M.Y., Venema, Y., Weinstein, S.: Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. Springer (2007)"},{"key":"15_CR9","unstructured":"Grohe, M.: Fixed-point logics on planar graphs. In: Proc. of LICS 1998, pp. 6\u201315. IEEE Computer Society (1998)"},{"issue":"5","key":"15_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2371656.2371662","volume":"59","author":"M. Grohe","year":"2012","unstructured":"Grohe, M.: Fixed-point definability and polynomial time on graphs with excluded minors. J. ACM 59(5), 27:1\u201327:64 (2012)","journal-title":"J. ACM"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/S0019-9958(86)80029-8","volume":"68","author":"N. Immerman","year":"1986","unstructured":"Immerman, N.: Relational queries computable in polynomial time. Inform. Control\u00a068, 86\u2013104 (1986)","journal-title":"Inform. Control"},{"issue":"4","key":"15_CR12","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1137\/0216051","volume":"16","author":"N. Immerman","year":"1987","unstructured":"Immerman, N.: Languages that capture complexity classes. SIAM J. Comput.\u00a016(4), 760\u2013778 (1987)","journal-title":"SIAM J. Comput."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Immerman, N.: Descriptive Complexity. Springer (1999)","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M. Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 114\u2013128. Springer, Heidelberg (2012)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-21581-0_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M. Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 230\u2013244. Springer, Heidelberg (2011)"},{"issue":"3","key":"15_CR16","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1145\/1149114.1149117","volume":"7","author":"N. Leone","year":"2006","unstructured":"Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic\u00a07(3), 499\u2013562 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-14186-7_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"C. Peschiera","year":"2010","unstructured":"Peschiera, C., Pulina, L., Tacchella, A., Bubeck, U., Kullmann, O., Lynce, I.: The seventh QBF solvers evaluation (QBFEVAL\u201910). In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 237\u2013250. Springer, Heidelberg (2010)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: The complexity of relational query languages. In: Proc. of STOC 1982, pp. 137\u2013146. ACM (1982)","DOI":"10.1145\/800070.802186"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2013"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39071-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:39:45Z","timestamp":1558301985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39071-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390708","9783642390715"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}