{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:12:38Z","timestamp":1746072758508,"version":"3.40.4"},"publisher-location":"Wiesbaden","reference-count":20,"publisher":"Vieweg+Teubner Verlag","isbn-type":[{"type":"print","value":"9783815420331"},{"type":"electronic","value":"9783322952332"}],"license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/978-3-322-95233-2_27","type":"book-chapter","created":{"date-parts":[[2013,4,17]],"date-time":"2013-04-17T05:17:04Z","timestamp":1366175824000},"page":"441-461","source":"Crossref","is-referenced-by-count":3,"title":["Inductive Theorem Proving by Consistency for First-Order Clauses"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Stuber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","first-page":"228","volume-title":"Proc. 3rd IEEE Symp. on Logic in Computer Science","author":"L Bachmair","year":"1988","unstructured":"Leo Bachmair. Proof by consistency in equational theories. In Proc. 3rd IEEE Symp. on Logic in Computer Science, pages 228\u2013233, Edinburgh, July 1988."},{"key":"27_CR2","volume-title":"Proc. 10th Int. Conf. on Automated Deduction","author":"L Bachmair","year":"1990","unstructured":"Leo Bachmair and Harald Ganzinger. On restrictions of ordered paramodulation with simplification. In Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, July 1990. Springer LNCS 449."},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. Completion of first-order clauses with equality by strict superposition. In Proc. 2nd Int. Workshop on Conditional and Typed Rewriting Systems, Montreal, June 1990. Springer LNCS 516.","DOI":"10.1007\/3-540-54317-1_89"},{"key":"27_CR4","volume-title":"Proc. 8th Int. Conf. on Logic Programming","author":"L Bachmair","year":"1991","unstructured":"Leo Bachmair and Harald Ganzinger. Perfect model semantics for logic programs with equality. In Proc. 8th Int. Conf. on Logic Programming. MIT Press, 1991."},{"key":"27_CR5","series-title":"Technical Report MPI-I-91\u2013208","volume-title":"Rewrite-based equational theorem proving with selection and simplification","author":"L Bachmair","year":"1991","unstructured":"Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Technical Report MPI-I-91\u2013208, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, August 1991."},{"key":"27_CR6","first-page":"516","volume-title":"Proc. 2nd Int. Workshop on Conditional and Typed Rewriting Systems","author":"E Bevers","year":"1990","unstructured":"Eddy Bevers and Johan Lewi. Proof by consistency in conditional equational theories. In Proc. 2nd Int. Workshop on Conditional and Typed Rewriting Systems, Montreal, June 1990. Springer LNCS 516."},{"key":"27_CR7","volume-title":"A Computational Logic","author":"R Boyer","year":"1979","unstructured":"Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, New York, 1979."},{"key":"27_CR8","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-52885-7_84","volume-title":"Proc. 10th Int. Conf. on Automated Deduction","author":"A Bundy","year":"1990","unstructured":"A. Bundy, F. van Harmelen, A. Smail, and A. Ireland. Extensions to the rippling-out tactic for guiding inductive proofs. In Proc. 10th Int. Conf. on Automated Deduction, pages 132\u2013146, Kaiserslautern, July 1990. Springer LNCS 449."},{"key":"27_CR9","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/3-540-16761-7_60","volume-title":"In Proc. 13th Int. Coll. on Automata, Languages and Programming","author":"L Fribourg","year":"1986","unstructured":"Laurent Fribourg. A strong restriction of the inductive completion procedure. In Proc. 13th Int. Coll. on Automata, Languages and Programming, pages 105\u2013115, Rennes, France, July 1986. Springer LNCS 226."},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"H. Ganzinger and R. Sch\u00e4fers. System support for modular order-sorted Horn clause specifications. Proc. 12th Int. Conf. on Software Engineering, Nice, pages 150\u2013163, 1990.","DOI":"10.1109\/ICSE.1990.63618"},{"key":"27_CR11","first-page":"219","volume-title":"Proc. 15th Annual ACM Symp. on Principles of Programming Languages","author":"SJ Garland","year":"1988","unstructured":"Stephen J. Garland and John V. Guttag. Inductive methods for reasoning about abstract data types. In Proc. 15th Annual ACM Symp. on Principles of Programming Languages, pages 219\u2013228, San Diego, January 1988."},{"key":"27_CR12","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G Huet","year":"1982","unstructured":"G\u00e9rard Huet and Jean-Marie Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25:239\u2013266, 1982.","journal-title":"Journal of Computer and System Sciences"},{"key":"27_CR13","first-page":"358","volume-title":"Proc. Symp. on Logic in Computer Science","author":"J-P Jouannaud","year":"1986","unstructured":"Jean-Pierre Jouannaud and Emmanuel Kounalis. Proofs by induction in equa-tional theories without constructors. In Proc. Symp. on Logic in Computer Science, pages 358\u2013366, Cambridge, Mass., June 1986."},{"key":"27_CR14","first-page":"32","volume":"28","author":"S Kaplan","year":"1986","unstructured":"Stephane Kaplan and Marianne Choquer. On the decidability of quasi-reducibility. EATCS Bulletin, 28:32\u201334, 1986.","journal-title":"EATCS Bulletin"},{"key":"27_CR15","first-page":"154","volume-title":"Proc. 7th Annual ACM Symp. on Principles of Programming Languages","author":"R David","year":"1980","unstructured":"David R. Musser. On proving inductive properties of abstract data types. In Proc. 7th Annual ACM Symp. on Principles of Programming Languages, pages 154\u2013162, Las Vegas, January 1980."},{"key":"27_CR16","unstructured":"Fernando Orejas. Theorem proving in conditional-equational theories. Draft."},{"issue":"1","key":"27_CR17","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00249354","volume":"7","author":"P Padawitz","year":"1991","unstructured":"Peter Padawitz. Inductive expansion: A calculus for verifying and synthesizing functional and logic programs. Journal of Automated Reasoning, 7(1):27\u2013103, March 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR18","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"A David","year":"1985","unstructured":"David A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182\u2013215, 1985.","journal-title":"Information and Control"},{"key":"27_CR19","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/B978-0-934613-40-8.50009-9","volume-title":"Foundations of Deductive Data Bases and Logic Programming","author":"TC Przymusinski","year":"1988","unstructured":"T. C. Przymusinski. On the declarative semantics of deductive databases and logic programs. In J. Minker, editor, Foundations of Deductive Data Bases and Logic Programming, pages 193\u2013216. Morgan Kaufmann Publishers, Los Altos, 1988."},{"key":"27_CR20","volume-title":"Master\u2019s thesis, Universit\u00e4t Dortmund","author":"J Stuber","year":"1991","unstructured":"J\u00fcrgen Stuber. Inductive theorem proving for horn clauses. Master\u2019s thesis, Universit\u00e4t Dortmund, April 1991."}],"container-title":["TEUBNER-TEXTE zur Informatik","Informatik"],"original-title":[],"language":"de","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-322-95233-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T05:08:35Z","timestamp":1745989715000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-322-95233-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783815420331","9783322952332"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-322-95233-2_27","relation":{},"ISSN":["1615-4584"],"issn-type":[{"type":"print","value":"1615-4584"}],"subject":[],"published":{"date-parts":[[1992]]}}}