{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:58Z","timestamp":1725663838633},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_32","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:22:19Z","timestamp":1330251739000},"page":"435-450","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Ordered chaining for total orderings"],"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,5,30]]},"reference":[{"key":"32_CR1","first-page":"427","volume-title":"Lecture Notes in Computer Science, vol. 449","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger, 1990. On Restrictions of Ordered Paramodulation with Simplification. In M. Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Lecture Notes in Computer Science, vol. 449, pp. 427\u2013441, Berlin, Springer-Verlag."},{"key":"32_CR2","volume-title":"Technical Report MPI-I-93-250","author":"L. Bachmair","year":"1993","unstructured":"L. Bachmair and H. Ganzinger, 1993. Ordered Chaining for Total Orderings. Technical Report MPI-I-93-250, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. Full version of this paper."},{"key":"32_CR3","volume-title":"Technical Report MPI-I-93-249","author":"L. Bachmair","year":"1993","unstructured":"L. Bachmair and H. Ganzinger, 1993. Rewrite Techniques for Transitive Relations. Technical Report MPI-I-93-249, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. To appear in Proc. LICS'94."},{"issue":"No.3","key":"32_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger, 1994. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, Vol. 4, No. 3, pp. 1\u201331. Revised version of Technical Report MPI-I-91-208. To appear.","journal-title":"Journal of Logic and Computation"},{"key":"32_CR5","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90015-3","volume":"27","author":"W. Bledsoe","year":"1985","unstructured":"W. Bledsoe, K. Kunen and R. Shostak, 1985. Completeness results for inequality provers. Artificial Intelligence, Vol. 27, pp. 255\u2013288.","journal-title":"Artificial Intelligence"},{"key":"32_CR6","first-page":"70","volume-title":"LNCS 87","author":"W. W. Bledsoe","year":"1980","unstructured":"W. W. Bledsoe and L. M. Hines, 1980. Variable Elimination and Chaining in a Resolution-based Prover for Inequalities. In Wolfgang Bibel, Robert Kowalski, editors, 5th Conference on Automated Deduction, LNCS 87, pp. 70\u201387, Les Arcs, France, Springer-Verlag."},{"key":"32_CR7","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. W. Bledsoe","year":"1990","unstructured":"W.W. Bledsoe, 1990. Challenge problems in elementary calculus. Journal of Automated Reasoning, Vol. 6, pp. 341\u2013359.","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR8","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand, 1975. Proving theorems with the modification method. SIAM Journal of Computing, Vol. 4, pp. 412\u2013430.","journal-title":"SIAM Journal of Computing"},{"key":"32_CR9","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-52885-7_88","volume-title":"10th International Conference on Automated Deduction, LNAI 449","author":"L. Hines","year":"1990","unstructured":"L. Hines, 1990. Str\u2214ve\u2282-: The Str\u2214ve-based Subset Prover. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, LNAI 449, pp. 193\u2013206, Kaiserslautern, FRG, Springer-Verlag."},{"key":"32_CR10","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BF00263449","volume":"8","author":"L. M. Hines","year":"1992","unstructured":"L. M. Hines, 1992. Completeness of a Prover for Dense Linear Logics. Journal of Automated Reasoning, Vol. 8, pp. 45\u201375.","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"L.M. Hines, 1988. Hyper-chaining and knowledge-based theorem proving. In Proc. 9th Int. Conf. on Automated Deduction, Lecture Notes in Computer Science, pp. 469\u2013486. Springer-Verlag.","DOI":"10.1007\/BFb0012850"},{"issue":"No.3","key":"32_CR12","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, 1991. Proving refutational completeness of theorem proving strategies: The transfinite semantic Tree method. Journal of the ACM, Vol. 38, No. 3, pp. 559\u2013587.","journal-title":"Journal of the ACM"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science, vol. 690","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-56868-9_3","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"1993","unstructured":"J. Levy and J. Agust\u00ed, 1993. Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations. In C. Kirchner, editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 17\u201331, Berlin, Springer."},{"issue":"No.2","key":"32_CR14","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","volume":"47","author":"R. Nieuwenhuis","year":"1993","unstructured":"R. Nieuwenhuis, 1993. Simple LPO constraint solving methods. Information Processing Letters, Vol. 47, No. 2, pp. 65\u201369.","journal-title":"Information Processing Letters"},{"key":"32_CR15","first-page":"436","volume-title":"LNCS 690","author":"P. Nivela","year":"1993","unstructured":"P. Nivela and R. Nieuwenhuis, 1993. Saturation of first-order (constrained) clauses with the Saturate system. In Claude Kirchner, editor, Rewriting Techniques and Applications, 5th International Conference, RTA-93, LNCS 690, pp. 436\u2013440, Montreal, Canada, Springer-Verlag."},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"M.M. Richter, 1984. Some reordering properties for inequality proof trees. Lecture Notes in Computer Science, vol. 171, pp. 183\u2013197. Springer-Verlag.","DOI":"10.1007\/3-540-13331-3_41"},{"key":"32_CR17","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, D. Michie, editors, Machine Intelligence 4, PP-133\u2013150. American Elsevier, New York."},{"key":"32_CR18","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1145\/321679.321689","volume":"19","author":"J. R. Slagle","year":"1972","unstructured":"J. R. Slagle, 1972. Automatic theorem proving for theories with Built-in Theories Including Equality, Partial Orderings, and Sets. Journal of the ACM, Vol. 19, pp. 120\u2013135.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:21:28Z","timestamp":1558254088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"30 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}