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).

Filter by
Sorted by
Tagged with
7 votes
1 answer

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 ...
Reubend's user avatar
  • 519