UNPKG

5.91 kBHTMLView Raw
1<html>
2<head>
3<title>FOLProof First-Order Logic Checker</title>
4<link rel="stylesheet" href="http://getbootstrap.com/dist/css/bootstrap.min.css">
5<link rel="stylesheet" href="http://getbootstrap.com/assets/css/docs.min.css">
6<script src="https://ajax.googleapis.com/ajax/libs/jquery/2.1.0/jquery.min.js"></script>
7<script type='text/javascript' src='folproof-parser.js'></script>
8<script type='text/javascript' src='folproof-web.js'></script>
9<script type='text/javascript' src='folproof-verifier.js'></script>
10<script type='text/javascript'>
11$(document).ready(function() {
12 var debugMode = true;
13 $("#parentheses").bind("click change", function() { $("#proof-input").keyup(); });
14 $("#proof-input").keyup(function(v) {
15 var proof = $(this).val();
16 var paren = $("#parentheses").val();
17 try {
18 parser.trace = function() { if (console && console.log) console.log(arguments); };
19 var ast = parser.parse(proof);
20 var result = folproof.Verifier.verifyFromAST(ast);
21 $("#result").text(result.message);
22 if (!result.valid) {
23 var str = "<p>Step: " + result.errorStep;
24 if (result.errorSrcLine)
25 str += ", Src Line: " + result.errorSrcLoc.first_line;
26 str += "</p>";
27 $("#result").append(str);
28 $("#result-box").css({ background: "", 'border-left' : "", color : "" });
29 } else {
30 $("#result-box").css({ background: "#ccffcc", 'border-left' : "3px solid green", color : "" });
31 }
32 } catch (err) {
33 $("#result").text(err);
34 $("#result-box").css({ background: "", 'border-left' : "", color : "" });
35 //throw err;
36 }
37 var html = folproofWeb.render(ast, { parentheses : paren });
38 $("#render-panel").empty().append(html);
39 });
40 $("#proof-input").keyup(); // force invocation on load
41 $("button.examples").click(function() {
42 var i = $(this).val();
43 var proof = $("#proof-input");
44 proof.val($("#example" + i).text().substr(1))
45 proof.keyup();
46 });
47});
48</script>
49<style type='text/css' rel='stylesheet'>
50#proof-input { height: 32em; width: 100%; font-family: monospace;}
51#render-panel { height: 21em; font-family: monospace; }
52#result-box { height: 7em; margin-top: 0.8em;}
53.justification { width: 50%; float: right; }
54.FOL-box, .simple-box { border: 1px solid black; border-radius: 3px; padding: 2px;}
55.folproof-error { color: red; font-weight: bold; }
56.lineno { display: block; float: left; width: 1.8em; }
57.rule { clear: both; }
58#examples { display: none; }
59</style>
60</head>
61<body>
62 <div class='container'>
63 <div class='row'>
64 <div class='col-md-12'>
65 <h1>FOLProof</h1>
66 <h4>Javascript First-Order Logic Proof Checker</h4>
67 Source: <a href='https://github.com/cdibbs/folproof/tree/master' title='folproof source on github'>https://github.com/cdibbs/folproof/tree/master</a>
68 <div class='bs-callout bs-callout-info'>
69 <h4>Instructions:</h4>
70 <p>
71 Enter your proof in the input box, below. As you type, the formatted proof
72 will appear on the right, along with a validation status, beneath that. To learn
73 the syntax, try playing with the examples, below, or see the
74 <a href='//github.com/cdibbs/folproof/blob/gh-pages/docs/language.md'>language reference.</a>
75 </p>
76 <p>
77 <strong>Note:</strong> Please be sure you have a modern browser, and that
78 Javascript is enabled.
79 </p>
80 <strong>Examples:<strong>
81 <button class='examples' value='0'>HW3 Problem 5</button>
82 <button class='examples' value='1'>HW3 Problem 4</button>
83 <button class='examples' value='2'>HW3 Problem 7</button>
84 <button class='examples' value='3'>Page 115</button>
85 </div>
86 </div>
87 </div>
88 <div class='row'>
89 <div id='leftcol' class='col-md-6'>
90 <textarea id='proof-input'>
911 A.x(P(x) -> ~Q(x)) : premise
922 | E.x(P(x) and Q(x)) : assumption
93 || with x0
943 || P(x0) and Q(x0) : assumption
954 || P(x0) : and elim1 3
965 || P(x0) -> ~Q(x0) : A.x/x0 elim 1
976 || ~Q(x0) : -> e 5,4
987 || Q(x0) : and elim2 3
998 || contradiction : not elim 6,7
100 ---
1019 | contradiction : E.x/x0 elim 2,3-8
102 ---
10310 ~(E.x(P(x) and Q(x))) : not introduction 2-9
104 </textarea>
105 </div>
106 <div id='rightcol' class='col-md-6'>
107 </div>
108 <div id='rightcol' class='col-md-6'>
109 <div id='render-panel' class='highlight'>
110 </div>
111 <div id='options'>
112 <label>
113 Parentheses:
114 <select id='parentheses'>
115 <option value='minimal'>Minimal (order-of-ops overrides)</option>
116 <option value='user' selected='selected'>User-defined</option>
117 <option value='explicit'>Explicit order-of-ops</option>
118 </select>
119 </label>
120 </div>
121 <div id='result-box' class='bs-callout bs-callout-warning'>
122 <h4>Result:</h4>
123 <div id='result'>
124 </div>
125 </div>
126 </div>
127 </div>
128</div>
129<!-- these are hidden by CSS style rules... -->
130<div id='examples'>
131<div id='example0'>
1321 A.x(P(x) -> ~Q(x)) : premise
1332 | E.x(P(x) and Q(x)) : assumption
134 || with x0
1353 || P(x0) and Q(x0) : assumption
1364 || P(x0) : and elim1 3
1375 || P(x0) -> ~Q(x0) : A.x/x0 elim 1
1386 || ~Q(x0) : -> e 5,4
1397 || Q(x0) : and elim2 3
1408 || contradiction : not elim 6,7
141 ---
1429 | contradiction : E.x/x0 elim 2,3-8
143 ---
14410 ~(E.x(P(x) and Q(x))) : not introduction 2-9
145</div>
146<div id='example1'>
147# Extraneous step #s in the src are ignored. Be careful.
148
1491 A.x(P(x,z))
150 | with y0
1512 | P(y0,z) : A.x/y0 e 1
152 ---
1533 A.y(P(y,z)) : A.y/y0 i 2-2
154</div>
155<div id='example2'>
156# Sloppy syntax is fine :-)
157
158P(a)
159| with x0
160|| a = x0 : assumption
161|| P(x0) : = e 2,1
162 -
163| a = x0 -> P(x0) : -> i 2-3
164-
165A.x(a=x->P(x)) : A.x/x0 i 2-4
166</div>
167<div id='example3'>
1681 A.x(Q(x) -&gt; R(x)) : premise
1692 E.x(P(x) and Q(x)) : premise
170 | with x0
1713 | P(x0) and Q(x0) : assumption
1724 | Q(x0) -&gt; R(x0) : A.x/x0 e 1
1735 | Q(x0) : and e2 3
1746 | R(x0) : -&gt; e 4,5
1757 | P(x0) : and e1 3
1768 | P(x0) and R(x0) : and i 7,6
1779 | E.x(P(x) and R(x)) : E.x/x0 i 8
178 ---
17910 E.x(P(x) and R(x)) : E.x/x0 e 2, 3-9
180</div>
181</div>
182</body>
183</html>