#include #include #include #include #include using namespace std; typedef vector vc; bool expr(); bool expr2(); bool expr3(); bool term(); bool factor(); bool primary(); char getToken(); char lookaheadToken(); bool parse(const string &); string subst(const string &,const vc &,int); vc findVars(const string &); bool expr() { bool a=expr2(); while(lookaheadToken()=='='){ getToken(); bool b=expr2(); a=(a==b); } return a; } bool expr2() { bool a=expr3(); while(lookaheadToken()=='>'){ getToken(); bool b=expr3(); a=(!a)||b; } return a; } bool expr3() { bool a=term(); while(toupper(lookaheadToken())=='V'){ getToken(); bool b=term(); a=a||b; } return a; } bool term() { bool a=factor(); while(lookaheadToken()=='^'){ getToken(); bool b=factor(); a=a&&b; } return a; } bool factor() { bool a=false; if(lookaheadToken()=='~') a=true,getToken(); bool b=primary(); if(a) b=!b; return b; } bool primary() { bool a; char tk=getToken(); if(tk=='('){ a=expr(); getToken(); // skip ')' } else if(toupper(tk)=='T') a=true; else a=false; return a; } queue tokens; char getToken() { if(!tokens.empty()){ char tk=tokens.front(); tokens.pop(); return tk; } else return '\0'; } char lookaheadToken() { return !tokens.empty()?tokens.front():'\0'; } bool parse(const string &s) { for(int i=0;i tbl(128,-1); for(int i=0;i>s){ vc vars=findVars(s); bool bef; int res=0; for(int i=0;i<(1<0 && ret!=bef){ res=-1; break; } bef=ret; } if(res!=-1) res=bef; switch(res){ case 1: cout<<"tautology"<A Av~A ~(A^~A) (D^~D)>A ((A>B)^A)>B ((A>B)^~B)>~A (A>B)>(~B>~A) ((AvB)^~A)>B ((AvB)^~B)>A ~(AvB)=~A^~B ~(A^B)=~Av~B ~AvB=A>B ((A>B)^(B>C))>(A>C) A^(BvC)=(A^B)v(A^C) Av(B^C)=(AvB)^(AvC) */