{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,11,6]],"date-time":"2022-11-06T17:28:24Z","timestamp":1667755704734},"reference-count":27,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80649-2","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"9-21","source":"Crossref","is-referenced-by-count":7,"title":["Citius altius fortius"],"prefix":"10.1016","volume":"86","author":[{"given":"Thomas","family":"Hillenbrand","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB1","doi-asserted-by":"crossref","unstructured":"J. Avenhaus, J. Denzinger, and M. Fuchs. Discount : a system for distributed equational deduction. In J. Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of LNCS, pages 397\u2013402. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59200-8_72"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB2","doi-asserted-by":"crossref","DOI":"10.1016\/S0747-7171(03)00024-5","article-title":"On using ground joinable equations in equational theorem proving","author":"Avenhaus","year":"2003","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB3","doi-asserted-by":"crossref","unstructured":"J. Avenhaus, and B. L\u00f6chner. CCE: Testing ground joinability. In Proceedings of the 1st International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pages 658\u2013662. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_53"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB4","series-title":"Canonical Equational Proofs","author":"Bachmair","year":"1991"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB5","series-title":"Resolution of Equations in Algebraic Structures, volume 2","first-page":"1","article-title":"Completion without failure","author":"Bachmair","year":"1989"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB6","doi-asserted-by":"crossref","unstructured":"H. Comon, P. Narendran, R. Nieuwenhuis, and M. Rusinowitch. Decision problems in ordered rewriting. In Proceedings of the 13th IEEE Symposium on Logics in Computer Science, pages 276\u2013286. IEEE Computer Society, 1998.","DOI":"10.1109\/LICS.1998.705664"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB7","doi-asserted-by":"crossref","unstructured":"J.-M. Gaillourdet, Th. Hillenbrand, B. L\u00f6chner, and H. Spies. The new Waldmeister loop at work. In F. Baader, editor, Proceedings of the 19th International Conference on Automated Deduction, LNAI. Springer-Verlag, 2003.","DOI":"10.1007\/978-3-540-45085-6_27"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB8","series-title":"Term Indexing, volume 1053 of LNCS","author":"Graf","year":"1996"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB9","doi-asserted-by":"crossref","unstructured":"Th. Hillenbrand, and B. L\u00f6chner. The next Waldmeister loop. In A. Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction, LNAI, pages 486\u2013500. Springer-Verlag, 2002.","DOI":"10.1007\/3-540-45620-1_38"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB10","unstructured":"A. Jaeger. Anwendungen von Nachfolgermengen in Termersetzungssystemen. Projektarbeit, Universit\u00e4t Kaiserslautern, 1997."},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB11","series-title":"The Art of Computer Programming, volume 3: Sorting and Searching","author":"Knuth","year":"1998"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB12","unstructured":"W. K\u00fcchlin. An implementation and investigation of the Knuth-Bendix completion procedure. Interner Bericht 17\/82, Universit\u00e4t Karlsruhe, Fakult\u00e4t f\u00fcr Informatik, 1982."},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB13","unstructured":"D. S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Technical Report ATP-39, University of Texas, Austin, 1977."},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB14","doi-asserted-by":"crossref","unstructured":"E. L. Lusk. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years (invited lecture). In A. Voronkov, editor, Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning, volume 624 of LNAI, pages 96\u2013106. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0013052"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB15","doi-asserted-by":"crossref","unstructured":"U. Martin and T. Nipkow. Ordered rewriting and confluence. In Proceedings of the 10th International Conference on Automated Deduction, volume 449 of LNCS, pages 366\u2013380. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_100"},{"issue":"3","key":"10.1016\/S1571-0661(04)80649-2_NEWBIB16","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","article-title":"Experiments with discrimination-tree indexing and path indexing for term retrieval","volume":"9","author":"McCune","year":"1992","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB17","doi-asserted-by":"crossref","unstructured":"W. McCune. Otte 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, 1994.","DOI":"10.2172\/10129052"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB18","series-title":"Automated Reasoning and its Applications: Essays in Honor of Larry Wos, chapter 5","first-page":"71","article-title":"33 basic test problems: a practical evaluation of some paramodulation strategies","author":"McCune","year":"1997"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB19","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis. Rewrite-based deduction and symbolic constraints (invited talk). In Proceedings of the 16th International Conference on Automated Deduction, volume 1632 of LNCS. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48660-7_28"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB20","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis, Th. Hillenbrand, A. Riazanov, and A. Voronkov. On the evaluation of indexing techniques for theorem proving. In R. Gor\u00e9, A. Leitsch, and T. Nipkow, editors, Proceedings of the First International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pages 257\u2013271. Springer-Verlag, 2001. See also http:\/\/www.mpi-sb.mpg.de\/~hillen\/compit.","DOI":"10.1007\/3-540-45744-5_19"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB21","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reduction for some equational theories","volume":"28","author":"Peterson","year":"1981","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB22","series-title":"Handbook of Automated Reasoning, volume II, chapter 26","first-page":"1853","article-title":"Term indexing","author":"Ramakrishnan","year":"2001"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB23","unstructured":"A. Riazanov and A. Voronkov. Limited resource strategy in resolution theorem proving. Technical Report CSPP-7, University of Manchester, 2000. Accepted for publication in Journal of Symbolic Computation."},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB24","unstructured":"G. Sutcliffe and C. B. Suttner. The CADE ATP system competition. See http:\/\/www.cs.miami.edu\/~tptp\/CASC."},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB25","unstructured":"C. B. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.2.0). Technical Report 99\/02, James Cook University, Townsville, 1999."},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB26","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Algorithms, datastructures, and other issues in efficient automated deduction (invited talk). In R. Gor\u00e9, editor, Proceedings of the First International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pages 13\u201328. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_3"},{"key":"10.1016\/S1571-0661(04)80649-2_NEWBIB27","series-title":"Handbook of Automated Reasoning, volume II, chapter 27","first-page":"1965","article-title":"Combining superposition, sorts and splitting","author":"Weidenbach","year":"2001"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806492?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806492?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:14:26Z","timestamp":1585898066000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806492"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1571066104806492"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80649-2","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}