{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:51Z","timestamp":1725664491242},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593386"},{"type":"electronic","value":"9783540492351"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59338-1_36","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:13:47Z","timestamp":1330276427000},"page":"185-200","source":"Crossref","is-referenced-by-count":2,"title":["Specifications of inference rules and their automatic translation"],"prefix":"10.1007","author":[{"given":"Gerd","family":"Neugebauer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Petermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Peter Baumgartner and Ulrich Furbach. Model elimination without contrapositives. In Alan Bundy, editor, CADE-12, volume LNCS 814, pages 87\u2013101. Springer Verlag, 1994.","key":"13_CR1","DOI":"10.1007\/3-540-58156-1_7"},{"doi-asserted-by":"crossref","unstructured":"G\u00e9rard Becher and Uwe Petermann. Rigid E-unification by completion and rigid paramodulation. In Bernhard Nebel and Leonie Dreschler-Fischer, editors, KI-94: Advances in Artificial Intelligence, volume LNAI 861, pages 319\u2013330. Springer Verlag, 1994.","key":"13_CR2","DOI":"10.1007\/3-540-58467-6_28"},{"doi-asserted-by":"crossref","unstructured":"Bernhardt Beckert. A completion-based method for mixed universal and rigid E-unification. In Alan Bundy, editor, CADE-12, volume LNCS 814, pages 678\u2013692. Springer Verlag, 1994.","key":"13_CR3","DOI":"10.1007\/3-540-58156-1_49"},{"doi-asserted-by":"crossref","unstructured":"Wolfgang Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.","key":"13_CR4","DOI":"10.1007\/978-3-322-90102-6"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving theorems with the modification method. SIAM Journal of Computation, 4:412\u2013430, 1975.","journal-title":"SIAM Journal of Computation"},{"doi-asserted-by":"crossref","unstructured":"Thierry Boy de la Tour. Minimizing the number of clauses by renaming. In Mark E. Stickel, editor, CADE-10, volume LNCS 449, pages 558\u2013572. Springer Verlag, July 1990.","key":"13_CR6","DOI":"10.1007\/3-540-52885-7_114"},{"doi-asserted-by":"crossref","unstructured":"J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Theorem proving with equational matings and rigid E-unification. Journal of the ACM, 1992.","key":"13_CR7","DOI":"10.1145\/128749.128754"},{"unstructured":"Jean Goubault. A rule-based algorithm for rigid E-unification. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, 3rd Kurt G\u00f6del Colloquium '93, volume 713 of LNCS. Springer Verlag, 1993.","key":"13_CR8"},{"doi-asserted-by":"crossref","unstructured":"Xiaorong Huang, Manfred Kerber, Michael Kohlhase, et al. KEIM: A toolkit for automated deduction. In Alan Bundy, editor, CADE-12, volume LNAI 814, pages 807\u2013810. Springer Verlag, 1994.","key":"13_CR9","DOI":"10.1007\/3-540-58156-1_65"},{"unstructured":"Gerd Neugebauer and Torsten Schaub. A pool-based connection calculus. In C. Boz\u015fahin, U. Halici, K. Oflazar, and N. Yalabik, editors, Proceedings of Third Turkish Symposium on Artificial Intelligence and Neural Networks, pages 297\u2013306. Middle East Technical University Press, 1994.","key":"13_CR10"},{"doi-asserted-by":"crossref","unstructured":"Uwe Petermann. Completeness of the pool calculus with an open built in theory. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, 3rd Kurt G\u00f6del Colloquium '93, volume LNCS 713. Springer Verlag, 1993.","key":"13_CR11","DOI":"10.1007\/BFb0022576"},{"unstructured":"Uwe Petermann. A theory connection calculus with positive refinement. NTZ-Report 25\/93, NTZ der Universit\u00e4t Leipzig, 1993.","key":"13_CR12"},{"unstructured":"Uwe Petermann. A complete connection calculus with rigid Eunification. In JELIA94, volume LNCS 838, pages 152\u2013167. Springer Verlag, 1994.","key":"13_CR13"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/BF00244355","volume":"6","author":"D. A. Plaisted","year":"1990","unstructured":"David A. Plaisted. A sequent-style model elimination strategy and a positive refinement. J. Automated Reasoning, 6:389\u2013402, 1990.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"13_CR15","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. H. Siekmann","year":"1989","unstructured":"J\u00f6rg H. Siekmann. Unification theory. J. Symbolic Computation, 7(1):207\u2013274, January 1989.","journal-title":"J. Symbolic Computation"},{"issue":"1","key":"13_CR16","first-page":"333","volume":"4","author":"M.E. Stickel","year":"1985","unstructured":"M.E. Stickel. Automated deduction by theory resolution. J. Automated Reasoning, 4(1):333\u2013356, 1985.","journal-title":"J. Automated Reasoning"},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Mark E. Stickel. A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. J. Automated Reasoning, 4:353\u2013380, 1988.","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59338-1_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:26:52Z","timestamp":1605648412000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59338-1_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593386","9783540492351"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-59338-1_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}