Is a statement of propositional logic always true? 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
Input formulas will use P, P', P'' ect. as variables. They can either be true or false.
(P and P') means both P and P' are true.
(P or P') means at least one of P and 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.
Example input: (P implies ((P' or P'') and P'''))
Output
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)
Test Cases
P: False
(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
and, or, not, and implies are the ONLY operators.
This is code-golf. Shortest program in bytes wins.
Clarification
The type of logic used here is Classical logic.
Retina 0.8.2, 136 124 121 bytes
{T`()`&lt;&gt;
.*P.*
&lt;$&amp; ¶ $&amp;&gt;
(?=(P'*))(?=.*\1[^P']*(¶|$))\1
$.2
¶
a
&lt;not 1&gt;|&lt;0 or 0&gt;|&lt;1 [ai]\w* 0&gt;|&lt;0 a\w* .&gt;|(&lt;[^P&lt;&gt;]*&gt;)
$#1

Try it online! Link includes test cases. Explanation: Works by considering each variable in turn, replacing the string f(p) with the string &lt;f(1) and f(0)&gt; for each variable p. The resulting string is then evaluated according to Boolean arithmetic.
{`

Repeat the entire program until the buffer stops changing.
T`()`&lt;&gt;

Change the ()s to something that doesn't need to be quoted.
.*P.*
&lt;$&amp; ¶ $&amp;&gt;

If the line still contains a variable, then duplicate it, and wrap the whole buffer in &lt;&gt;, however the two copies are still separated by a newline for now.
(?=(P'*))(?=.*\1[^P']*(¶|$))\1
$.2

Replace all copies of the last variable in the line with 1 or 0 depending on whether this is the original or duplicate line.
¶
a

Replace the newline with an a so that the two lines are joined together by an &lt; and &gt; operation.
&lt;not 1&gt;|&lt;0 or 0&gt;|&lt;1 [ai]\w* 0&gt;|&lt;0 a\w* .&gt;|(&lt;[^P&lt;&gt;]*&gt;)
$#1

Simplify any expressions that only contain constants. The expressions &lt;not 1&gt;, &lt;0 or 0&gt;, &lt;1 implies 0&gt;, &lt;1 and 0&gt;, &lt;0 and 0&gt;, &lt;0 and 1&gt; and &lt;0 and P&gt; (edge case) all evaluate to 0, while any other expression that contains no sub-expressions or variables evaluates to 1. (The original version of the code was buggy in this respect and needed a byte to fix it which I have included in the revised byte count in the header.)