I also found another way:
"In a complete logic, a formula is contradictory if and only if it is unsatisfiable". Source
In that case, we can check if the proposition is satisfiable and after negate the result. If the output is True
that means that the original statement was unsatisfiable which also means that it was contradiction. If the output was False
it means that the result was satisfiable, which means that it was tautology or contingency.
For example, lets check if p && !p
is contradiction:
Not[SatisfiableQ[p && ! p, {p}]]
output:
True
It means that p && !p
is contradiction.
Lets check if p || ! p
is contradiction:
Not[SatisfiableQ[p || ! p, {p}]]
output:
False
It means that p || ! p
is not contradiction. The output does not say that but it is tautology.
Lets check if p && q
is contradiction:
Not[SatisfiableQ[p && q, {p, q}]]
output:
False
It means that p && q
is not contradiction. The output does not say that but it is contingency.