{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:18:41Z","timestamp":1725455921923},"publisher-location":"Berlin\/Heidelberg","reference-count":18,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055873X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013841","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:24:11Z","timestamp":1132730651000},"page":"420-434","source":"Crossref","is-referenced-by-count":5,"title":["Theorem proving for hierarchic first-order theories"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","unstructured":"Leo Bachmair and Harald Ganzinger, 1991a. Perfect Model Semantics for Logic Programs with Equality. In Proc. ICLP'91, pp. 645\u2013659. MIT Press."},{"key":"27_CR2","volume-title":"Technical Report MPI-I-91-208","author":"L. Bachmair","year":"1991","unstructured":"Leo Bachmair and Harald Ganzinger, 1991b. Rewrite-Based Equational Theorem Proving With Selection and Simplification. Technical Report MPI-I-91-208, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. Revised version to appear in Journal of Logic and Computation."},{"key":"27_CR3","first-page":"5","volume-title":"Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, vol. 90","author":"J. Barwise","year":"1977","unstructured":"Jon Barwise, 1977. An Introduction to First-Order Logic. In Jon Barwise, editor, Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, vol. 90, chapter A.1, pp. 5\u201346. North-Holland Publishing Company, Amsterdam, New York, Oxford."},{"key":"27_CR4","first-page":"193","volume-title":"LNCS 118","author":"J. A. Bergstra","year":"1981","unstructured":"J[an] A. Bergstra, M[anfred] Broy, J[ohn] V. Tucker and M[artin] Wirsing, 1981. On the Power of Algebraic Specifications. In Jozef Gruska, Michal Chytil, editors, Mathematical Foundations of Computer Science, 10th Symposium, LNCS 118, pp. 193\u2013204, \u0160trebsk\u00e9 Pleso, Czechoslovakia, Springer-Verlag."},{"key":"27_CR5","first-page":"292","volume-title":"LNAI 449","author":"A. Boudet","year":"1990","unstructured":"Alexandre Boudet, 1990. Unification in a Combination of Equational Theories: an Efficient Algorithm. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, LNAI 449, pp. 292\u2013307, Kaiserslautern, FRG, Springer-Verlag."},{"key":"27_CR6","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand, 1975. Proving theorems with the modification method. SIAM Journal on Computing, Vol. 4, pp. 412\u2013430.","journal-title":"SIAM Journal on Computing"},{"key":"27_CR7","first-page":"244","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud, 1990. Rewrite Systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6, pp. 244\u2013320. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo."},{"issue":"No.2","key":"27_CR8","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/5383.5389","volume":"33","author":"V. J. Digricoli","year":"1986","unstructured":"Vincent J. Digricoli and Malcolm C. Harrison, 1986. Equality-Based Binary Resolution. Journal of the ACM, Vol. 33, No. 2, pp. 253\u2013289.","journal-title":"Journal of the ACM"},{"key":"27_CR9","unstructured":"Dov Gabbay and Hans J\u00fcrgen Ohlbach, 1992. Quantifier Elimination in Second Order Predicate Logic. Submitted to KR 92."},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Joxan Jaffar and Jean-Louis Lassez, 1987. Constraint Logic Programming. In Fourteenth Annual ACM Symposium on Principles of Programming Languages, pp. 111\u2013119, Munich, West Germany.","DOI":"10.1145\/41625.41635"},{"key":"27_CR11","first-page":"174","volume-title":"LNCS 488","author":"H. Kirchner","year":"1991","unstructured":"H\u00e9l\u00e8ne Kirchner, 1991. Proofs in Parameterized Specifications. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, LNCS 488, pp. 174\u2013187, Como, Italy, Springer-Verlag."},{"key":"27_CR12","volume-title":"Elements of Mathematical Logic","author":"G. Kreisel","year":"1967","unstructured":"Georg Kreisel and Jean-Louis Krivine, 1967. Elements of Mathematical Logic. North-Holland, Amsterdam."},{"key":"27_CR13","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schauss","year":"1989","unstructured":"Manfred Schmidt-Schauss, 1989. Unification in a Combination of Arbitrary Disjoint Equational Theories. Journal of Symbolic Computation, Vol. 8, pp. 51\u201399.","journal-title":"Journal of Symbolic Computation"},{"key":"27_CR14","first-page":"150","volume-title":"LNCS 488","author":"W. Snyder","year":"1991","unstructured":"Wayne Snyder and Christopher Lynch, 1991. Goal Directed Strategies for Paramodulation. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, LNCS 488, pp. 150\u2013161, Como, Italy, Springer-Verlag."},{"issue":"No.4","key":"27_CR15","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. E. Stickel","year":"1985","unstructured":"Mark E. Stickel, 1985. Automated Deduction by Theory Resolution. Journal of Automated Reasoning, Vol. 1, No. 4, pp. 333\u2013355.","journal-title":"Journal of Automated Reasoning"},{"issue":"No.2","key":"27_CR16","first-page":"369","volume":"90","author":"Y. Toyama","year":"1991","unstructured":"Yoshihito Toyama, 1991. How to prove equivalence of term rewriting systems without induction. Theoretical Computer Science, Vol. 90, No. 2, pp. 369\u2013390.","journal-title":"Theoretical Computer Science"},{"key":"27_CR17","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-009-6259-0_4","volume-title":"Handbook of Philosophical Logic, volume II: Extensions of Classical Logic","author":"J. Benthem Van","year":"1984","unstructured":"Johan Van Benthem, 1984. Correspondence Theory. In Dov M. Gabbay, Franz Guenthner, editors, Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, chapter II.4, pp. 167\u2013247. D. Reidel Publishing Company, Dordrecht, Boston, Lancaster."},{"key":"27_CR18","first-page":"675","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics","author":"M. Wirsing","year":"1990","unstructured":"Martin Wirsing, 1990. Algebraic Specification. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 13, pp. 675\u2013788. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo."}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0013841.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:08:14Z","timestamp":1607353694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013841"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055873X"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0013841","relation":{},"subject":[]}}