{"id":131,"date":"2015-02-10T11:44:37","date_gmt":"2015-02-10T11:44:37","guid":{"rendered":"http:\/\/zenon.dsic.upv.es\/muterm-testing\/?page_id=131"},"modified":"2022-07-08T15:28:22","modified_gmt":"2022-07-08T15:28:22","slug":"web-interface","status":"publish","type":"page","link":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/web-interface\/","title":{"rendered":"Web Interface"},"content":{"rendered":"<p><script type=\"text\/javascript\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/scripts\/jquery.pack.js\"><\/script><br \/>\n<script type=\"text\/javascript\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/scripts\/jquery.blockUI.js\"><\/script><br \/>\n<script type=\"text\/javascript\" src=\"http:\/\/zenon.dsic.upv.es\/muterm\/scripts\/webinterface.js\"><\/script><\/p>\n<p>Please enter your program here in <a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/documentation\/#TPDB\" title=\"TPDB\">TPDB<\/a> format or <a href=\"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/documentation\/#OBJMaude\" title=\"OBJ\/Maude\">OBJ\/Maude<\/a> format:<\/p>\n<form method=\"post\" name=\"myform\" onsubmit=\"filterTRS();\" enctype=\"multipart\/form-data\">\n<input type=\"hidden\" name=\"MAX_FILE_SIZE\" value=\"30000\"><\/p>\n<p><textarea id=\"area\" name=\"TRSCad\" rows=\"25\" style=\"width:100%;background:url(http:\/\/zenon.dsic.upv.es\/muterm\/wp-content\/uploads\/2015\/02\/artes1.jpg);background-size:cover;\"><\/textarea><br \/>\nor upload a file: <input id=\"myfile\" name=\"userfile\" type=\"file\" title=\"Load the content of the file as the program.\"> <input class=\"button\" onclick=\"getFile();\" type=\"button\" title=\"Load the content of the file and show it above.\" value=\"Upload\"> &nbsp;&nbsp; or load an existing example: <select id=\"myselect\" name=\"exSelect\"><option value=\"0\">Example 1 &#8211; IJCAR20<\/option><option value=\"1\">Example 4 &#8211; IJCAR20<\/option><option value=\"2\">Example 6 &#8211; IJCAR20<\/option><option value=\"3\">Example 7 &#8211; IJCAR20<\/option><\/select> <input class=\"button\" onclick=\"getExample();\" type=\"button\" title=\"Load preset example.\" value=\"Load\"><\/p>\n<fieldset style=\"border:1px solid #CCCCCC;padding: 1px;vertical-align: middle;\">\n<legend>Basic usage<\/legend>\n<p>&nbsp;&nbsp;<input id=\"autobutton\" name=\"Submit\" type=\"button\" onclick=\"filterTRS('0');\" value=\"Prove Automatically\" title=\"Prove termination using the best methods.\"> using a timeout of <input id=\"time0\" name=\"timeoutaut\" type=\"text\" value=\"60\" size=\"3\" maxlength=\"3\"> seconds.<\/fieldset>\n<div style=\"overflow:hidden;height:220px;\">\n<div style=\"width:50%;float:left;height:220px;\">\n<fieldset style=\"height:90%;border:1px solid #CCCCCC;padding: 10px;vertical-align: middle;\">\n<legend>Proof settings<\/legend>\n<ol>\n<li><select id=\"polytype\" name=\"polytype\" onchange=\"checkDimension()\"><option value=\"Linear\" selected=\"selected\">linear<\/option><option value=\"SimpleMixed\">simple-mixed<\/option><\/select> polynomials,<\/li>\n<li><select id=\"polycoeff\" name=\"polycoeff\" onchange=\"checkDimension()\"><option value=\"Rational\" selected=\"selected\">rational<\/option><option value=\"NoRational\">no rational<\/option><\/select> coefficients,<\/li>\n<li>coefficients dimension <input type=\"text\" id=\"dimcoeff\" name=\"dimcoeff\" value=\"1\" size=\"3\" maxlength=\"3\">,<\/li>\n<li>coefficients maximum value <input type=\"text\" id=\"maxvalue\" name=\"maxvalue\" value=\"2\" size=\"3\" maxlength=\"3\">,<\/li>\n<li>and timeout of <input name=\"timeoutadv\" type=\"text\" value=\"5\" size=\"3\" maxlength=\"3\"> seconds.<\/li>\n<\/ol>\n<\/fieldset>\n<\/div>\n<div style=\"height:220px;width:48%;overflow:hidden;float:right;\">\n<fieldset style=\"height:90%;border:1px solid #CCCCCC;padding: 10px;vertical-align: middle;\">\n<legend>Proof techniques<\/legend>\n<p>    Proof with (only (CS-)TRSs in TPDB format):<\/p>\n<ol>\n<li><input class=\"button\" name=\"Submit\" type=\"button\" onclick=\"filterTRS('1');\" value=\"Polynomials\" title=\"Prove termination using polynomial interpretation.\"><\/li>\n<li><input class=\"button\" name=\"Submit\" type=\"button\" onclick=\"filterTRS('2');\" value=\"RPO\" title=\"Prove termination using Recursive Path Orderings.\"><\/li>\n<li><input class=\"button\" name=\"Submit\" type=\"button\" onclick=\"filterTRS('3');\" value=\"DP\" title=\"Prove termination using DPs and polymial interpretation.\" <=\"\" ol=\"\"><\/li>\n<\/ol>\n<\/fieldset>\n<\/div>\n<\/div>\n<\/form>\n<div>\n<h1>Result<\/h1>\n<pre id=\"divResult\"><\/pre>\n<\/div>\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":4,"comment_status":"closed","ping_status":"open","template":"page-templates\/full-width.php","meta":{"footnotes":""},"class_list":["post-131","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/pages\/131","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=131"}],"version-history":[{"count":59,"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/pages\/131\/revisions"}],"predecessor-version":[{"id":508,"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/pages\/131\/revisions\/508"}],"wp:attachment":[{"href":"http:\/\/zenon.dsic.upv.es\/muterm\/index.php\/wp-json\/wp\/v2\/media?parent=131"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}