All Questions
Tagged with automated-theorem-proving contradiction
1
question
7
votes
1
answer
142
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 ...