// The JavaScript Program to implement an equational decision procedure for Residuated Lattices // version of 5 June 2000, by Peter Jipsen, http://proof.mth.uct.ac.za/~pjipsen // The code has three main parts to it: // 1. Handling formulas (actually only the part about equations and inequations is used) // parsing the ascii input and writing html output. // 2. Implementing the Gentzen system decision procedure. // 3. Administering the RL quiz // Part 1. Handling formulas avar = {name:"a", arity:0, output:"a"}; bvar = {name:"b", arity:0, output:"b"}; cvar = {name:"c", arity:0, output:"c"}; dvar = {name:"d", arity:0, output:"d"}; xvar = {name:"x", arity:0, output:"x"}; yvar = {name:"y", arity:0, output:"y"}; zvar = {name:"z", arity:0, output:"z"}; vari = [ xvar, yvar, zvar ]; zero = {name:"0", arity:0, output:"0"}; unit = {name:"1", arity:0, output:"1"}; topp = {name:"T", arity:0, output:"T"}; cons = [ zero, unit, topp ]; meet = {name:"^", arity:2, priority:6, output:' Ù ', infix:true, paren:true}; join = {name:"v", arity:2, priority:6, output:' Ú ', infix:true, paren:true}; times = {name:"*", arity:2, priority:8, output:'*', infix:true, paren:true}; over = {name:"/", arity:2, priority:8, output:'/', infix:true, paren:true}; under = {name:"\\", arity:2, priority:8, output:'\\', infix:true, paren:true}; oper = [ meet, join, times, over, under ]; eq = {name:"=", arity:2, output:' = ', infix:true, priority:4}; //less = {name:"<", arity:2, output:' < ', infix:true}; leq = {name:"<=", arity:2, output:' £ ', infix:true, priority:4}; geq = {name:">=", arity:2, output:' ³ ', infix:true, priority:4}; pred = [ eq, leq, geq ]; for (var i=0; iØ'}; impSymbol = {name:"->", arity:2, priority:1, output:' ® ', infix:true,paren:true}; andSymbol = {name:"and", arity:2, priority:3, output:'  and  ', infix:true,paren:true}; orSymbol = {name:"or", arity:2, priority:2, output:'  or  ', infix:true,paren:true}; iffSymbol = {name:"iff", arity:2, priority:0, output:'   iff   ', infix:true,paren:true}; allSymbol = {name:"A", arity:2, output:'"'}; exSymbol = {name:"E", arity:2, output:'\$'}; conn = [notSymbol, andSymbol, orSymbol, impSymbol, iffSymbol, allSymbol, exSymbol]; comma = {name:",", punc:true}; leftBracket = {name:"(", punc:true}; rightBracket = {name:")", punc:true}; leftSqBracket = {name:"[", punc:true}; rightSqBracket = {name:"]", punc:true}; punc = [comma, leftSqBracket, rightSqBracket, leftBracket, rightBracket ]; function add(arr, elt){ // the push method is not supported in IExpl*der arr[arr.length]=elt; } function Expr(symbol, arg, priority){ // third argument only used during parsing this.symbol = symbol; this.arg = arg; this.priority = priority; } function randomInt(n) { return Math.floor(n*Math.random()); } function randomElt(a) { return a[Math.floor(a.length*Math.random())]; } function randomVari(){ return new Expr(randomElt(vari), []) } function randomList(len,max){ //random list of values in [0..max-1] with one of them = max-1 var l=[]; for (var i=0; i 0) { var op=randomElt(oper); var dep=randomList(op.arity,depth); var arg=[]; for (var i=0; i 0) { var co=randomElt(conn); if (co==allSymbol || co==exSymbol){ var arg = [randomVari(), randomFormula(fDepth-1,tDepth)]; return new Expr(co, arg); } var dep=randomList(co.arity,fDepth); var arg=[]; for (var i=0; i s2.name) return 1 else return -1; } symbols = vari.concat(cons, oper, pred, conn, punc); symbols.sort(compareNames); names = []; for (var i=0; imaxPriority) maxPriority = symbols[i].priority; maxPriority++; //names should contain no blanks function removeCharsAndBlanks(str,n) { var st = str.slice(n); for (var i=0; i=str } function getSymbol(str) { var k=0; var j=0; var st=""; var oldst=""; var more = true; for (var i=1; i<=str.length && more; i++) { oldst=st; st=str.slice(0,i); j=k; k=position(names, st, j); more = (ksymbol.priority || (right.priority==symbol.priority && right.symbol.rightparen)) { expr=new Expr(symbol, [expr,right], symbol.priority); } else { insert=right; while (insert.arg[0].priority && insert.arg[0].prioritysymbol.priority || insert.arg[0].symbol.rightparen) { expr=new Expr(symbol, [expr,insert.arg[0]], symbol.priority); insert.arg[0]=expr; } else { expr=new Expr(symbol, [expr,insert.arg[0].arg[0]], symbol.priority); insert.arg[0].arg[0]=expr; } expr=right; } return [expr,str]; } function parse(str) { var temp = str2expr(str); if (temp[1].slice(0,5)=="Error") document.write("

"+temp[1]+"

"); else if (temp[1].slice(0,5)!="") document.write("

Parse Leftover: "+temp[1]+"

