Proper.Formula
data Formula s
checkTheorem
neg
con
dis
val
bic
imp
truthAssignment
evalFormula
isValidByTruthTable
toCNF
theorem
bddCheckTaut