(* August 19, 1997 (as part of general overhaul) *) (* this script develops the tautology checker NEWTAUT and proves the Gries axioms for propositional logic using the checker *) script "logicdefs"; (* basic logic definitions *) (* convert any propositional expression to a true/false case expression *) (* MAKE_CASE: ?p = ODDCHOICE <= EQUATION => BOOLDEF => (?p = bool : ?p) => ?p ["BOOLDEF","EQUATION","ODDCHOICE"] *) s "?p"; ri "(?p=bool:?p)"; (* uses theorem lookup *) ri "BOOLDEF"; ri "EQUATION"; rri "ODDCHOICE"; p "MAKE_CASE"; (* case expansions for propositional connectives *) (* assertion *) (* ASSERT_EXP: (|-?p) || ?x , ?y = ?p || ?x , ?y ["ASSERT","BOOLDEF","ODDCHOICE"] *) s "(|-?p)||?x,?y"; ri "(LEFT@ASSERT**BOOLDEF)** \$ODDCHOICE"; ex(); p "ASSERT_EXP"; (* negation *) (* NOT_EXP: ( ~?p) || ?a , ?b = ?p || ?b , ?a ["CASEINTRO","NOT","ODDCHOICE"] *) s "(~?p)||?a,?b"; left(); ri "NOT"; ex(); top(); ri "UNPACK"; ex(); rri "ODDCHOICE"; ex(); p "NOT_EXP"; (* conjunction *) (* AND_EXP: (?p & ?q) || ?a , ?b = ?p || (?q || ?a , ?b) , ?b ["AND","CASEINTRO","ODDCHOICE"] *) s "(?p&?q)||?a,?b"; ri "LEFT@AND"; ex(); ri "UNPACK"; ex(); ri "EVERYWHERE@ \$ODDCHOICE"; ex(); p "AND_EXP"; (* disjunction *) (* OR_EXP: (?p | ?q) || ?a , ?b = ?p || ?a , ?q || ?a , ?b ["AND","CASEINTRO","NOT","ODDCHOICE","OR"] *) s "(?p|?q)||?a,?b"; ri "LEFT@OR"; ex(); ri "NOT_EXP";ex(); ri "AND_EXP"; ex(); ri "EVERYWHERE@NOT_EXP"; ex(); p "OR_EXP"; (* implication *) (* IF_EXP: (?p -> ?q) || ?a , ?b = ?p || (?q || ?a , ?b) , ?a ["AND","CASEINTRO","IF","NOT","ODDCHOICE","OR"] *) s "(?p->?q)||?a,?b"; ri "LEFT@IF"; ex(); ri "OR_EXP"; ex(); ri "NOT_EXP"; ex(); p "IF_EXP"; (* a silly lemma *) s "false=true"; ri "EQUATION"; ex(); right();left(); rri "0|-|1"; ex(); top(); rri "CASEINTRO"; ex(); p "NONTRIV2a"; (* it's called NONTRIV2a because this is already present in logicdefs2 *) (* equivalence *) (* IFF_EXP: (?p == ?q) || ?a , ?b = ?p || (?q || ?a , ?b) , ?q || ?b , ?a ["BOOLDEF","CASEINTRO","EQUATION","IFF","NONTRIV","ODDCHOICE","REFLEX"] *) s "(?p==?q)||?a,?b"; ri "LEFT@IFF"; ex(); ri "PCASEINTRO@?q"; ex(); ri "ODDCHOICE"; ex(); ri "EVERYWHERE@LEFT@RL@BOOLDEF"; ex(); ri "EVERYWHERE@LEFT@RIGHT@EQUATION"; ex(); right();left(); ri "EVERYWHERE@LEFT@RIGHT@1|-|1"; ex(); up();right(); ri "EVERYWHERE@LEFT@RIGHT@1|-|1"; ex(); top(); ri "PCASEINTRO@?p"; ex(); ri "ODDCHOICE"; ex(); ri "EVERYWHERE@LEFT@LEFT@EQUATION"; ex(); right();left(); ri "EVERYWHERE@LEFT@LEFT@1|-|1"; ex(); up();right(); ri "EVERYWHERE@LEFT@LEFT@1|-|1"; ex(); top(); ri "EVERYWHERE@LEFT@RL@REFLEX**NONTRIV**NONTRIV2a"; ex(); ri "EVERYWHERE@LEFT@REFLEX**NONTRIV**NONTRIV2a"; ex(); ri "EVERYWHERE@ \$ODDCHOICE"; ex(); p "IFF_EXP"; (* exclusive or/inequivalence *) (* XOR_EXP: (?p =/= ?q) || ?a , ?b = ?p || (?q || ?b , ?a) , ?q || ?a , ?b ["BOOLDEF","CASEINTRO","EQUATION","IFF","NONTRIV","NOT","ODDCHOICE","REFLEX","XOR"] *) s "(?p=/=?q)||?a,?b"; ri "LEFT@XOR"; ex(); ri "NOT_EXP"; ex(); ri "IFF_EXP"; ex(); p "XOR_EXP"; (* converse implication *) (* CN_EXP: (?p <- ?q) || ?a , ?b = ?q || (?p || ?a , ?b) , ?a ["AND","CASEINTRO","CONVIF","IF","NOT","ODDCHOICE","OR"] *) s "(?p<-?q)||?a,?b"; ri "LEFT@CONVIF"; ex(); ri "IF_EXP"; ex(); p "CN_EXP"; (* The case reasoning tool used in the tautology checker *) dpt "ALT_PUSH"; (* ALT_PUSH: ?p || ?a , ?b = CASEINTRO <= ?p || (ALT_PUSH => (EVERYWHERE @ 1 |-| 1) => ?a) , ALT_PUSH => (EVERYWHERE @ 1 |-| 1) => ?b ["CASEINTRO"] *) s "?p||?a,?b"; right();left(); ri "EVERYWHERE@1|-|1"; ri "ALT_PUSH"; up();right(); ri "EVERYWHERE@1|-|1"; ri "ALT_PUSH"; top(); rri "CASEINTRO"; p "ALT_PUSH"; (* procedure for carrying out expansions *) (* ALL_EXP: ?p || ?a , ?b = CN_EXP =>> XOR_EXP =>> IFF_EXP =>> IF_EXP =>> OR_EXP =>> AND_EXP =>> NOT_EXP => ?p || ?a , ?b ["AND","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR"] *) dpt "ALL_EXP"; s "?p||?a,?b"; (* right();left(); ri "ALL_EXP"; up();right(); ri"ALL_EXP"; top(); *) ri "ALL_EXP*>ASSERT_EXP"; ari "ALL_EXP*>NOT_EXP"; ari "ALL_EXP*>AND_EXP"; ari "ALL_EXP*>OR_EXP"; ari "ALL_EXP*>IF_EXP"; ari "ALL_EXP*>IFF_EXP"; ari "ALL_EXP*>XOR_EXP"; ari "ALL_EXP*>CN_EXP"; prove "ALL_EXP"; (* the tautology checker -- a loop tactic *) (* NEWTAUT: ?x = ALL_STEPS => STARTLOOP => MAKE_CASE => ?x ["AND","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR"] *) s "?x"; ri "MAKE_CASE"; ri "TOPDOWN@ALL_EXP"; ri "ALT_PUSH"; prove "NEWTAUT"; (* typing lemmas needed for propositional logic *) (* used by PROVETAUT tactics below *) s "|-?p==?q"; ri "RIGHT@BTYPE"; ri "TWOASSERTS"; rri "BTYPE"; ex(); p "BRULE1"; s "(|-?p)==?q"; ri "BTYPE"; ri "RIGHT@LEFT@TWOASSERTS"; rri "BTYPE"; ex(); p "BRULE2"; s "?p== |-?q"; ri "BTYPE"; ri "RIGHT@RIGHT@TWOASSERTS"; rri "BTYPE"; ex(); p "BRULE3"; s "|-?p|?q"; ri "RIGHT@DTYPE"; ri "TWOASSERTS"; rri "DTYPE"; ex(); p "DRULE1"; s "(|-?p)|?q"; ri "DTYPE"; ri "RIGHT@LEFT@TWOASSERTS"; rri "DTYPE"; ex(); p "DRULE2"; s "?p| |-?q"; ri "DTYPE"; ri "RIGHT@RIGHT@TWOASSERTS"; rri "DTYPE"; ex(); p "DRULE3"; s "|-?p&?q"; ri "RIGHT@CTYPE"; ri "TWOASSERTS"; rri "CTYPE"; ex(); p "CRULE1"; s "(|-?p)&?q"; ri "CTYPE"; ri "RIGHT@LEFT@TWOASSERTS"; rri "CTYPE"; ex(); p "CRULE2"; s "?p& |-?q"; ri "CTYPE"; ri "RIGHT@RIGHT@TWOASSERTS"; rri "CTYPE"; ex(); p "CRULE3"; s "|-?p=/=?q"; ri "RIGHT@XORTYPE"; ri "TWOASSERTS"; rri "XORTYPE"; ex(); p "XRULE1"; s "(|-?p)=/=?q"; ri "XORTYPE"; ri "RIGHT@LEFT@TWOASSERTS"; rri "XORTYPE"; ex(); p "XRULE2"; s "?p=/= |-?q"; ri "XORTYPE"; ri "RIGHT@RIGHT@TWOASSERTS"; rri "XORTYPE"; ex(); p "XRULE3"; s "|- ~?p"; ri "RIGHT@NTYPE"; ri "TWOASSERTS"; rri "NTYPE"; ex(); p "NRULE1"; s "~ |-?p"; ri "NTYPE"; ri "RIGHT@RIGHT@TWOASSERTS"; rri "NTYPE"; ex(); p "NRULE2"; s "|-?p->?q"; ri "RIGHT@IMPTYPE"; ri "TWOASSERTS"; rri "IMPTYPE"; ex(); p "IRULE1"; s "(|-?p)->?q"; ri "IMPTYPE"; ri "RIGHT@LEFT@TWOASSERTS"; rri "IMPTYPE"; ex(); p "IRULE2"; s "?p-> |-?q"; ri "IMPTYPE"; ri "RIGHT@RIGHT@TWOASSERTS"; rri "IMPTYPE"; ex(); p "IRULE3"; s "|-?p<-?q"; ri "RIGHT@CONTYPE"; ri "TWOASSERTS"; rri "CONTYPE"; ex(); p "CNRULE1"; s "(|-?p)<-?q"; ri "CONTYPE"; ri "RIGHT@LEFT@TWOASSERTS"; rri "CONTYPE"; ex(); p "CNRULE2"; s "?p<- |-?q"; ri "CONTYPE"; ri "RIGHT@RIGHT@TWOASSERTS"; rri "CONTYPE"; ex(); p "CNRULE3"; (* Needed: tactic for converting case expressions to a more readable form *) (* Alves-Foss theorem CONDCASES could be part of such a procedure *) (* tactic for applying NEWTAUT *) initializecounter(); s "bool:?x"; ri "CASEINTRO"; ex(); assign "?y_1" "(bool:?x)=bool:?y"; right();left(); ri "0|-|1"; ex(); top();left(); rri "IFF"; ri "NEWTAUT"; top(); prove "PROVETAUT@?y"; s "?x"; rri "BRULE1"; arri "CRULE1"; arri "DRULE1"; arri "NRULE1"; arri "XRULE1"; arri "IRULE1"; arri "CNRULE1"; ri "ASSERT"; ri "PROVETAUT@?y"; ri "ASSERT2"; ri "BRULE1"; ari "CRULE1"; ari "DRULE1"; ari "NRULE1"; ari "XRULE1"; ari "IRULE1"; ari "CNRULE1"; prove "PROVETAUT2@?y"; (* proofs of Gries propositional axioms *) (* BASSOC: (?p == ?q) == ?r = ?p == ?q == ?r ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "(?p==?q)==?r"; ri "PROVETAUT2@?p==?q==?r"; ex(); p "BASSOC"; (* BSYM: ?p == ?q = ?q == ?p ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p==?q"; ri "PROVETAUT2@?q==?p"; ex(); p "BSYM"; (* BID: ?p == ?p = true ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR"] *) s "?p==?p"; ri "NEWTAUT"; ex(); p "BID"; (* BID2: ?p == true = |-?p ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p==true"; ri "PROVETAUT2@ ?p"; ex(); p "BID2"; (* the argument of PROVETAUT2 above is ?p, not |-?p *) (* FDEF: false = ~true ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR"] *) s "~true"; ri "NEWTAUT"; ex(); workback(); p "FDEF"; (* BDIS: ~?p == ?q = (~?p) == ?q ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "~?p==?q"; ri "PROVETAUT2@(~?p)==?q"; ex(); p "BDIS"; (* XORDEF: ?p =/= ?q = ~?p == ?q ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p=/=?q"; ri "PROVETAUT2@ ~?p==?q"; ex(); p "XORDEF"; (* DASSOC: (?p | ?q) | ?r = ?p | ?q | ?r ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "(?p|?q)|?r"; ri "PROVETAUT2@?p|?q|?r"; ex(); p "DASSOC"; (* DSYM: ?p | ?q = ?q | ?p ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p|?q"; ri "PROVETAUT2@?q|?p";ex(); p "DSYM"; (* DIDEM: ?p | ?p = |-?p ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p|?p"; ri "PROVETAUT2@?p"; ex(); p "DIDEM"; (* DDIS: ?p | ?q == ?r = (?p | ?q) == ?p | ?r ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p|?q==?r"; ri "PROVETAUT2@(?p|?q)==?p|?r";ex(); p "DDIS"; (* DXM: ?p | ~?p = true ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR"] *) s "?p| ~?p"; ri "NEWTAUT"; ex(); p "DXM"; (* converse forms of Gries axioms which destroy information *) ae "BID"; wb(); p "BIDF@?p"; ae "DXM"; wb(); p "DXMF@?p"; (* GR: (?p & ?q) == ?p | ?q = ?p == ?q ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "(?p&?q)==?p|?q"; ri "PROVETAUT2@?p==?q"; ex(); p "GR"; (* IDEF: ?p -> ?q = (?p | ?q) == ?q ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p->?q"; ri "PROVETAUT2@(?p|?q)==?q"; ex(); p "IDEF"; (* CONS: ?p -> ?q = ?q <- ?p ["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"] *) s "?p->?q"; ri "PROVETAUT2@?q<-?p"; ex(); p"CONS"; (* LZ: (?e = ?f) & ?F @ ?e = (?e = ?f) & ?F @ ?f ["AND","BOOLDEF","EQUATION","ODDCHOICE"] *) s "(?e=?f)&?F@?e"; ri "AND"; ex(); ri "LEFT@ \$BOOLDEF"; ex(); ri "LEFT@ \$EQBOOL"; ex(); right();left(); ri "EVERYWHERE@0|-|1"; ex(); up();up(); ri "LEFT@EQBOOL"; ri "LEFT@BOOLDEF"; rri "AND"; ex(); p "LZ"; (* ASRTEQ: ?e = ?f = |-?e = ?f ["ASSERT","BOOLDEF","EQUATION","ODDCHOICE"] *) s "?e=?f"; ri "EQBOOL"; ri "ASSERT2"; ex(); p "ASRTEQ"; (* BCONV: ?e == ?f = (|-?e) = |-?f ["ASSERT","IFF"] *) s "?e==?f"; ri "IFF"; ri "RL@ASSERT2"; ex(); p "BCONV"; (* EQT: (|-?p) = true = ?p = true ["ASSERT","BOOLDEF","CASEINTRO","EQUATION","REFLEX","TYPES"] *) s "(|-?p)=true"; ri "EQSYMM"; rri "BOOLDEF"; ri "RIGHT@ASSERT"; ri "TYPES"; ex(); ri "BOOLDEF"; ri "EQSYMM"; ex(); p "EQT"; quit();