"); //still have to check arities of expressions return temp[0]; } function outputList(li) { for (var i=0; i"); add(proofattempt,proof[proof.length-1]); var l=proof.length; //document.write(space(n)+seq2str(s)+"      "+reason+"
"); if (s.left.length==1 && equalTerms(s.left[0],s.right)) return true; //Id if (s.left.length==0 && s.right.symbol==unit) return true; // 1-right if (s.right.symbol==topp) return true; // T-right if (s.right.symbol==under) // \-right if (isProvable(under.output+"-r", n, new Seq(concat([s.right.arg[0]],s.left),s.right.arg[1]))) return true; else {proof = proof.slice(0,l); return false;} if (s.right.symbol==over) // /-right if (isProvable(over.output+"-r", n, new Seq(concat(s.left,[s.right.arg[1]]),s.right.arg[0]))) return true; else {proof = proof.slice(0,l); return false;} if (s.right.symbol==meet) // meet-right if (isProvable(meet.output+"-r1", n+1, new Seq(s.left,s.right.arg[0])) && isProvable(meet.output+"-r2", n+1, new Seq(s.left,s.right.arg[1]))) return true; else {proof = proof.slice(0,l); return false;} for (var i=0; il", n, new Seq(concat(s.left.slice(0,i),s.left.slice(i+1)),s.right))) return true; else {proof = proof.slice(0,l); return false;} if (s.left[i].symbol==zero) // 0-left return true; if (s.left[i].symbol==times) // *-left if (isProvable(times.output+"-l", n, new Seq(s.left.slice(0,i).concat(s.left[i].arg,s.left.slice(i+1)), s.right))) return true; else {proof = proof.slice(0,l); return false;} if (s.left[i].symbol==meet) // meet-left if (isProvable(meet.output+"-l1", n, new Seq(modify(s.left,i,s.left[i].arg[0]),s.right))) return true; else { proof = proof.slice(0,l); if (isProvable(meet.output+"-l2", n, new Seq(modify(s.left,i,s.left[i].arg[1]),s.right))) return true; else proof = proof.slice(0,l); // try other rules before returning false } if (s.left[i].symbol==join) // join-left if (isProvable(join.output+"-l1", n+1, new Seq(modify(s.left,i,s.left[i].arg[0]),s.right)) && isProvable(join.output+"-l2", n+1, new Seq(modify(s.left,i,s.left[i].arg[1]),s.right))) return true; else {proof = proof.slice(0,l);} // return false;} if (s.left[i].symbol==under) {// \-left for (var j=0; j<=i; j=j+1) // sigma=s.left[j..i-1], gamma=s.left[0..j-1] if (isProvable(under.output+"-l1", n+1, new Seq(s.left.slice(j,i),s.left[i].arg[0])) && isProvable(under.output+"-l2", n+1, new Seq(concat(s.left.slice(0,j), modify(s.left.slice(i),0,s.left[i].arg[1])),s.right))) return true; else proof = proof.slice(0,l); // return false; } if (s.left[i].symbol==over) {// /-left for (var j=i; jl1", n+1, new Seq(s.left.slice(i+1,j+1),s.left[i].arg[1])) && isProvable(over.output+"-l2", n+1, new Seq(concat(modify(s.left.slice(0,i+1),i,s.left[i].arg[0]), s.left.slice(j+1)),s.right))) return true; else proof = proof.slice(0,l); // return false; } } if (s.right.symbol==join) // join-right if (isProvable(join.output+"-r1", n, new Seq(s.left,s.right.arg[0]))) return true; else { proof = proof.slice(0,l); if (isProvable(join.output+"-r2", n, new Seq(s.left,s.right.arg[1]))) return true; else {proof = proof.slice(0,l); return false;} } if (s.right.symbol==times) { // *-right for (var i=0; i<=s.left.length; i=i+1) if (isProvable(times.output+"-r1", n+1, new Seq(s.left.slice(0,i),s.right.arg[0])) && isProvable(times.output+"-r2", n+1, new Seq(s.left.slice(i),s.right.arg[1]))) return true; else proof = proof.slice(0,l); return false; } proof = proof.slice(0,l); return false; } function showProof(s) { proof=[]; proofattempt=[]; if (isProvable("",0,s)) document.write(proof.join("")+"true
"); else document.write(proofattempt.join("")+"false
"); } function pr2str(s) { proof=[]; proofattempt=[]; if (isProvable("",0,s)) return proof.join("")+"true
"; else return proofattempt.join("")+"false
"; } function b(a1,sym,a2) { return new Expr(sym,[a1,a2]); } function eq2leq(eqn){ return b(eqn.arg[0],leq,eqn.arg[1]); } function eq2geq(eqn){ return b(eqn.arg[1],leq,eqn.arg[0]); } function leq2seq(le){ return new Seq([le.arg[0]],le.arg[1]); } //************************************** // Part 3. Administering the RL quiz //generate inequations for quiz inequations=[]; for (var i=0; i<5; i=i+1) add(inequations,b(randomTerm(2),leq,randomTerm(2))); function correct(win, score, st) { win.document.write("Correct, "+st+", 1 point."); return score+1; } function wrong(win, score, st) { win.document.write("Wrong, "+st+", -1 point."); return score-1; } function comment(win, st) { win.document.write("

"+st+"
"); } function check(frm) { //analyse the radio buttons and output results win=open("", "resultWindow", "height=450,width=750,menubar=yes,resizable=yes,scrollbars=yes"); win.document.open(); var score=0; win.document.write("Quiz Results"); win.document.write("

### "+ "Results for your personalised Quiz 1

"); for (var i=0; i"); } win.document.write("

### "+ "Your Score is "+score+"/"+inequations.length+"

"); if (score<1) comment(win,"Guessing will get you nowhere :-)"); else if (score
Click the X in the top right '+ 'hand corner to close this window
'); win.document.write('

Here are the Gentzen sequent proofs and proof attempts '+ 'for the above inequalities:'); for (var i=0; i"+(i+1)+".   "+e2s(inequations[i])+"

"+ pr2str(leq2seq(inequations[i]))); // showProof(win, leq2seq(inequations[i])); } win.document.write(""); win.document.close(); }