{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:15:59Z","timestamp":1757542559942},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_185","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:20:30Z","timestamp":1330251630000},"page":"462-476","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["Basic paramodulation and superposition"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[]},{"given":"Christopher","family":"Lynch","sequence":"additional","affiliation":[]},{"given":"Wayne","family":"Snyder","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"35_CR1","first-page":"427","volume-title":"Lect. Notes in Comput. Sci., vol. 449","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In Proc. 10th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 449, pp. 427\u2013441, Berlin, 1990. Springer-Verlag."},{"key":"35_CR2","volume-title":"Technical Report MPI-I-91-208","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Technical Report MPI-I-91-208, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, 1991. To appear in Journal of Logic and Computation."},{"key":"35_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair. Canonical Equational Proofs. Birkhauser Boston, Inc., Boston MA (1991)."},{"key":"35_CR4","volume-title":"Technical Report No. 92-001","author":"L. Bachmair","year":"1992","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic Paramodulation and Superposition. Technical Report No. 92-001, Boston University, Boston, MA, 1992."},{"key":"35_CR5","doi-asserted-by":"crossref","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 Computing 4:4 (1975) pp. 412\u2013430.","journal-title":"SIAM Journal of Computing 4"},{"key":"35_CR6","unstructured":"M. Fay. First-order unification in an equational theory. In Proc. 4th Workshop on Automated Deduction, Austin, Texas (1979)."},{"issue":"3","key":"35_CR7","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. J. ACM 38:3 (July 1991) pp. 559\u2013587.","journal-title":"J. ACM"},{"key":"35_CR8","first-page":"318","volume-title":"Lect. Notes in Comput. Sci., vol. 87","author":"J.-M. Hullot","year":"1980","unstructured":"J.-M. Hullot. Canonical forms and unification. In Proc. 5th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 87, pp. 318\u2013334, Berlin, 1980. Springer-Verlag."},{"key":"35_CR9","volume-title":"Reprinted in Unification","author":"W. Nutt","year":"1990","unstructured":"W. Nutt, P. R\u00e9ty, and G. Smolka. Basic Narrowing Revisited. Reprinted in Unification, C. Kirchner (ed.), Academic Press, London (1990)."},{"key":"35_CR10","unstructured":"W. McCune. Skolem functions and equality in automated deduction. In Proc. 8th Nat. Conf. on AI, MIT Press, 1990, pp. 246\u2013251."},{"key":"35_CR11","volume-title":"Technical Report ANL-90\/9","author":"W. McCune","year":"1990","unstructured":"W. McCune. OTTER 2.0 users guide. Technical Report ANL-90\/9, Argonne National Laboratory, Argonne IL, 1990."},{"key":"35_CR12","first-page":"16","volume-title":"Proc. 10th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 449","author":"X. Nie","year":"1990","unstructured":"X. Nie and D. Plaisted. A complete semantic back-chaining proof system. In Proc. 10th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 449, pp. 16\u201327, Berlin, 1990. Springer-Verlag."},{"key":"35_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(08)80130-7","volume":"11","author":"J. Pais","year":"1991","unstructured":"J. Pais and G. Peterson. Using forcing to prove completeness of resolution and paramodulation. J. Symbolic Computation 11 (1991) pp. 3\u201319.","journal-title":"J. Symbolic Computation"},{"key":"35_CR14","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. Pelletier","year":"1986","unstructured":"F. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning 2 (1986) pp. 191\u2013216.","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR15","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. Peterson","year":"1983","unstructured":"G. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computing 12 (1983) pp. 82\u2013100.","journal-title":"SIAM Journal of Computing"},{"key":"35_CR16","first-page":"228","volume-title":"LNCS vol. 256","author":"P. Rety","year":"1987","unstructured":"P. Rety. Improving basic narrowing techniques. In P. Lescanne, editor, Proc. of 2nd Int. Conf. on Rewrite Techniques and Applications, LNCS vol. 256, pp. 228\u2013241, Berlin, 1987. Springer-Verlag."},{"key":"35_CR17","first-page":"133","volume-title":"Machine Intelligence 4","author":"G.A. Robinson","year":"1969","unstructured":"G.A. Robinson and L. T. Wos. Paramodulation and theorem proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence 4 pp. 133\u2013150. American Elsevier, New York, 1969."},{"key":"35_CR18","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. Slagle","year":"1974","unstructured":"J. Slagle. Automated theorem proving with simplifiers, commutativity, and associativity. J. ACM 21 (1974) pp. 622\u2013642.","journal-title":"J. ACM"},{"key":"35_CR19","unstructured":"M. Smith and D. Plaisted. Term-rewriting techniques for logic programming I: completion. Report TR88-019, Department of Computer Science, Univ. North Carolina (1988)."},{"key":"35_CR20","first-page":"150","volume-title":"Lect. Notes in Comput. Sci., vol. 488","author":"W. Snyder","year":"1991","unstructured":"W. Snyder and C. Lynch. Goal directed strategies for paramodulation. In Proc. 4th Int. Conf. on Rewriteing Techniques and Applications, Lect. Notes in Comput. Sci., vol. 488, pp. 150\u2013161, Berlin, 1991. Springer-Verlag."},{"key":"35_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0435-0","volume-title":"A Proof Theory for General Unification","author":"W. Snyder","year":"1991","unstructured":"W. Snyder. A Proof Theory for General Unification. Birkhauser Boston, Inc., Boston MA (1991)."},{"key":"35_CR22","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. T. Wos","year":"1967","unstructured":"L. T. Wos, G. A. Robinson, D. F. Carson, and L. Shalla. The concept of demodulation in theorem proving. Journal of the ACM, Vol. 14, pp. 698\u2013709, 1967.","journal-title":"Journal of the ACM"},{"key":"35_CR23","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"L. Wos. Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs, New Jersey, 1988."},{"key":"35_CR24","unstructured":"H. Zhang. Reduction, Superposition, and Induction: Automated Reasoning in an Equational Logic. Ph.D. Thesis, Rensselaer Polytechnic Institute (1988)."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_185","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:39:22Z","timestamp":1558269562000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_185"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_185","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}