coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities
Chronological Thread
- From: Laurent Thery <Laurent.Thery AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities
- Date: Fri, 15 Apr 2016 11:39:12 +0200
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
- [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Pierre-Marie Pédrot, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/16/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/16/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/16/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Assia Mahboubi, 04/19/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
Archive powered by MHonArc 2.6.18.