Question: Simplifying arithmetic modulo 2 - Propositional logic

Dear maple team.

I would like to suggest something about the treatment that Maple makes of arithmetic modulo 2.
If you write the command:"x+x mod 2", the Maple output is "0", because "x+x" is always even. Perfect.
The problem I have is:
When  you write "x^2 + x mod 2", the Maple output is "x^2 + x"  instead of "0". Maple doesn't takes into account when simplifying that all the variables are idempotent modulo 2 (i.e, x*x = x)

If I write
" EXPRESION mod 2"   
(where 'EXPRESION' is a set of sums and multiplications on the variables (a,b,c,d))
the Maple output is:
" a*b*c+a^2*c*d+d+c^2*d^2*a^2*b^2+d^2*a*b^2*c+d^2*a*b^2+a*c+c*d+d*b+d*a^2*b*c+c+c^2+d^2*a^2*c+d^2*a^2*b^2*c+d^2*b^2+d^2*a+
d^2+b*c^2+c^2*d^2+b*c^2*d+a^2*c^2*b*d+c^2*d^2*a^2+c*d*a*b+a*b^2*c*d+b^2*c*d+b^2*c^2*d+d^2*a*c+a^2*b^2*c^2*d+b*c+d*a*b+d*a+
a^2*c^2+a^2*c^2*b+c^2*d^2*b^2 "

Then I have to get this expression and eliminate the powers manually:
" EXPRESION:= a*b*c+a*c*d+d+c*d*a*b+d*a*b*c+d*a*b+a*c+c*d+d*b+d*a*b*c+c+c+d*a*c+d*a*b*c+d*b+d*a+
d+b*c+c*d+b*c*d+a*c*b*d+c*d*a+c*d*a*b+a*b*c*d+b*c*d+b*c*d+d*a*c+a*b*c*d+b*c+d*a*b+d*a+a*c+a*c*b+c*d*b "
(this is the output calculated by Maple without the powers)

And then, finally, if I write:
" EXPRESION mod 2 "  I have my desired "0" .

This is important to me because I'm working with propositional logic as arithmetic modulo 2, so I have:
true  proposition <-> even number   <->  0 mod 2
false proposition <-> odd n umber   <->  1 mod 2
And the connectives are defined as:
p or q   := p*q
~p       := 1+p
p and q  := 1 + (1+p)*(1+q)
p->q      := (1+p)*q
and so on.

So if I have to prove this theorem:
(a or b) ->{ (a->a') and (b->b')} -> a'or b' }
Maple calculates:
c^2*d^2*a^2*b+c^2*d^2*a+c^2*d^2*a^2*b^2+c^2*d*a^2*b+c^2*d*a+c^2*d^2+c^2*d^2*b^2*a+c^2*d^2*b+c^2*d*a*b+c^2*d+c*a*d^2*b+c*d^2+c*a*d^2*b^2+c*d^2*b+c*a*d*b+c*d
when indeed it's value is "0", that is: is TRUE.

Best regards

 

Please Wait...