(* FILE: plgtst.joy *) "\ntesting the propositional logic library in file plglib.joy\n\n" putchars. "plglib" libload. 1 setecho. (* There are many notations. Begin using minimally bracketed infix: *) DEFINE m-show == Min2Tre taut-show-all. [ raining or not raining ] m-show. [ raining or not windy ] m-show. [ [p and q] imp [p or q] ] m-show. [ [p or q] imp [p and q] ] m-show. (* Really using minimal bracketing on the last two examples: *) [ p and q imp p or q ] m-show. [ p or q imp p and q ] m-show. (* Longer examples show the benefit of minimal bracketing: *) [ p and q and r imp p or r or q ] m-show. [ p and q and r iff p or r or q ] m-show. (* Using a more compact single symbol notation: *) [ p & q & r & s > p v r v q v s ] m-show. [ p & q & r & s = p v r v q v s ] m-show. [ - p & - q > - [p v q] ] m-show. [ - p v - p > - [p v q] ] m-show. [ p > q > r > p & q & r ] m-show. [ p > q > r > p & q & s ] m-show. [ [[p > q] > p] > p ] m-show. [ [[p > q] > q] > p ] m-show. [ [ p & q v p & r ] = p & [q v r] ] m-show. [ [ p & q v p & r ] = q & [p v r] ] m-show. [ [p v q] & [p > r] & [q > s] > [r v s] ] m-show. [ [p v q] & [p > r] & [q > s] > [r & s] ] m-show. (* The original Polish notation, used by Polish logicians in the 1920's *) (* N = not, K = and, A = or, C = imp, E = iff : *) DEFINE p-show == Pol2Tre taut-show-all. [ A p N p ] p-show. [ A p N q ] p-show. [ C C p q C N q N p ] p-show. [ C C p q C N p N q ] p-show. [ C K K A p q C p r C q s A r s ] p-show. [ C K K A p q C p r C q s K r s ] p-show. (* But we can also use the other symbols for Polish notation: *) [ imp and imp p q imp q r imp p r ] p-show. [ imp and imp p q imp p r imp q r ] p-show. [ > v p & q r & v p q v p r ] p-show. [ > v p & q r v & p q & p r ] p-show. (* Using reverse Polish (postfix, Joy) notation: *) DEFINE r-show == Rev2Tre taut-show-all. [ p not q not and r imp q p or not and r imp ] r-show. [ p not q not and r imp q p and not and r imp ] r-show. (* The remaining tests only use minimally bracketed infix for input. *) (* There are four additional versions of the possible output: *) (* 1. Instead of showing all countermodels, show only one: *) DEFINE m-show1 == Min2Tre taut-show-first. [ p & q & r > p v q v r ] m-show. [ p v q v r > p & q & r ] m-show. [ p v q v r > p & q & r ] m-show1. (* 2. Do not show, but collect into list (for further processing ?): *) DEFINE m-collect == Min2Tre taut-collect-all; m-collect1 == Min2Tre taut-collect-first. [ [p > q] & [q > s] > [p > s] ] m-collect. [ [p > q] & [q > s] > [s > p] ] m-collect. [ [p > q] & [q > s] > [s > p] ] m-collect1. (* 3. Do not show or collect, just return number of countermodels: *) DEFINE m-count == Min2Tre taut-count. [ [p > q] & [r > s] > [[p & r] > [q v s]] ] m-count. [ [p > q] & [r > s] > [[p v r] > [q & s]] ] m-count. [ [p > q] & [r > s] > [[p v r] > [q & s]] ] m-show. (* 4. Disregard countermodels, just determine whether tautology: *) DEFINE m-test == Min2Tre taut-test. [ [p & q & r] > [p = q = r] ] m-test. [ [p = q = r] > [p & q & r] ] m-test. [ [p = q = r] > [p v q v r] ] m-test. [ [p v q v r] > [p = q = r] ] m-test. (* Finally, for big formulas it can be useful to give a definition: *) (* Also, it can help to set them out over several lines: *) DEFINE big-formula == [ [ CEO-sells-shares imp insider-trading and traders-conspire ] and [ i-trade-exposed imp CEO-resigns or CEO-is-sacked ] and [ CEO-resigns imp i-trade-exposed and shares-drop ] and [ traders-conspire and CEO-is-sacked imp sales-drop ] and [ sales-drop imp CEO-is-sacked and shares-drop ] imp [ CEO-sells-shares imp shares-drop ] ]. big-formula m-test. big-formula m-show. (* So, it ain't half as bad as long as you let them get away with it... *) (* end plgtst.joy *)