The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 4 Oct 2013 11:56:22 -0700,
t x 
<txrev319 AT gmail.com>
 a écrit :

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

"P ∨ ¬P" is solvable in Coq…
Just take P=True (or False, as you prefer).

I think you mix two things.
SAT solving is finding a valuation (that is a function from litterals
to "bool", which is isomorphic to "True+False").
If you want to get problems with excluded middle, your problem occurs
when you want to show that it holds for ALL valuation (assuming you
take Prop instead of bool), not for A valuation.

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