{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:02:07Z","timestamp":1725487327321},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421177"},{"type":"electronic","value":"9783540451273"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45127-7_22","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:25:25Z","timestamp":1184603125000},"page":"291-305","source":"Crossref","is-referenced-by-count":6,"title":["Deriving Focused Calculi for Transitive Relations"],"prefix":"10.1007","author":[{"given":"Georg","family":"Struth","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,8]]},"reference":[{"issue":"3","key":"22_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. J. Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"J. Logic and Computation"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Rewrite techniques for transitive relations. In Ninth Annual IEEE Symposium on Logic in Computer Science, pages 384\u2013393. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316051"},{"issue":"6","key":"22_CR3","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1145\/293347.293352","volume":"45","author":"L. Bachmair","year":"1998","unstructured":"L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM, 45(6):1007\u20131049, 1998.","journal-title":"Journal of the ACM"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Strict basic superposition. In 15th International Conference on Automated Deduction, volume 1421 of LNAI, pages 160\u2013174. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0054258"},{"key":"22_CR5","doi-asserted-by":"publisher","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. Completeness results for inequality provers. Artificial Intelligence, 27:255\u2013288, 1985.","journal-title":"Artificial Intelligence"},{"key":"22_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/3-540-10009-1_7","volume-title":"5th Conference on Automated Deduction","author":"W. W. Bledsoe","year":"1980","unstructured":"W. W. Bledsoe and L. M. Hines. Variable elimination and chaining in a resolution-based prover for inequalities. In W. Bibel and R. Kowalski, editors, 5th Conference on Automated Deduction, volume 87 of LNCS, pages 70\u201387. Springer-Verlag, 1980."},{"key":"22_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF00263449","volume":"8","author":"L. M. Hines","year":"1992","unstructured":"L. M. Hines. Completeness of a prover for dense linear logics. J. Automated Reasoning, 8:45\u201375, 1992.","journal-title":"J. Automated Reasoning"},{"key":"22_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1006\/jsco.1996.0053","volume":"22","author":"J. Levy","year":"1996","unstructured":"J. Levy and J. Agust\u00ed. Bi-rewrite systems. J. Symbolic Computation, 22:279\u2013314, 1996.","journal-title":"J. Symbolic Computation"},{"key":"22_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/3-540-52885-7_100","volume-title":"10th International Conference on Automated Deduction","author":"U. Martin","year":"1990","unstructured":"U. Martin and T. Nipkow. Ordered rewriting and con uence. In M. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of LNCS, pages 366\u2013380. Springer-Verlag, 1990."},{"key":"22_CR10","series-title":"Lect Notes Comput Sci","first-page":"183","volume-title":"Logic and Machines: Decision Problems and Complexity, Proc. Symposium \u201cRekursive Kombinatorik\u201d","author":"M. M. Richter","year":"1983","unstructured":"M. M. Richter. Some reordering properties for inequality proof trees. In E. B\u00f6rger, G. Hasenjaeger, and D. R\u00f6dding, editors, Logic and Machines: Decision Problems and Complexity, Proc. Symposium \u201cRekursive Kombinatorik\u201d, volume 171 of LNCS, pages 183\u2013197. Springer-Verlag, 1983."},{"issue":"1","key":"22_CR11","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/321679.321689","volume":"19","author":"J. R. Slagle","year":"1972","unstructured":"J. R. Slagle. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. Journal of the ACM, 19(1):120\u2013135, 1972.","journal-title":"Journal of the ACM"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"M. Stickel. Automated deduction by theory resolution. In A. Joshi, editor, 9th International Joint Conference on Artificial Intelligence, pages 1181\u20131186. Morgan Kaufmann, 1985.","DOI":"10.1007\/BF00244275"},{"key":"22_CR13","unstructured":"G. Struth. Deriving focused calculi for transitive relations (extended version). \n                    http:\/\/www.informatik.uni-freiburg.de\/~struth\/papers\/focus.ps.gz."},{"key":"22_CR14","unstructured":"G. Struth. Canonical Transformations in Algebra, Universal Algebra and Logic. PhD thesis, Institut f\u00fcr Informatik, Universit\u00e4t des Saarlandes, 1998."},{"issue":"4","key":"22_CR15","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G.A. Robinson, and D.F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12(4):536\u2013541, 1965.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45127-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T01:45:55Z","timestamp":1550454355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45127-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421177","9783540451273"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45127-7_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}