{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:14:09Z","timestamp":1760015649067,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Twee is an automated theorem prover for equational logic. It implements unfailing Knuth-Bendix completion with ground joinability testing and a connectedness-based redundancy criterion. It came second in the UEQ division of CASC-J10, solving some problems that no other system solved. This paper describes Twee\u2019s design and implementation.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_35","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"602-613","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Twee: An Equational Theorem Prover"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2880-6121","authenticated-orcid":false,"given":"Nicholas","family":"Smallbone","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"35_CR1","doi-asserted-by":"publisher","unstructured":"Avenhaus, J., Hillenbrand, T., L\u00f6chner, B.: On using ground joinable equationsin equational theorem proving. Journal of Symbolic Computation 36(1), 217\u2013233 (2003), https:\/\/doi.org\/10.1016\/S0747-7171(03)00024-5","DOI":"10.1016\/S0747-7171(03)00024-5"},{"key":"35_CR2","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. Journal of Symbolic Computation 6(1), 1\u201318 (1988), https:\/\/doi.org\/10.1016\/S0747-7171(88)80018-X","DOI":"10.1016\/S0747-7171(88)80018-X"},{"key":"35_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kaci, H., Nivat, M. (eds.) Rewriting Techniques, pp. 1\u201330. Academic Press (1989), https:\/\/doi.org\/10.1016\/B978-0-12-046371-8.50007-9","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"35_CR4","doi-asserted-by":"publisher","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction \u2013 CADE-23. Lecture Notes in Computer Science, vol. 6803, pp. 207\u2013221. Springer (2011), https:\/\/doi.org\/10.1007\/978-3-642-22438-6_17","DOI":"10.1007\/978-3-642-22438-6_17"},{"key":"35_CR5","doi-asserted-by":"publisher","unstructured":"Claessen, K., Smallbone, N.: Efficient encodings of first-order Horn formulas in equational logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated IJCAR 2018- 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10900, pp. 388\u2013404. Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-94205-6_26","DOI":"10.1007\/978-3-319-94205-6_26"},{"key":"35_CR6","doi-asserted-by":"publisher","unstructured":"Comon, H., Narendran, P., Nieuwenhuis, R., Rusinowitch, M.: Deciding the confluence of ordered term rewrite systems. ACM Transactions on Computational Logic 4(1), 33\u201355 (Jan 2003), https:\/\/doi.org\/10.1145\/601775.601777","DOI":"10.1145\/601775.601777"},{"key":"35_CR7","doi-asserted-by":"publisher","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT - a distributed and learning equational prover. Journal of Automated Reasoning 18(2), 189\u2013198 (Apr 1997), https:\/\/doi.org\/10.1023\/A:1005879229581","DOI":"10.1023\/A:1005879229581"},{"key":"35_CR8","doi-asserted-by":"publisher","unstructured":"Denzinger, J., Schulz, S.: Recording and analysing knowledge-based distributed deduction processes. Journal of Symbolic Computation 21(4), 523\u2013541 (1996), https:\/\/doi.org\/10.1006\/jsco.1996.0029","DOI":"10.1006\/jsco.1996.0029"},{"key":"35_CR9","doi-asserted-by":"publisher","unstructured":"Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF. A mechanised logic of computation. Springer, Berlin, Heidelberg (1979), https:\/\/doi.org\/10.1007\/3-540-09724-4","DOI":"10.1007\/3-540-09724-4"},{"key":"35_CR10","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science. pp. 291\u2013302. LICS \u201900, IEEE Computer Society, Los Alamitos, CA, USA (2000), https:\/\/doi.org\/10.1109\/LICS.2000.855777","DOI":"10.1109\/LICS.2000.855777"},{"key":"35_CR11","doi-asserted-by":"publisher","unstructured":"L\u00f6chner, B.: Things to know when implementing KBO. Journal of Automated Reasoning 36(4), 289\u2013310 (Apr 2006), https:\/\/doi.org\/10.1007\/s10817-006-9031-4","DOI":"10.1007\/s10817-006-9031-4"},{"key":"35_CR12","unstructured":"L\u00f6chner, B., Hillenbrand, T.: A phytography of WALDMEISTER. AI Communications 15(2,3), 127\u2013133 (Aug 2002)"},{"key":"35_CR13","doi-asserted-by":"publisher","unstructured":"Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction. pp. 366\u2013380. Springer Berlin Heidelberg, Berlin, Heidelberg (1990), https:\/\/doi.org\/10.1007\/3-540-52885-7_100","DOI":"10.1007\/3-540-52885-7_100"},{"key":"35_CR14","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) Automated Deduction \u2013 CADE 27. pp. 495\u2013507. Springer International Publishing, Cham (2019), https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"35_CR15","doi-asserted-by":"publisher","unstructured":"Sekar, R., Ramakrishnan, I., Voronkov, A.: Chapter 26 - Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1853\u20131964. Handbook of Automated Reasoning, North-Holland, Amsterdam (2001), https:\/\/doi.org\/10.1016\/B978-044450813-3\/50028-X","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"35_CR16","unstructured":"Smallbone, N.: Jukebox. https:\/\/github.com\/nick8325\/jukebox\/ (2018)"},{"key":"35_CR17","doi-asserted-by":"crossref","unstructured":"Smallbone, N.: Twee, an equational theorem prover. https:\/\/nick8325.github.io\/twee\/ (2021)","DOI":"10.1007\/978-3-030-79876-5_35"},{"key":"35_CR18","doi-asserted-by":"publisher","unstructured":"Socher-Ambrosius, R.: A goal oriented strategy based on completion. In: Kirchner, H., Levi, G. (eds.) Algebraic and Logic Programming. pp. 435\u2013445. Springer Berlin Heidelberg, Berlin, Heidelberg (1992), https:\/\/doi.org\/10.1007\/BFb0013842","DOI":"10.1007\/BFb0013842"},{"key":"35_CR19","doi-asserted-by":"publisher","unstructured":"Winkler, S., Moser, G.: M\u00e6dMax: A maximal ordered completion tool. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning. pp. 472\u2013480. Springer International Publishing, Cham (2018), https:\/\/doi.org\/10.1007\/978-3-319-94205-6_31","DOI":"10.1007\/978-3-319-94205-6_31"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:32:33Z","timestamp":1672723953000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}