{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:31Z","timestamp":1725663511058},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540543176"},{"type":"electronic","value":"9783540475583"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54317-1_89","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:40:02Z","timestamp":1330209602000},"page":"162-180","source":"Crossref","is-referenced-by-count":16,"title":["Completion of first-order clauses with equality by strict superposition"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"13_CR1","first-page":"1","volume":"2","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted, 1989. Completion without failure. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, vol. 2, pp. 1\u201330. Academic Press.","journal-title":"Resolution of Equations in Algebraic Structures"},{"key":"13_CR2","series-title":"Lect. Notes in Comput. Sci.","volume-title":"Proc. 3rd Int Conf. Rewriting Techniques and Applications","author":"H. Bertling","year":"1989","unstructured":"H. Bertling and H. Ganzinger, 1989. Completion-time optimization of rewrite-time goal solving. In Proc. 3rd Int Conf. Rewriting Techniques and Applications, Lect. Notes in Comput. Sci., vol. 355, Berlin, Springer-Verlag."},{"key":"13_CR3","series-title":"Lect. Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/3-540-52885-7_105","volume-title":"On restrictions of ordered paramodulation with simplification","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger, 1990. 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, Springer-Verlag."},{"key":"13_CR4","unstructured":"L. Bachmair and H. Ganzinger, 1991. Perfect Model Semantics for Logic Programs with Equality. Submitted for publication."},{"key":"13_CR5","series-title":"Lect. Notes in Comput. Sci.","volume-title":"Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems","author":"N. Dershowitz","year":"1991","unstructured":"N. Dershowitz, 1991. A Maximal-Literal Unit Strategy for Horn Clauses. In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, Lect. Notes in Comput. Sci., vol. to appear, Berlin, Springer-Verlag."},{"key":"13_CR6","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-19242-5_6","volume":"308","author":"H. Ganzinger","year":"1987","unstructured":"H. Ganzinger, 1987. A completion procedure for conditional equations. In S. Kaplan and J.-P. Jouannaud, editors, Conditional Term Rewriting Systems, Lect. Notes in Comput. Sci., vol. 308, pp. 62\u201383, Berlin, Springer-Verlag. To appear in J. Symbolic Computation.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"13_CR7","series-title":"Lect. Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/BFb0039613","volume-title":"STACS'87","author":"H. Ganzinger","year":"1987","unstructured":"H. Ganzinger, 1987. Ground term confluence in parametric conditional equational sepcifications. In STACS'87, Lect. Notes in Comput. Sci., vol. 247, pp. 286\u2013298, Berlin, Springer-Verlag."},{"key":"13_CR8","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume":"267","author":"J. Hsiang","year":"1987","unstructured":"J. Hsiang and M. Rusinowitch, 1987. On word problems in equational theories. In T. Ottmann, editor, Proc. 14th ICALP, Lect. Notes in Comput. Sci., vol. 267, pp. 54\u201371, Berlin, Springer-Verlag.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"13_CR9","unstructured":"J. Hsiang and M. Rusinowitch, 1989. Proving refutational completeness of theorem proving strategies: The transfinite semantic Tree method. Submitted for publication, 1989."},{"key":"13_CR10","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"D. Knuth and P. Bendix, 1970. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford."},{"key":"13_CR11","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1007\/BFb0012854","volume":"310","author":"E. Kounalis","year":"1988","unstructured":"E. Kounalis and M. Rusinowitch, 1988. On word problems in Horn theories. In E. Lusk and R. Overbeek, editors, Proc. 9th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 310, pp. 527\u2013537, Berlin, Springer-Verlag.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"13_CR12","series-title":"Technical Report","volume-title":"Canonical inference","author":"D. Lankford","year":"1975","unstructured":"D. Lankford, 1975. Canonical inference. Technical Report ATP-32, Dept. of Mathematics and Computer Science, University of Texas, Austin."},{"key":"13_CR13","series-title":"Technical Report","volume-title":"Ordered Rewriting and Confluence","author":"U. Martin","year":"1989","unstructured":"U. Martin and T. Nipkow, 1989. Ordered Rewriting and Confluence. Technical Report, Univ. of Cambridge, Cambridge, U.K."},{"key":"13_CR14","series-title":"Lect. Notes in Comput. Sci.","volume-title":"Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems","author":"R. Nieuwenhuis","year":"1991","unstructured":"R. Nieuwenhuis and F. Orejas, 1991. Clausal Rewriting. In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, Lect. Notes in Comput. Sci., vol. to appear, Berlin, Springer-Verlag."},{"key":"13_CR15","unstructured":"M. Rusinowitch, 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, 1988."},{"key":"13_CR16","first-page":"133","volume-title":"Machine Intelligence 4","author":"G.A. Robinson","year":"1969","unstructured":"G.A. Robinson and L. T. Wos, 1969. 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."},{"key":"13_CR17","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, 1967. The concept of demodulation in theorem proving. Journal of the ACM, Vol. 14, pp. 698\u2013709.","journal-title":"Journal of the ACM"},{"key":"13_CR18","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-15976-2_2","volume":"202","author":"H.T. Zhang","year":"1985","unstructured":"H.T. Zhang and J-L. R\u00e9my, 1985. Contextual Rewriting. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, Lect. Notes in Comput. Sci., vol. 202, pp. 46\u201362, Berlin, Springer-Verlag.","journal-title":"Lect. Notes in Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Conditional and Typed Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54317-1_89.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:20:53Z","timestamp":1619572853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54317-1_89"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540543176","9783540475583"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-54317-1_89","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}