{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:18:58Z","timestamp":1725455938087},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055873X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013842","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:24:11Z","timestamp":1132730651000},"page":"435-445","source":"Crossref","is-referenced-by-count":2,"title":["A goal oriented strategy based on completion"],"prefix":"10.1007","author":[{"given":"Rolf","family":"Socher-Ambrosius","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","first-page":"348","volume-title":"SbReve2: A Term Rewriting Laboratory with (AC)Unfailing Completion","author":"S. Anantharaman","year":"1989","unstructured":"S. Anantharaman, J. Hsiang, and J. Mzali. SbReve2: A Term Rewriting Laboratory with (AC)Unfailing Completion. In: D. Plaisted (Ed.) Proc. of 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill, N.C. (1989). Springer LNCS, 348\u2013360."},{"key":"28_CR2","unstructured":"L. Bachmair, N. Dershowitz and J. Hsiang. Orderings for Equational Proofs. Proc. of 1st Workshop on Logic in Computer Science (1986), 346\u2013357."},{"key":"28_CR3","volume-title":"Coll. On the Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1987","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without Failure. Coll. On the Resolution of Equations in Algebraic Structures, Austin (1987), Academic Press."},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"M. P. Bonacina and J. Hsiang. On Fairness of Completion-Based Theorem Proving Strategies. In: R. V. Book (Ed.). Proc. of 4th Int. Conf. on Rewriting Techniques and Applications, Como (1991). Springer LNCS 488, 348\u2013360.","DOI":"10.1007\/3-540-53904-2_109"},{"key":"28_CR5","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.L. Chang","year":"1973","unstructured":"C.L. Chang and R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York 1973."},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"N. Dershowitz. Termination of Linear Rewriting Systems. In: S. Even, O. Kariv (Ed.). Proc. of 8th Int. Coll. on Automata, Languages and Programming, Acre, Israel (1981). Springer LNCS 115, 448\u2013458.","DOI":"10.1007\/3-540-10843-2_36"},{"key":"28_CR7","first-page":"162","volume":"43","author":"N. Dershowitz","year":"1991","unstructured":"N. Dershowitz, J.-P. Jouannaud. Notations for Rewriting. Bulletin of the EATCS, 43 (1991), 162\u2013173.","journal-title":"Bulletin of the EATCS"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"D. J. Dougherty and P. Johann. An Improved General E-Unification Method. In: M. E. Stickel (Ed.). Proc. 10th Int. Conference on Automated Deduction, Kaiserslautern (1990). Springer LNCS 449, 261\u2013275.","DOI":"10.1007\/3-540-52885-7_93"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"J. Hsiang and M. Rusinowitch. On Word Problems in Equational Theories. In: Th. Ottmann (Ed.). Proc. of 14th Int. Colloquium on Automata, Languages and Programming, Karlsruhe (1987). Springer LNCS 267, 54\u201371.","DOI":"10.1007\/3-540-18088-5_6"},{"key":"28_CR10","unstructured":"J. W. Klop. Term Rewriting Systems. In: S. Abramsky, D. M. Cabbay, and T. S. E. Maibaum (Eds.). Handbook of Logic in Computer Science, Oxford University Press, Oxford, to appear."},{"key":"28_CR11","unstructured":"D.E. Knuth and P.B. Bendix. Simple Word Problems in Universal Algebra. In: J. Leech (Ed.). Computational Problems in Universal Algebra, Pergamon Press (1970)."},{"key":"28_CR12","unstructured":"E. Lusk and R. Overbeek. A short problem set for testing systems that include equational reasoning. Argonne National Laboratory 1984."},{"key":"28_CR13","unstructured":"J. Morris. E-Resolution: Extensions of Resolution to Include the Equality Relation. In: Proc. of 1st Int. Joint Conf. on Artificial Intelligence, Washington, D.C. (1969), 287\u2013294."},{"key":"28_CR14","unstructured":"W. McCune. OTTER User's Manual, Argonne Report ANL-88-44 1988."},{"key":"28_CR15","unstructured":"G. Robinson and L. Wos. Paramodulation and theorem-proving in firstorder theories with equality. In: B. Meltzer, & D. Michie, (Eds.): Machine Intelligence 4. Edinburgh, (1969), 135\u2013150."},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"W. Snyder and Ch. Lynch. Goal Directed Strategies for Paramodulation. In: R. V. Book (Ed.). Proc. of 4th Int. Conf. on Rewriting Techniques and Applications, Como (1991). Springer LNCS 488, 150\u2013161.","DOI":"10.1007\/3-540-53904-2_93"},{"key":"28_CR17","volume-title":"A Goal Oriented Strategy Based on Completion. MPI-I-92-206","author":"R. Socher-Ambrosius","year":"1992","unstructured":"R. Socher-Ambrosius. A Goal Oriented Strategy Based on Completion. MPI-I-92-206, Max-Planck-Inst. f. Informatik, Saarbr\u00fccken 1992."},{"key":"28_CR18","first-page":"698","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, D. Carson, and G. Robinson. Efficiency and Completeness of the set of support strategy in theorem proving. Journal of the ACM 12, (1965), 698\u2013709.","journal-title":"Journal of the ACM"},{"key":"28_CR19","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 1988."}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0013842.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:08:14Z","timestamp":1607353694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013842"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055873X"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0013842","relation":{},"subject":[]}}