{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:53:38Z","timestamp":1725537218705},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_25","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T13:27:52Z","timestamp":1252934872000},"page":"332-347","source":"Crossref","is-referenced-by-count":9,"title":["Deciding the Inductive Validity of \u2200\u2009\u2203\u2009* Queries"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"25_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"25_CR2","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A.: Automated theorem proving by test set induction. Journal of Symbolic Computation\u00a023(1), 47\u201377 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Bouhoula, A., Jouannaud, J.-P.: Automata-driven automated induction. In: Information and Computation, Warsaw, Poland, pp. 14\u201325 (1997) (press)","DOI":"10.1109\/LICS.1997.614920"},{"issue":"6","key":"25_CR4","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Caferra, R., Zabel, N.: A method for simultanous search for refutations and models by equational constraint solving. J. Symb. Comp.\u00a013(6), 613\u2013642 (1992)","journal-title":"J. Symb. Comp."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Clark, K.L.: Negation as failure. In: Logic and Data Bases, pp. 293\u2013322 (1977)","DOI":"10.1007\/978-1-4684-3384-5_11"},{"issue":"3-4","key":"25_CR6","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation\u00a07(3-4), 371\u2013425 (1989)","journal-title":"Journal of Symbolic Computation"},{"issue":"1\/2","key":"25_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-axiomatization + first-order consistency. Information and Computation\u00a0159(1\/2), 151\u2013186 (2000)","journal-title":"Information and Computation"},{"key":"25_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/11916277_4","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Falke","year":"2006","unstructured":"Falke, S., Kapur, D.: Inductive decidability using implicit induction. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 45\u201359. Springer, Heidelberg (2006)"},{"key":"25_CR9","first-page":"295","volume-title":"Proc. 14th IEEE Symposium on Logic in Computer Science","author":"H. Ganzinger","year":"1999","unstructured":"Ganzinger, H., Nivelle, H.D.: A superposition decision procedure for the guarded fragment with equality. In: Proc. 14th IEEE Symposium on Logic in Computer Science, pp. 295\u2013305. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-56393-8_17","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1993","unstructured":"Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 226\u2013241. Springer, Heidelberg (1993)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-87531-4_22","volume-title":"Computer Science Logic","author":"M. Horbach","year":"2008","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 293\u2013307. Springer, Heidelberg (2008)"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Horbach, M., Weidenbach, C.: Deciding the inductive validity of \u2200 \u2203* queries. Research Report MPI\u2013I\u20132009\u2013RG1\u2013001, Max-Planck Institute for Informatics, Saarbr\u00fccken, Germany (May 2009)","DOI":"10.1007\/978-3-642-04027-6_25"},{"issue":"1\/2","key":"25_CR13","first-page":"81","volume":"11","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. Journal of Symbolic Computation\u00a011(1\/2), 81\u2013111 (1991)","journal-title":"Journal of Symbolic Computation"},{"issue":"1-2","key":"25_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0747-7171(03)00028-2","volume":"36","author":"N. Peltier","year":"2003","unstructured":"Peltier, N.: Model building with ordered resolution: extracting models from saturated clause sets. Journal of Symbolic Computation\u00a036(1-2), 5\u201348 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"25_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-32275-7_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Seidl","year":"2005","unstructured":"Seidl, H., Verma, K.N.: Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 79\u201394. Springer, Heidelberg (2005)"},{"key":"25_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 27, vol.\u00a02, pp. 1965\u20132012. Elsevier, Amsterdam (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T11:19:28Z","timestamp":1558523968000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}