{"id":259,"date":"2014-11-14T11:58:09","date_gmt":"2014-11-14T11:58:09","guid":{"rendered":"http:\/\/zenon.dsic.upv.es\/muterm-testing\/?page_id=4"},"modified":"2024-11-18T13:14:21","modified_gmt":"2024-11-18T13:14:21","slug":"home","status":"publish","type":"page","link":"http:\/\/zenon.dsic.upv.es\/muterm\/","title":{"rendered":"Description"},"content":{"rendered":"<p>MU-TERM is a tool which can be used to verify a number of termination properties of <i>term rewriting systems<\/i> (TRSs) via different reduction relations which can be associated to them:<\/p>\n<ul>\n<li><a style=\"font-size: 1rem;\" title=\"Termination of Rewriting\" href=\"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/documentation\/#rewterm\">termination of rewriting<\/a><span style=\"font-size: 1rem;\">,<\/span><\/li>\n<li>termination of innermost rewriting,<\/li>\n<li><a title=\"Termination of CS Rewriting\" href=\"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/documentation\/#csrterm\">termination of context-sensitive rewriting<\/a>,<\/li>\n<li>termination of innermost context-sensitive rewriting,<\/li>\n<li><a title=\"Termination of OS Rewriting\" href=\"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/documentation\/#osterm\">termination of order-sorted rewriting<\/a>,<\/li>\n<li>termination of equational rewriting for AvC-theories,<\/li>\n<li>operational termination of conditional rewriting.<\/li>\n<\/ul>\n<p>A number of powerful techniques, frameworks and processors have been implemented and combined to achieve such termination proofs automatically. Among others:<\/p>\n<ul>\n<li>modular treatment of TRSs.<\/li>\n<li>mechanization of the process of finding a proof of termination by using the appropriate instance of the dependency pair framework (including processors for the SCC treatment, narrowing, instantiation, subterm criterion, reduction pairs with usable rules, RPOs, etc.).<\/li>\n<li>Removal processors using polynomial interpretations with linear and simple-mixed interpretations on natural and rational domains.<\/li>\n<li>Removal processors using piecewise polynomial interpretations on convex domains using logic-based model generators as AGES and Mace4.<\/li>\n<li>Polynomial constraint solving using SAT\/SMT and CSP techniques (Multisolver and Barcelogic).<\/li>\n<\/ul>\n<p>The application is written in <a title=\"Haskell\" href=\"http:\/\/haskell.org\/\">Haskell<\/a> and has been developed with <a title=\"GHC\" href=\"http:\/\/www.haskell.org\/ghc\/\">GHC<\/a>, a popular <a title=\"Haskell\" href=\"http:\/\/haskell.org\/\">Haskell<\/a> compiler. The <a title=\"Web Interface\" href=\"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/web-interface\/\">web interface<\/a> is intended to provide a simplified use of the tool and the techniques which can be useful for teaching purposes (for instance, we provide direct access to RPO, polynomial and DP-termination proofs which can be conveniently parameterized).<\/p>\n<p>The current version of MU-TERM is 6.0.4, released in March 2019. It is remarkable that in the last <a title=\"2021 Termination Competition\" href=\"https:\/\/termcomp.github.io\/Y2021\/\">termination competition (2021)<\/a>, MU-TERM participated in five categories and it is the most powerful tool for proving termination of context-sensitive rewriting and operational termination of conditional rewriting.<\/p>\n<hr>\n<p><center><a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/FondosUnionEuropea.png\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone  wp-image-5\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/FondosUnionEuropea.png\" alt=\"Union Europea\" width=\"180\" height=\"62\"><\/a>&nbsp; &nbsp;<a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/?attachment_id=256\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone wp-image-256 size-full\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2016\/12\/2011-Web-EconomiaC-63px.jpg\" width=\"252\" height=\"63\"><\/a><a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/?attachment_id=258\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone wp-image-258 size-full\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2016\/12\/logo_SEIDI.jpg\" width=\"104\" height=\"63\"><\/a><\/center><center><\/center><center><a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/logo_CEducacio.gif\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-full wp-image-8\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/logo_CEducacio.gif\" alt=\"Generalitat Valenciana\" width=\"112\" height=\"48\"><\/a>&nbsp; &nbsp;<a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/logo_upv.jpg\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-full wp-image-9\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/logo_upv.jpg\" alt=\"Universitat Polit\u00e8cnica de Val\u00e8ncia\" width=\"112\" height=\"48\"><\/a>&nbsp; &nbsp;<a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/dsic.gif\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-full wp-image-10\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2014\/11\/dsic.gif\" alt=\"DSIC\" width=\"112\" height=\"48\"><\/a>&nbsp;&nbsp;<a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2024\/11\/vrain.png\" alt=\"VRAIN\"><img decoding=\"async\" class=\"alignnone size-full wp-image-10\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2024\/11\/vrain.png\" width=\"160\" alt=\"VRAIN\"><\/img><\/a><\/center><center><\/center><center><i>&#8220;Una manera de hacer Europa&#8221;<\/i><\/center><\/p>\n","protected":false},"excerpt":{"rendered":"<p>\t\t\t\t<![CDATA[]]>\t\t<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":1,"comment_status":"closed","ping_status":"closed","template":"page-templates\/full-width.php","meta":{"footnotes":""},"class_list":["post-259","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/pages\/259","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/comments?post=259"}],"version-history":[{"count":18,"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/pages\/259\/revisions"}],"predecessor-version":[{"id":549,"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/pages\/259\/revisions\/549"}],"wp:attachment":[{"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/media?parent=259"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}