{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:07:48Z","timestamp":1725487668143},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660866"},{"type":"electronic","value":"9783540487548"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48754-9_25","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:20:56Z","timestamp":1184588456000},"page":"293-307","source":"Crossref","is-referenced-by-count":1,"title":["Full First-Order Free Variable Sequents and Tableaux in Implicit Induction"],"prefix":"10.1007","author":[{"given":"Claus-Peter","family":"Wirth","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,11]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Matthias Baaz, Uwe Egly, Christian G. Ferm\u00fcller (1997). Lean Induction Principles for Tableaux. 6thTABLEAUX1997, LNAI1227, pp. 62\u201375, Springer.","DOI":"10.1007\/BFb0027405"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair (1988). Proof By Consistency in Equational Theories. 3rd IEEE symposium on Logic In Computer Sci., pp. 228\u2013233, IEEE Press.","DOI":"10.1109\/LICS.1988.5122"},{"key":"25_CR3","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0004-3702(96)00042-2","volume":"90","author":"P. Baumgartner","year":"1997","unstructured":"Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg (1997). Computing Answers with Model Elimination. Artificial Intelligence 90, pp. 135\u2013176.","journal-title":"Artificial Intelligence"},{"key":"25_CR4","unstructured":"Herbert B. Enderton (1973). A Mathematical Introduction to Logic. Academic Press."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Melvin Fitting (1996). First-Order Logic and Automated Theorem Proving. 2nd extd. ed., Springer.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"25_CR6","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gerhard Gentzen (1935). Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift 39, pp. 176\u2013210, 405\u2013431.","journal-title":"Mathematische Zeitschrift"},{"key":"25_CR7","unstructured":"Alfons Geser (1995). A Principle of Non-Wellfounded Induction. In: Tiziana Margaria (ed.): Kolloquium Programmiersprachen und Grundlagen der Programmierung, MIP-9519, pp. 117\u2013124, Univ. Passau."},{"key":"25_CR8","unstructured":"Ulrich K\u00fchler (1999). A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Dissertation (Ph.D. thesis), Univ. Kaiserslautern, to appear."},{"key":"25_CR9","series-title":"Lect Notes Comput Sci","first-page":"38","volume-title":"Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving","author":"U. K\u00fchler","year":"1996","unstructured":"Ulrich K\u00fchler, Claus-Peter Wirth (1996). Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. SEKI-Report SR-96-11, FB Informatik, Univ. Kaiserslautern. Short version in: 8th RTA 1997, LNCS 1232, pp. 38\u201352, Springer."},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1006\/jsco.1996.0003","volume":"21","author":"P. Padawitz","year":"1996","unstructured":"Peter Padawitz (1996). Inductive Theorem Proving for Design Specifications. J. Symbolic Computation 21, pp. 41\u201399, Academic Press.","journal-title":"J. Symbolic Computation"},{"key":"25_CR11","unstructured":"Dag Prawitz (1960). An Improved Proof Procedure. In: Siekmann & Wrightson (1983), Vol. 1, pp. 159\u2013199."},{"key":"25_CR12","unstructured":"Herman Rubin, Jean E. Rubin (1985). Equivalents of the Axiom of Choice. Elsevier."},{"key":"25_CR13","unstructured":"J\u00f6rg Siekmann, G. Wrightson (eds.) (1983). Automation of Reasoning. Springer."},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Raymond M. Smullyan (1968). First-Order Logic. Springer.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"25_CR15","volume-title":"Positive\/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving","author":"C.-P. Wirth","year":"1997","unstructured":"Claus-Peter Wirth (1997). Positive\/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving. Dissertation (Ph.D. thesis), Verlag Dr. Kova\u010d, Hamburg."},{"key":"25_CR16","unstructured":"Claus-Peter Wirth (1998). Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized \u03b4-Rule but Without Skolemization. Report 698\/1998, FB Informatik, Univ. Dortmund. Short version in: Gernot Salzer, Ricardo Caferra (eds.). Proc. 2nd Int. Workshop on First-Order Theorem Proving (FTP), pp. 244\u2013255, Vienna, 1998. Also submitted for LNCS version, Springer, 1999."},{"key":"25_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-60381-6_21","volume-title":"4thCTRS1994","author":"C.-P. Wirth","year":"1995","unstructured":"Claus-Peter Wirth, Klaus Becker (1995). Abstract Notions and Inference Systems for Proofs by Mathematical Induction. 4thCTRS1994, LNCS968, pp. 353\u2013373, Springer."},{"key":"25_CR18","unstructured":"Claus-Peter Wirth, Bernhard Gramlich (1994). On Notions of Inductive Validity for First-Order Equational Clauses. 12thCADE1994, LNAI814, pp. 162\u2013176, Springer."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48754-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T19:34:00Z","timestamp":1550432040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48754-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660866","9783540487548"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48754-9_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}