GenZ-0.1.0.0: exec/index.html
<!DOCTYPE html>
<html lang="en">
<head>
<title>GenZ prover</title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="width=device-width, minimum-scale=1.0, maximum-scale=1.0" />
<script src="jquery.js"></script>
<script>
MathJax = {
tex: {
inlineMath: {'[+]': [['$', '$']]}
}
};
</script>
<script defer src="https://cdn.jsdelivr.net/npm/mathjax@4/tex-chtml.js"></script>
<style type="text/css">
#textinput {
font-size:110%;
margin: 0.1em;
padding: 0.1em;
width:50%;
}
#help {
border:1px solid gray;
display:none;
margin-bottom:1em;
}
#help pre {
font-size:120%;
}
#runbutton {
font-size:110%;
width:40%;
}
#output {
border: 2px solid #666;
margin-top: 1em;
padding: 1em;
width:auto;
overflow-x: hidden;
}
pre, svg {
overflow-x: auto;
max-width:100%;
height:auto;
}
.success {
color: green;
}
.error {
color: red;
font-weight:bold;
}
#running {
color: orange;
display: none;
float: right;
}
details {
margin-top:1em;
border: 1px solid #ddd;
border-radius:2px;
padding-left:5px;
}
summary h3 {
display:inline;
}
.linker {
color:gray;
float:right;
cursor:pointer;
}
.linker:active {
color: black;
text-shadow: 1px 2px #666;
transform: translateY(2px) translateX(2px);
}
/* responsiveness */
@media screen and (max-width: 600px) {
#textinput { width:97% !important; }
#runbutton { width:100%; }
}
</style>
<link rel="icon" href="data:,">
</head>
<body>
<p>
This is the web interface of
<a href="https://github.com/XiaoshuangYang999/GenZ">GenZ</a>.
</p>
<p>
Please choose
<label for="logic">a logic:</label>
<select name="logic" id="logic">
<optgroup label="Propositional">
<option value="prop">CPL</option>
<option value="prop">IPL</option>
</optgroup>
<optgroup label="Modal">
<option value="modal">D</option>
<option value="modal">D4</option>
<option value="modal">D45</option>
<option value="modal">GL</option>
<option value="modal" selected>K</option>
<option value="modal">K4</option>
<option value="modal">K45</option>
<option value="modal">S4</option>
<option value="modal">T</option>
</optgroup>
</select>
and a
<label for="struct">data structure:</label>
<select name="struct" id="struct">
<option value="zipper">zipper</option>
<option value="tree">tree</option>
</select>
</p>
<p>
Enter a formula below <a href="#" onClick='$("#help").slideToggle()'>using this syntax</a> or <label for="examples">choose an example:</label>
<select name="examples" id="examples">
<optgroup label="CPL">
<option value="CPL">p → p</option>
<option value="CPL">p → ¬¬p</option>
<option value="CPL">p ↔ ¬¬p</option>
</optgroup>
<optgroup label="IPL">
<option value="IPL">p → p</option>
<option value="IPL">p → ¬¬p</option>
<option value="IPL">p ↔ ¬¬p</option>
<option value="IPL">¬¬(p | ¬p)</option>
<option value="IPL">(p → q) → ⊥</option><!-- not valid -->
</optgroup>
<optgroup label="D">
<option value="D">☐p → ◇p</option>
</optgroup>
<optgroup label="D4">
<option value="D4">☐p → ☐☐◇p</option>
</optgroup>
<optgroup label="D45">
<option value="D45">◇p → □◇p</option>
</optgroup>
<optgroup label="GL">
<option value="GL">☐(☐p → p) → ☐p</option>
</optgroup>
<optgroup label="K">
<option value="K" selected>☐(p1 & p2) → (☐p1 | ☐p2)</option>
<option value="K">¬◇false</option>
<option value="K">☐☐☐☐true</option>
<option value="K">¬¬¬¬false</option><!-- not valid -->
<option value="K">☐p1 → ☐☐p1</option><!-- not valid -->
</optgroup>
<optgroup label="K4">
<option value="K4">☐☐p → ☐p</option>
<option value="K4">☐☐☐☐☐☐p → ☐☐☐p</option>
<option value="K4">◇□p | □◇□p</option><!-- not valid -->
</optgroup>
<optgroup label="S4">
<option value="S4">☐☐p → ☐p</option>
<option value="S4">p → ◇p</option>
<option value="S4">☐(☐p → ⊥) → ☐(p → ⊥)</option><!-- not valid -->
<option value="S4">☐(☐p → ⊥) → ☐q</option><!-- not valid -->
</optgroup>
<optgroup label="K45">
<option value="K45">◇p → □◇p</option>
</optgroup>
<optgroup label="S4">
<option value="S4">□□p → □p</option>
<option value="S4">□p → □□p</option>
</optgroup>
<optgroup label="T">
<option value="T">□p → p</option>
<option value="T">p → □p</option><!-- not valid -->
</optgroup>
</select>
</p>
<div id="help">
<pre>
| Symbols | Meaning | Note |
|--------------------|-------------------------|----------------------------------|
| p, q, bla, ... | atomic propositions | |
| true, ⊤ | top (constant true) | |
| false, ⊥ | bottom (constant false) | |
| !, ~, ¬ | negation (not) | abreviation for ... -> false |
| & | conjunction (and) | primitive |
| |, v | disjunction (or) | primitive |
| ->, -->, =>, → | implication (if-then) | primitive |
| <->, <-->, <=>, ↔ | bi-implication (iff) | abbreviation using -> and & |
| <>, <a>, ◇ | diamond (possible) | abbreviation for ~ [] ~ ... |
| [], [a], ☐, ◻ | box (necessary) | primitive |
</pre>
</div>
<div>
<input id="textinput" name="textinput" value="☐(p1 & p2) → (☐p1 | ☐p2)" />
<input id="runbutton" type="submit" value="Try to prove this!" onclick="prove()" />
<div id="running">running</div>
</div>
<div id="output"></div>
<script>
"use strict";
function prove() {
$('#running').css("display", "block");
$.ajax({
type: "POST",
url: "prove",
data: { "syntax": $('#logic').val()
, "logic": $('#logic option:selected').text()
, "textinput": $('#textinput').val()
, "struct": $('#struct').val()
},
success:
function(data,textStatus,jqXHR) {
$('#output').html(data);
$('#running').css("display", "none");
MathJax.typesetPromise();
},
timeout: 7000,
error:
function(jqXHR,textStatus,errorThrown) {
$('#output').html("<pre>" + textStatus + " " + errorThrown + "</pre>" );
$('#running').css("display", "none");
}
});
}
$('#textinput').on('keypress', function (e) {
if(e.which === 13){
prove();
}
});
$('#examples').change(function (e) {
$('#textinput').val( $('#examples option:selected').text() );
// also adjust chosen logic to the example
$('#logic option').filter(function(index) {
return $(this).text() === $('#examples option:selected').val();
}).prop('selected', true);
prove();
});
const hash = window.location.hash.substring(1);
if (hash) {
$('#textinput').val(decodeURIComponent(hash));
$('#runbutton').click();
// remove hash?
// history.pushState("", document.title, window.location.pathname + window.location.search);
}
</script>
</body>
</html>