{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:19Z","timestamp":1740123319897,"version":"3.37.3"},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2021,9,9]],"date-time":"2021-09-09T00:00:00Z","timestamp":1631145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,9,9]],"date-time":"2021-09-09T00:00:00Z","timestamp":1631145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002835","name":"Chalmers University of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002835","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a number of alternative ways of handling transitive binary relations that commonly occur in first-order problems, in particular <jats:italic>equivalence relations<\/jats:italic>, <jats:italic>total orders<\/jats:italic>, and <jats:italic>transitive relations<\/jats:italic> in general. We show how such relations can be discovered syntactically in an input theory, and how they can be expressed in alternative ways. We experimentally evaluate different such ways on problems from the TPTP, using resolution-based reasoning tools as well as instance-based tools. Our conclusions are that (1) it is beneficial to consider different treatments of binary relations as a user, and that (2) reasoning tools could benefit from using a preprocessor or even built-in support for certain types of binary relations.\n<\/jats:p>","DOI":"10.1007\/s10817-021-09605-z","type":"journal-article","created":{"date-parts":[[2021,9,9]],"date-time":"2021-09-09T21:46:55Z","timestamp":1631224015000},"page":"1097-1124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Handling Transitive Relations in First-Order Automated Reasoning"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8113-4478","authenticated-orcid":false,"given":"Koen","family":"Claessen","sequence":"first","affiliation":[]},{"given":"Ann","family":"Lilliestr\u00f6m","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,9,9]]},"reference":[{"issue":"6","key":"9605_CR1","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1145\/293347.293352","volume":"45","author":"L Bachmair","year":"1998","unstructured":"Leo Bachmair and Harald Ganzinger. Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM, 45(6), 1007\u20131049, 1998","journal-title":"J. ACM"},{"key":"9605_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911). Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9605_CR3","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for sets, binary relations and partial functions. In: Proceedings of the 28th Conference on Computer Aided Verification (CAV\u201916). Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-41528-4_10"},{"key":"9605_CR4","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908). Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9605_CR5","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T., Piskac, R., Waldmann, U., Weidenbach, C.: From search to computation: Redundancy criteria and simplification at work. In: Programming Logics: Essays in Memory of Harald Ganzinger, pp. 169\u2013193. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-37651-1_7"},{"key":"9605_CR6","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Gough, G.: Description logics with transitive roles. Descr. Logics 9(3), 385\u2013410 (1997)","DOI":"10.1093\/logcom\/9.3.385"},{"key":"9605_CR7","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Proceedings of the 25th Conference on Computer Aided Verification (CAV\u201913). Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9605_CR8","doi-asserted-by":"crossref","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.: Relational constraint solving in SMT. In: de Moura, L. (ed.) Proceedings of the 26nd Conference on Automated Deduction (CADE-26). Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-63046-5_10"},{"issue":"4","key":"9605_CR9","doi-asserted-by":"publisher","first-page":"19-es","DOI":"10.1145\/1276920.1276921","volume":"8","author":"RA Schmidt","year":"2007","unstructured":"Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Trans. Comput. Logic 8(4), 19 (2007)","journal-title":"ACM Trans. Comput. Logic"},{"key":"9605_CR10","unstructured":"Schulz, S.: The E theorem prover (2015). http:\/\/www.eprover.org\/. Accessed 3 June 2021"},{"key":"9605_CR11","unstructured":"Sutcliffe, G.: The TPTP problem library (2015). http:\/\/www.tptp.org\/. Accessed 3 June 2021"},{"key":"9605_CR12","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907). Springer, Berlin (2007)"},{"key":"9605_CR13","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: Proceedings of the 22nd Conference on Automated Deduction (CADE-22). Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09605-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09605-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09605-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T03:09:04Z","timestamp":1645499344000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09605-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,9]]},"references-count":13,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["9605"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09605-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,9,9]]},"assertion":[{"value":"9 May 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 July 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 September 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2022","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The open access funding note was missing from this article and should have read \u2018Open access funding provided by Chalmers University of Technology\u2019.","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}