{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:49Z","timestamp":1767928009660,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540528852","type":"print"},{"value":"9783540471714","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_105","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:45:23Z","timestamp":1330188323000},"page":"427-441","source":"Crossref","is-referenced-by-count":44,"title":["On restrictions of ordered paramodulation with simplification"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"31_CR1","first-page":"1","volume":"2","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., and Plaisted, D. 1989. Completion without failure. In Resolution of Equations in Algebraic Structures, vol. 2, ed. H. Ait-Kaci and M. Nivat, 1\u201330. Academic Press.","journal-title":"Resolution of Equations in Algebraic Structures"},{"key":"31_CR2","series-title":"Lect. Notes in Comput. Sci.","volume-title":"Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L., and Ganzinger, H. 1990. Completion of first-order clauses with equality by strict superposition. In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems. Lect. Notes in Comput. Sci. Berlin, Springer-Verlag. To appear."},{"key":"31_CR3","series-title":"Lect. Notes in Comput. Sci.","first-page":"62","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1987","unstructured":"Ganzinger, H. 1987. A completion procedure for conditional equations. In Conditional Term Rewriting Systems, ed. S. Kaplan and J.-P. Jouannaud, 62\u201383. Lect. Notes in Comput. Sci., vol. 308. Berlin, Springer-Verlag. To appear in J. Symbolic Computation."},{"key":"31_CR4","series-title":"Lect. Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Proc. 14th ICALP","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., and Rusinowitch, M. 1987. On word problems in equational theories. In Proc. 14th ICALP, ed. T. Ottmann, 54\u201371. Lect. Notes in Comput. Sci., vol. 267. Berlin, Springer-Verlag."},{"key":"31_CR5","unstructured":"Hsiang, J., and Rusinowitch, M. 1989. Proving refutational completenes of theorem proving strategies: The transfinite semantic tree method. Submitted for publication."},{"key":"31_CR6","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G. 1980. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27:797\u2013821.","journal-title":"J. ACM"},{"key":"31_CR7","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, 263\u2013297. Oxford, Pergamon Press."},{"key":"31_CR8","series-title":"Lect. Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1007\/BFb0012854","volume-title":"Proc. 9th Int. Conf. on Automated Deduction","author":"E. Kounalis","year":"1988","unstructured":"Kounalis, E., and Rusinowitch, M. 1988. On word problems in Horn theories. In Proc. 9th Int. Conf. on Automated Deduction, ed. E. Lusk and R. Overbeek, 527\u2013537. Lect. Notes in Comput. Sci., vol. 310. Berlin, Springer-Verlag."},{"key":"31_CR9","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":"31_CR10","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, 133\u2013150. New York, American Elsevier."},{"key":"31_CR11","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. Submitted for publication."},{"key":"31_CR12","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. ACM 14:698\u2013709.","journal-title":"J. ACM"},{"key":"31_CR13","volume-title":"Reduction, superposition and induction: Automated reasoning in an equational logic","author":"H. Zhang","year":"1988","unstructured":"Zhang, H. 1988. Reduction, superposition and induction: Automated reasoning in an equational logic. Ph.D. diss., Rensselaer Polytechnic Institute, Schenectady, New York."},{"key":"31_CR14","series-title":"Lect. Notes in Comput. Sci.","first-page":"1","volume-title":"Proc. 9th Int. Conf. on 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 Int. Conf. on Automated Deduction, ed. E. Lusk and R. Overbeek, 1\u201320. Lect. Notes in Comput. Sci., vol. 310. Berlin, Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_105.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:09:35Z","timestamp":1619557775000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_105","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990]]}}}