{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:57:28Z","timestamp":1725663448137},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540510819"},{"type":"electronic","value":"9783540461494"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51081-8_97","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:37:01Z","timestamp":1330184221000},"page":"15-28","source":"Crossref","is-referenced-by-count":5,"title":["Proof normalization for resolution and paramodulation"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"3_CR1","volume-title":"Proof methods for equational theories","author":"L. Bachmair","year":"1987","unstructured":"Bachmair, L. 1987. Proof methods for equational theories. Ph.D. diss., University of Illinois, Urbana-Champaign."},{"key":"3_CR2","unstructured":"Bachmair, L., Dershowitz, N., and Hsiang, J. 1986. Orderings for equational proofs. In Proc. Symp. Logic in Computer Science, Boston, Massachusetts, 346\u2013357."},{"key":"3_CR3","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D. 1975. Proving theorems with the modification method. SIAM J. Comput.4:412\u2013430.","journal-title":"SIAM J. Comput."},{"key":"3_CR4","volume-title":"A structured design-method for specialized proof procedures","author":"T. Brown","year":"1975","unstructured":"Brown, T. 1975. A structured design-method for specialized proof procedures. Ph.D. diss., California Institute of Technology, Pasadena."},{"key":"3_CR5","volume-title":"Symbolic logic and mechanical theorem proving","author":"C. Chang","year":"1973","unstructured":"Chang, C., and Lee, R. C. 1973. Symbolic logic and mechanical theorem proving. New York, Academic Press."},{"key":"3_CR6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N. 1982. Orderings for term-rewriting systems. Theor. Comput. Sci.17:279\u2013301.","journal-title":"Theor. Comput. Sci."},{"key":"3_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N. 1987. Termination of rewriting. J. Symbolic Computation3:69\u2013116.","journal-title":"J. Symbolic Computation"},{"key":"3_CR8","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., and Manna, Z. 1979. Proving termination with multiset orderings. Commun. ACM22:465\u2013476.","journal-title":"Commun. ACM"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Ganzinger, H. 1988. A completion procedure for conditional equations. To appear in J. Symbolic Computation.","DOI":"10.1007\/3-540-19242-5_6"},{"key":"3_CR10","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-16780-3_86","volume":"230","author":"J. Hsiang","year":"1986","unstructured":"Hsiang, J., and Rusinowitch, M. 1986. A new method for establishing refutational completeness in theorem proving. In Proc. 8th Int. Conf. on Automated Deduction, ed. J. H. Siekmann, Lect. Notes in Comput. Sci., vol. 230, Berlin, Springer-Verlag, 141\u2013152.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"3_CR11","unstructured":"Hsiang, J., and Rusinowitch, M. 1988. Proving refutational completeness of theorem proving strategies, Part I: The transfinite semantic tree method. Submitted for publication."},{"key":"3_CR12","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W. Joyner","year":"1976","unstructured":"Joyner, W. 1976. Resolution strategies as decision procedures. J. ACM23:398\u2013417.","journal-title":"J. ACM"},{"key":"3_CR13","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., and Bendix, P. 1970. simple word problems in universal algebras. In Computational Problems in Abstract Algebra, ed. J. Leech, Oxford, Pergamon Press, 263\u2013297."},{"key":"3_CR14","series-title":"Tech. Rep.","volume-title":"Canonical inference","author":"D. Lankford","year":"1975","unstructured":"Lankford, D. 1975. Canonical inference. Tech. Rep. ATP-32, Dept. of Mathematics and Computer Science, University of Texas, Austin."},{"key":"3_CR15","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. Peterson","year":"1983","unstructured":"Peterson, G. 1983. A technique for establishing completeness results in theorem proving with equality. SIAM J. Comput.12:82\u2013100.","journal-title":"SIAM J. Comput."},{"key":"3_CR16","first-page":"133","volume-title":"Machine Intelligence 4","author":"G. Robinson","year":"1969","unstructured":"Robinson, G., and Wos, L. T. 1969. Paramodulation and theorem proving in first order theories with equality. In Machine Intelligence 4, ed. B. Meltzer and D. Michie, New York, American Elsevier, 133\u2013150."},{"key":"3_CR17","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM12:23\u201341.","journal-title":"J. ACM"},{"key":"3_CR18","unstructured":"Rusinowitch, M. 1988. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix procedure as a complete set of inference rules."},{"key":"3_CR19","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. R. Slagle","year":"1974","unstructured":"Slagle, J. R. 1974. Automated theorem proving for theories with simplifiers, commutativity, and associativity. J. ACM21:622\u2013642.","journal-title":"J. ACM"},{"key":"3_CR20","first-page":"609","volume-title":"Word Problems","author":"L. T. Wos","year":"1973","unstructured":"Wos, L. T., and Robinson, G. 1973. Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving. In Word Problems, ed. W.W. Boone et al., Amsterdam, North-Holland, 609\u2013639."},{"key":"3_CR21","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. T. Wos","year":"1967","unstructured":"Wos, L. T., Robinson, G. A., Carson, D. F., and Shalla, L. 1967. The concept of demodulation in theorem proving. J. ACM14:698\u2013709.","journal-title":"J. ACM"},{"key":"3_CR22","series-title":"Let. Notes in Comput. Sci.","first-page":"1","volume-title":"Proc. 9th Conf. Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., and Kapur, D. 1988. First-order theorem proving using conditional rewrite rules. In Proc. 9th Conf. Automated Deduction, Let. Notes in Comput. Sci. Berlin, Springer-Verlag, 1\u201320."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51081-8_97.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:19:35Z","timestamp":1605629975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51081-8_97"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540510819","9783540461494"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-51081-8_97","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}