{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T02:14:09Z","timestamp":1783649649188,"version":"3.55.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) for discovering redundant clauses and inferences. Implementing term orderings is, however, challenging. While KBO comparisons can be performed in linear time and LPO checks in quadratic time, using the best-known algorithms for these orders is not enough. Indeed, our experiments show that for some examples, term ordering checks may use about 98% of the overall proving time. The reason for this is that some equalities that cannot be ordered can become ordered after applying a substitution (post-ordered), and we have to check for post-ordering repeatedly for the same equalities. In this paper, we show how to improve post-ordering checks by introducing a new data structure called\n                    <jats:italic>term ordering diagrams<\/jats:italic>\n                    , in short TODs, which creates an index for these checks. We achieve efficiency by lazy modifications of the index and by storing and reusing information from previously performed checks to speed up subsequent checks. Our experiments demonstrate the efficiency of TODs.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_29","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:54Z","timestamp":1753789674000},"page":"552-569","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Term Ordering Diagrams"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-2613","authenticated-orcid":false,"given":"M\u00e1rton","family":"Hajdu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4735-5215","authenticated-orcid":false,"given":"Robin","family":"Coutelier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"29_CR1","doi-asserted-by":"publisher","unstructured":"Comon, H., Narendran, P., Nieuwenhuis, R., Rusinowitch, M.: Deciding the confluence of ordered term rewrite systems. ACM TOCL (2003). https:\/\/doi.org\/10.1145\/601775.601777","DOI":"10.1145\/601775.601777"},{"key":"29_CR2","doi-asserted-by":"publisher","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT - A Distributed and Learning Equational Prover. Journal of Automated Reasoning (1997). https:\/\/doi.org\/10.1023\/A:1005879229581","DOI":"10.1023\/A:1005879229581"},{"key":"29_CR3","doi-asserted-by":"publisher","unstructured":"Duarte, A., Korovin, K.: Ground Joinability and Connectedness in the Superposition Calculus. In: IJCAR (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_11","DOI":"10.1007\/978-3-031-10769-6_11"},{"key":"29_CR4","doi-asserted-by":"publisher","unstructured":"Gleiss, B., Kov\u00e1cs, L., Rath, J.: Subsumption Demodulation in First-Order Theorem Proving. In: IJCAR (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_17","DOI":"10.1007\/978-3-030-51074-9_17"},{"key":"29_CR5","doi-asserted-by":"publisher","unstructured":"Hajdu, M., Coutelier, R., Kov\u00e1cs, L., Voronkov, A.: Term Ordering Diagrams (extended) (2025). https:\/\/doi.org\/10.48550\/arXiv.2505.22181","DOI":"10.48550\/arXiv.2505.22181"},{"key":"29_CR6","unstructured":"Kamin, S., L\u00e9vy, J.J.: Two generalizations of the recursive path ordering. Unpublished manuscript (1980)"},{"key":"29_CR7","doi-asserted-by":"publisher","unstructured":"Knuth, D.E., Bendix, P.B.: Simple Word Problems in Universal Algebras. In: Automation of Reasoning 2. Springer (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_23","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"29_CR8","doi-asserted-by":"publisher","unstructured":"Korovin, K.: iProver \u2014 An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: IJCAR (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"29_CR9","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: Knuth-Bendix Constraint Solving Is NP-Complete. In: ICALP (2001). https:\/\/doi.org\/10.1007\/3-540-48224-5_79","DOI":"10.1007\/3-540-48224-5_79"},{"key":"29_CR10","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth\u2013Bendix order. Information and Computation (2003). https:\/\/doi.org\/10.1016\/S0890-5401(03)00021-X","DOI":"10.1016\/S0890-5401(03)00021-X"},{"key":"29_CR11","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: CAV. pp. 1\u201335 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"29_CR12","doi-asserted-by":"publisher","unstructured":"L\u00f6chner, B.: A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. In: CADE (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_2","DOI":"10.1007\/978-3-540-25984-8_2"},{"key":"29_CR13","doi-asserted-by":"publisher","unstructured":"L\u00f6chner, B.: Things To Know When Implementing LPO. International Journal on Artificial Intelligence Tools (2006). https:\/\/doi.org\/10.1142\/S0218213006002564","DOI":"10.1142\/S0218213006002564"},{"key":"29_CR14","unstructured":"L\u00f6chner, B., Schulz, S.: An Evaluation of Shared Rewriting. In: IWIL (2001), https:\/\/www.researchgate.net\/publication\/229079124"},{"key":"29_CR15","doi-asserted-by":"publisher","unstructured":"L\u00f6chner, B.: Things to Know when Implementing KBO. Journal of Automated Reasoning (2006). https:\/\/doi.org\/10.1007\/s10817-006-9031-4","DOI":"10.1007\/s10817-006-9031-4"},{"key":"29_CR16","doi-asserted-by":"publisher","unstructured":"McCune, W., Wos, L.: Otter - the CADE-13 competition incarnations. Journal of Automated Reasoning (1997). https:\/\/doi.org\/10.1023\/A:1005843632307","DOI":"10.1023\/A:1005843632307"},{"key":"29_CR17","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, chap.\u00a07. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50009-6","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"29_CR18","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R.: Simple LPO constraint solving methods. Information Processing Letters (1993). https:\/\/doi.org\/10.1016\/0020-0190(93)90226-Y","DOI":"10.1016\/0020-0190(93)90226-Y"},{"key":"29_CR19","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R.: Invited Talk: Rewrite-Based Deduction and Symbolic Constraints. In: CADE (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_28","DOI":"10.1007\/3-540-48660-7_28"},{"key":"29_CR20","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rivero, J.M.: Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. Information and Computation (2002). https:\/\/doi.org\/10.1006\/inco.2002.3146","DOI":"10.1006\/inco.2002.3146"},{"key":"29_CR21","doi-asserted-by":"publisher","unstructured":"Riazanov, A., Voronkov, A.: Partially Adaptive Code Trees. In: JELIA (2000). https:\/\/doi.org\/10.1007\/3-540-40006-0_15","DOI":"10.1007\/3-540-40006-0_15"},{"key":"29_CR22","doi-asserted-by":"publisher","unstructured":"Riazanov, A., Voronkov, A.: Efficient Checking of Term Ordering Constraints. In: CADE (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_3","DOI":"10.1007\/978-3-540-25984-8_3"},{"key":"29_CR23","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, Higher, Stronger: E 2.3. In: CADE (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"29_CR24","doi-asserted-by":"publisher","unstructured":"Sekar, R., Ramakrishnan, I., Voronkov, A.: Term Indexing. In: Handbook of Automated Reasoning, chap.\u00a026. MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50028-X","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"29_CR25","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The CADE ATP System Competition - CASC. AI Magazine (2016). https:\/\/doi.org\/10.1609\/aimag.v37i2.2620","DOI":"10.1609\/aimag.v37i2.2620"},{"key":"29_CR26","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: Stepping Stones in the TPTP World. In: IJCAR (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_3","DOI":"10.1007\/978-3-031-63498-7_3"},{"key":"29_CR27","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: The anatomy of Vampire: Implementing bottom-up procedures with code trees 15(2), 237\u2013265 (1995)","DOI":"10.1007\/BF00881918"},{"key":"29_CR28","doi-asserted-by":"publisher","unstructured":"Vukmirovic, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making Higher-Order Superposition Work. Journal of Automated Reasoning (2022). https:\/\/doi.org\/10.1007\/s10817-021-09613-z","DOI":"10.1007\/s10817-021-09613-z"},{"key":"29_CR29","doi-asserted-by":"publisher","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Science of Computer Programming (2015). https:\/\/doi.org\/10.1016\/j.scico.2014.07.009","DOI":"10.1016\/j.scico.2014.07.009"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:28:49Z","timestamp":1781882929000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}