The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I want to understand algorithms for solving propositional logic in Coq.

  The initial thing I did was read up on SAT solvers, which was rather insightful. However, this does not appear to relate to Coq Props because I don't have the law of excluded middle (which many SAT solvers) appear to rely on. (In particular, P \/ ~P is solvable in SAT but not in Coq).

  Thus, my question: what algorithm can be used to solve propositional logic in Coq?

Thanks!