Questions tagged [contradiction]
Most of the time, a proposition ϕ is a contradiction if assuming there is a proof of false, hence if the hypothetical judgement ϕ ⊢ ⊥ is valid. (from nLab).
1
question
7
votes
1
answer
122
views
Understanding "saturating" theorem provers
The documentation for the E Theorem Prover explains this as the first step in its process:
A clausification algorithm translates first-order input into clause
normal form, such that the resulting ...
- 519