The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

> It seems that I now have the complete decision procedure (for boolean
> rings) that I was looking for, except that I may have run into a bug in
> nsatz.
> I have illustrated it in the lemma nsatzNotComplete below, where nsatz
> fails unexpectedly and succeeds if I reorder a hypothesis.
> Is this a known limitation of nsatz, or just a bug?

It looks like a bug. I look into it.


> I can use the ring tactic with the additional equations for all
> variables, but I was hoping for a complete decision procedure for
> unquantified equations in a boolean ring.

Maybe I am missing something here but as

x = y can be encoded as x + y + 1
and
x -> y as x * y + y + 1

can you just turn your equational problem into a tautology checking that 
can be solved by ring plus the basic equations x * x = x and x + x = 0 
on variables?

--
Laurent