{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:26:41Z","timestamp":1726406801176},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633853"},{"type":"electronic","value":"9783540698067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63385-5_28","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:25:21Z","timestamp":1330298721000},"page":"1-3","source":"Crossref","is-referenced-by-count":2,"title":["Paramodulation, superposition, and simplification"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Canonical equational proofs. Birkh\u00e4user, Boston, 1991.","DOI":"10.1007\/978-1-4684-7118-2"},{"key":"1_CR2","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. J. of the Association for Computing Machinery, 41:236\u2013276, 1994.","journal-title":"J. of the Association for Computing Machinery"},{"key":"1_CR3","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures (Vol. 2: Rewriting Techniques)","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair, N. Dershowitz, and D. A. Plaisted. Completion without failure. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures (Vol. 2: Rewriting Techniques), pages 1\u201330. Boston, Academic Press, 1989."},{"key":"1_CR4","series-title":"volume 449 of Lect. Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/3-540-52885-7_105","volume-title":"Proc. Tenth Int. Conf. on Automated Deduction","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In Proc. Tenth Int. Conf. on Automated Deduction, volume 449 of Lect. Notes in Artificial Intelligence, pages 427\u2013441. Springer-Verlag, Berlin, 1990."},{"key":"1_CR5","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput., 4:217\u2013247, 1994.","journal-title":"J. Logic Comput."},{"key":"1_CR6","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation. Information and Computation, 121:172\u2013192, 1995.","journal-title":"Information and Computation"},{"key":"1_CR7","volume-title":"Cylindrical Algebaas, Part I","author":"L. Henkin","year":"1971","unstructured":"L. Henkin, J.D. Monk, and A. Tarski. Cylindrical Algebaas, Part I. North-Holland, Amsterdam, 1971."},{"key":"1_CR8","series-title":"Vol. 267 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Proceedings of the Fourteenth EATCS International Conference on Automata, Languages and Programming","author":"J. Hsiang","year":"1987","unstructured":"J. Hsiang and M. Rusinowitch. On word problems in equational theories. In T. Ottmann, editor, Proceedings of the Fourteenth EATCS International Conference on Automata, Languages and Programming, pages 54\u201371, Karlsruhe, West Germany, July 1987. Vol. 267 of Lecture Notes in Computer Science, Springer, Berlin."},{"key":"1_CR9","first-page":"133","volume":"3","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch. A new method for establishing refutational completeness in theorem proving. J. of the Association for Computing Machinery, 3:133\u2013151, 1991.","journal-title":"J. of the Association for Computing Machinery"},{"key":"1_CR10","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery, 27:797\u2013821, 1980.","journal-title":"J. of the Association for Computing Machinery"},{"key":"1_CR11","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, U. K., 1970. Reprinted in Automation of Reasoning 2, Springer, Berlin, pp. 342\u2013376 (1983)."},{"key":"1_CR12","series-title":"Technical Report","volume-title":"Canonical inference","author":"D. Lankford","year":"1975","unstructured":"D. Lankford. Canonical inference. Technical Report ATP-32, Dept. of Mathematics and Computer Science, University of Texas, Austin, 1975."},{"key":"1_CR13","series-title":"Lect. Notes in Comput. Sci.","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-63104-6","volume-title":"Proc. Eighth Int. Conf. on Rewriting Techniques and Applications","author":"W. McCune","year":"1997","unstructured":"W. McCune. Well-behaved search and the Robbins problem. In Proc. Eighth Int. Conf. on Rewriting Techniques and Applications, Lect. Notes in Comput. Sci. Springer-Verlag, Berlin, 1997. To appear."},{"key":"1_CR14","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. J. Symbolic Computation, 19:321\u2013351, 1995.","journal-title":"J. Symbolic Computation"},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. E. Peterson","year":"1983","unstructured":"G. E. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM J. on Computing, 12:82\u2013100, 1983.","journal-title":"SIAM J. on Computing"},{"key":"1_CR16","first-page":"135","volume-title":"Machine Intelligence 4","author":"G. Robinson","year":"1969","unstructured":"G. Robinson and L. Wos. Paramodulation and theorem-proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 135\u2013150. Edinburgh University Press, Edinburgh, Scotland, 1969."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"M. Rusinowitch. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix procedure as a complete set of inference rules. J. Symbolic Computation, 1991. To appear.","DOI":"10.1016\/S0747-7171(08)80131-9"},{"key":"1_CR18","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. J. of the Association for Computing Machinery, 14:698\u2013709, 1967.","journal-title":"J. of the Association for Computing Machinery"},{"key":"1_CR19","volume-title":"Reduction, superposition and induction: Automated reasoning in an equational logic","author":"H. Zhang","year":"1988","unstructured":"H. Zhang. Reduction, superposition and induction: Automated reasoning in an equational logic. PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York, 1988."},{"key":"1_CR20","series-title":"Vol. 310 of Lecture Notes in Computer Science","first-page":"1","volume-title":"Proceedings of the Ninth International Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Hantao Zhang and Deepak Kapur. First-order theorem proving using conditional equations. In E. Lusk and R. Overbeek, editors, Proceedings of the Ninth International Conference on Automated Deduction, pages 1\u201320, Argonne, Illinois, May 1988. Vol. 310 of Lecture Notes in Computer Science, Springer, Berlin."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63385-5_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:18Z","timestamp":1605647898000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63385-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633853","9783540698067"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-63385-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}