(* :Title: TruthTable *) 
(* :Author: Christopher Moretti *) 
(* :Summary: 
        TruthTable[ expression-list, variable-list] creates a full truth table
           whose 
columns start with the variables from
variable-list followed by the logical expressions 
from expression-list. *) 
(* :History: Version 1.0 by Christopher Moretti, 1997 *) 

Clear[TruthTable] 
TruthTable[ expr_,vars_List]:= 
 Block[ {num,tab,i,j,l,bin1,bin2,truthcomps,value}, 
  num=Length[vars]; 
  tab={Flatten[Join[vars,{expr}]], 
        Table["-----",{j,0,num-1+ Length[Flatten[{expr}]]}]}; 
  Do[ 
   bin1=IntegerDigits[i,2]; 
   bin2=Join[Table[0,{l,0,num-1-Length[bin1]}],bin1]+1; 
   truthcomps=Map[(#1==1)&,bin2]; 
   value=(expr/.Table[vars[[j]]->truthcomps[[j]],{j,1,num}]); 
   AppendTo[truthcomps,value]; 
   AppendTo[tab,Flatten[truthcomps]];,{i,0,2^num-1}]; 
  Return[TableForm[tab]] 
 ];
TruthTable::usage=
    "TruthTable[ expression-list, variable-list] creates a full truth table \
whose 
columns start with the variables from
variable-list followed by the logical expressions 
from expression-list." 


(* :Title: LogicalTypeCheck *) 
(* :Author: Christopher Moretti *) 
(* :Summary: LogicalTypeCheck[ logicalexpression, variable-list] returns \
whether 
logicalexpression is a tautology, contradiction, or a contigency (based on \
the variables in 
variable-list). *) 
(* :History: Version 1.0 by Christopher Moretti, 1997 *) 

LogicalTypeCheck[ expr_,vars_List]:= 
 Block[ {num,tab,i,j,l,bin1,bin2,truthcomps,value,lasrow}, 
  num=Length[vars]; 
  tab={}; 
  Do[ 
   bin1=IntegerDigits[i,2]; 
   bin2=Join[Table[0,{l,0,num-1-Length[bin1]}],bin1]+1; 
   truthcomps=Map[(#1==1)&,bin2]; 
   value=(expr/.Table[vars[[j]]->truthcomps[[j]],{j,1,num}]); 
   AppendTo[truthcomps,value]; 
   AppendTo[tab,Flatten[truthcomps]];,{i,0,2^num-1}]; 
  lasrow=Union[Transpose[tab][[-1]]]; 
  Which[lasrow=={False}, 
      Print["The logical expression ",expr," is a contradiction."], 
   lasrow=={True},Print["The logical expression ",expr," is a tautology."], 
Length[lasrow]==2, Print["The logical expression
",expr," is a contingency."]]; 
  ];

LogicalTypeCheck::usage=" LogicalTypeCheck[ logicalexpression, variable-list] 
    returns whether 
logicalexpression is a tautology, contradiction, 
  or a contigency (based on the variables in 
variable-list)."
			
(* Examples :
			TruthTable[ p && (q|| !r),{p,q,r}]
			LogicalTypeCheck[ p|| !p,{p}] *)