{"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":1725663511834},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540563938"},{"type":"electronic","value":"9783540475491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56393-8_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:08:02Z","timestamp":1330254482000},"page":"257-271","source":"Crossref","is-referenced-by-count":2,"title":["Conditional term rewriting and first-order theorem proving"],"prefix":"10.1007","author":[{"given":"David A.","family":"Plaisted","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoffrey D.","family":"Alexander","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heng","family":"Chu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shie-Jue","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"19_CR1","unstructured":"J. Avenhaus and K. Becker. Conditional rewriting modulo a built-in algebra. Technical Report SEKI-Report SR 92-11, Universitaet Kaiserslautern, March 1992."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"G. Alexander and D. Plaisted. Proving equality theorems with hyper-linking. In Proceedings of the 11th International Conference on Automated Deduction, pages 706\u2013710, 1992. system abstract.","DOI":"10.1007\/3-540-55602-8_208"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Owen Astrachan and M. Stickel. Caching and lemma use in model elimination theorem provers. In D. Kapur, editor, Proceedings of the Eleventh International Conference on Automated Deduction, 1992.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"19_CR4","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures 2: Rewriting Techniques","author":"L. Bachmair","year":"1989","unstructured":"Leo Bachmair, N. Dershowitz, and D. Plaisted. Completion without failure. In Hassan Ait-Kaci and Maurice Nivat, editors, Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, pages 1\u201330, New York, 1989. Academic Press."},{"key":"19_CR5","first-page":"427","volume-title":"On restrictions of ordered paramodulation with simplification","author":"L. Bachmair","year":"1990","unstructured":"Leo Bachmair and Harold Ganzinger. On restrictions of ordered paramodulation with simplification. In Mark Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, pages 427\u2013441, New York, 1990. Springer-Verlag."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and basic strict superposition. submitted, 1991.","DOI":"10.1007\/3-540-55602-8_185"},{"key":"19_CR7","unstructured":"W. W. Bledsoe. A new method for proving certain presburger formulas. In Proc. of the 3rd IJCAI, pages 15\u201321, Stanford, CA, 1975."},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1\u201335, 1977.","journal-title":"Artificial Intelligence"},{"key":"19_CR9","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving theorems with the modification method. SIAM J. Comput., 4:412\u2013430, 1975.","journal-title":"SIAM J. Comput."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"H. Comon. Solving inequations in term algebras. In Proceedings of 5th IEEE Symposium on Logic in Computer Science, pages 62\u201369, 1990.","DOI":"10.1109\/LICS.1990.113734"},{"key":"19_CR11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201\u2013215, 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"19_CR12","first-page":"153","volume-title":"Computers and Thought","author":"H. Gelernter","year":"1963","unstructured":"H. Gelernter, J.R. Hansen, and D.W. Loveland. Empirical explorations of the geometry theorem proving machine. In E. Feigenbaum and J. Feldman, editors, Computers and Thought, pages 153\u2013167. McGraw-Hill, New York, 1963."},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and T. Walsh. A theory of abstraction. Artificial Intelligence. to appear.","DOI":"10.1016\/0004-3702(92)90021-O"},{"key":"19_CR14","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken. The intractability of resolution. Theoretical Computer Science, 39:297\u2013308, 1985.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"19_CR15","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M Rusinowitch. Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method. J. Assoc. Comput. Mach., 38(3):559\u2013587, July 1991.","journal-title":"J. Assoc. Comput. Mach."},{"key":"19_CR16","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 Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon, Oxford, U.K., 1970."},{"issue":"3","key":"19_CR17","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue Francaise d'Intelligence Artificielle, 4(3):9\u201352, 1990.","journal-title":"Revue Francaise d'Intelligence Artificielle"},{"key":"19_CR18","volume-title":"PhD thesis","author":"S.-J. Lee","year":"1990","unstructured":"S.-J. Lee. CLIN: An Automated Reasoning System Using Clause Linking. PhD thesis, University of North Carolina at Chapel Hill, 1990."},{"key":"19_CR19","unstructured":"S.-J. Lee and D. Plaisted. Theorem proving using hyper-matching strategy. In Proceedings of the 4th International Symposium on Methodologies for Intelligent Systems, pages 467\u2013476, 1989."},{"key":"19_CR20","unstructured":"S.-J. Lee and D. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 1990. to appear."},{"key":"19_CR21","unstructured":"S.-J. Lee and D. Plaisted. New applications of a fast prepositional calculus decision procedure. In Proceedings of the 8th Biennial Conference of Canadian Society for Computational Studies of Intelligence, pages 204\u2013211, 1990."},{"key":"19_CR22","unstructured":"S.-J. Lee and D. Plaisted. Reasoning with predicate replacement. In Proceedings of the 5th International Symposium on Methodologies for Intelligent Systems, 1990."},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"W. McCune and L. Wos. Experiments in automated deduction with condensed detachment. In Proceedings of the 11th International Conference on Automated Deduction, pages 209\u2013223, July 1992.","DOI":"10.1007\/3-540-55602-8_167"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In Proceedings of the 11th International Conference on Automated Deduction, pages 477\u2013491, July 1992.","DOI":"10.1007\/3-540-55602-8_186"},{"key":"19_CR25","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(82)90041-8","volume":"18","author":"D. Plaisted","year":"1982","unstructured":"D. Plaisted. A simplified problem reduction format. Artificial Intelligence, 18:227\u2013261, 1982.","journal-title":"Artificial Intelligence"},{"key":"19_CR26","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"D. Plaisted. Non-Horn clause logic programming without contrapositives. Journal of Automated Reasoning, 4:287\u2013325, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR27","unstructured":"D. Plaisted. The search efficiency of theorem proving strategies. Draft, 1992."},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"M. Protzen. Disproving conjectures. In Proceedings of the 11th International Conference on Automated Deduction, pages 340\u2013354, July 1992.","DOI":"10.1007\/3-540-55602-8_176"},{"key":"19_CR29","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF00381144","volume":"3","author":"T. C. Wang","year":"1987","unstructured":"T.C. Wang and W.W. Bledsoe. Hierarchical deduction. Journal of Automated Reasoning, 3:35\u201377, 1987.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Conditional Term Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56393-8_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:03:33Z","timestamp":1605647013000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56393-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540563938","9783540475491"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-56393-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}