The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Apr 14, 2016 at 7:00 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
 wrote:
> Thanks, Daniel.
> I was overlooking the fact that the boolean ring in my application is not an
> integral domain.
> So I cannot use nsatz.
> 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.

Would it work to convert to an identity over boolean algebras, then
use a decision procedure for that?  For example, the dumb decision
procedure of trying all combinations of T/F assignments to the atoms
would probably work fine for a small number of atoms.  (Or come to
think of it, you wouldn't even need the translation for that approach
- just try all assignments of 0/1 to the atoms and calculate in the
boolean ring Z/2Z.)

As it happens, I just recently decided to look up the proof of cut
elimination in sequent calculus, and see if I could formalize it in
Coq.  After some false starts, I managed to do so, and I posted the
results on github: https://github.com/dschepler/coq-sequent-calculus .
(Though the current state is fairly messy.)  My hope is eventually to
be able to also prove the completeness of LJT* (as used in the tauto
tactic) for intuitionistic propositional logic, and formalize the
corresponding decision procedure.  Such a development would also apply
to a decision procedure for classical propositional logic, and thus
for boolean algebra identities, via the double-negation translation -
and it would hopefully be more efficient for identities with larger
numbers of atoms.  (However, given the co-NP-completeness of deciding
classical propositional logic identities, you probably can't hope for
an algorithm that's truly efficient in all cases.)
-- 
Daniel Schepler