{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:36:49Z","timestamp":1759639009950,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,9,21]],"date-time":"2017-09-21T00:00:00Z","timestamp":1505952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Vienna Science Fund","award":["VRG12-004"],"award-info":[{"award-number":["VRG12-004"]}]},{"name":"FWF project","award":["W1255-N23"],"award-info":[{"award-number":["W1255-N23"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>We present an algorithm to optimally compress a finite set of terms using a vectorial totally rigid acyclic tree grammar. This class of grammars has a tight connection to proof theory, and the grammar compression problem considered in this article has applications in automated deduction. The algorithm is based on a polynomial-time reduction to the MaxSAT optimization problem. The crucial step necessary to justify this reduction consists of applying a term rewriting relation to vectorial totally rigid acyclic tree grammars. Our implementation of this algorithm performs well on a large real-world dataset.<\/jats:p>","DOI":"10.1145\/3127401","type":"journal-article","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T13:03:12Z","timestamp":1506344592000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars"],"prefix":"10.1145","volume":"18","author":[{"given":"Sebastian","family":"Eberhard","sequence":"first","affiliation":[{"name":"TU Wien, Wien, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Ebner","sequence":"additional","affiliation":[{"name":"TU Wien, Wien, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6461-5982","authenticated-orcid":false,"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[{"name":"TU Wien, Wien, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,9,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(83)90064-1"},{"key":"e_1_2_1_2_1","first-page":"2","article-title":"The first and second max-SAT evaluations.Journal on Satisfiability","volume":"4","author":"Argelich Josep","year":"2008","journal-title":"Boolean Modeling and Computation"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90050-5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90024-5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90044-X"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2008.01.004"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60178-3_85"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 3rd International Workshop on Implementing Automata (WIA\u201998)","volume":"1660","author":"C\u00e2mpeanu Cezar","year":"1998"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00292-9"},{"key":"e_1_2_1_10_1","unstructured":"Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2007. Tree Automata Techniques and Applications. (2007). Available on: http:\/\/www.grappa.univ-lille3.fr\/tata.  Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2007. Tree Automata Techniques and Applications. (2007). Available on: http:\/\/www.grappa.univ-lille3.fr\/tata."},{"volume-title":"Plaisted","year":"2001","author":"Dershowitz Nachum","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19225-3_8"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2015.01.002"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Sebastian Eberhard and Stefan Hetzl. 2017. On the compressibility of finite languages and formal proofs. http:\/\/www.dmg.tuwien.ac.at\/hetzl\/research\/compressibility_proofs.pdf. To appear.  Sebastian Eberhard and Stefan Hetzl. 2017. On the compressibility of finite languages and formal proofs. http:\/\/www.dmg.tuwien.ac.at\/hetzl\/research\/compressibility_proofs.pdf. To appear.","DOI":"10.1016\/j.ic.2017.09.001"},{"key":"e_1_2_1_15_1","unstructured":"Gabriel Ebner Stefan Hetzl Alexander Leitsch Giselle Reis and Daniel Weller. 2017. On the generation of quantified lemmas. (2017). Submitted.  Gabriel Ebner Stefan Hetzl Alexander Leitsch Giselle Reis and Daniel Weller. 2017. On the generation of quantified lemmas. (2017). Submitted."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_20"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.03.033"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28332-1_26"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_17"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.05.018"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_19"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00982-2_38"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.11.015"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.841160"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/DCC.1999.755679"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1515\/gcc-2012-0016"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2013.06.006"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Ruben Martins Vasco M. Manquinho and In\u00eas Lynce. 2014. Open-WBO: A modular MaxSAT solver. In Theory and Applications of Satisfiability Testing (SAT\u201914). 438--445.  Ruben Martins Vasco M. Manquinho and In\u00eas Lynce. 2014. Open-WBO: A modular MaxSAT solver. In Theory and Applications of Satisfiability Testing (SAT\u201914). 438--445.","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622776.1622780"},{"key":"e_1_2_1_31_1","first-page":"153","article-title":"A note on inductive generalization","volume":"5","author":"Plotkin Gordon D.","year":"1970","journal-title":"Machine Intelligence"},{"key":"e_1_2_1_32_1","first-page":"101","article-title":"A further note on inductive generalization","volume":"6","author":"Plotkin Gordon D.","year":"1971","journal-title":"Machine Intelligence"},{"key":"e_1_2_1_33_1","first-page":"135","article-title":"Transformational systems and the algebraic structure of atomic formulas","volume":"5","author":"Reynolds John C.","year":"1970","journal-title":"Machine Intelligence"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2009.01.004"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/322344.322346"},{"volume-title":"Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning (Lecture Notes in Artificial Intelligence)","author":"Sutcliffe Geoff","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","first-page":"1","article-title":"GNU parallel - The command-line power tool. ;login","volume":"36","author":"Tange Ole","year":"2011","journal-title":"The USENIX Magazine"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(87)80004-5"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39917-9_25"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127401","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127401","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:37:08Z","timestamp":1750217828000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127401"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,21]]},"references-count":39,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3127401"],"URL":"https:\/\/doi.org\/10.1145\/3127401","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2017,9,21]]},"assertion":[{"value":"2016-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}