The challenge is to golf a program that checks if a statement of propositional calculus/logic is a logical tautology (i.e. it is true for all possible values of the variables).
Input formulas will use
P'' ect. as variables. They can either be true or false.
(P and P') means both
P' are true.
(P or P') means at least one of
P' is true.
(P implies P') means that if
P is true, than
P' must be true.
(not P) means that P is false.
These forms can be nested.
(P implies ((P' or P'') and P'''))
Output will be a truthy value if the input is a tautology, and a falsy value if it is not. (i.e True/False 1/0)
(P implies P): True
((P implies P') implies ((P' implies P'') implies (P implies P''))): True
(P implies (P or P')): True
(P implies (P and P')): False
(P or (not P)): True
implies are the ONLY operators.
This is code-golf. Shortest program in bytes wins.
The type of logic used here is Classical logic.