Martin Baker wrote:
>
> I have now implemented the following simplification rules:
>
> ~T -> _|_
> ~(~T) -> T
> ~x /\ x -> _|_
> x /\ ~x -> _|_
> x /\ x -> x
> _|_ /\ x -> _|_
> x /\ _|_ -> _|_
> T \/ x -> T
> x \/ T -> T
>
> in computation.spad.pamphlet at:
> https://github.com/martinbaker/multivector/
I have now commited an updated version. I had to elliminate
a few remaining non-ASCII chars. Also I did a little whitespace
normlization (eliminated tabs and trailing whitespace). And
I have renamed Ski to SKICombinators and changed abbreviations
from COMP to COMPUTIL and SKI to SKICOMB (I feel that originals
were too short and likely to cause conflicts in the future).
There are also rules:
x \/ x -> x
x /\ T -> x
x \/ _|_ -> x
More generaly, Heyting algebra is a lattice, so all usual lattice
simplifications apply. Moreover, Heyting algebra is a distributive
lattice, so distributive law gives more simplifications.
Also
~~~x -> ~x
BTW, there is a bug:
(9) -> ~(~(~proposition("a")))
>> Error detected within library code:
(1 a) cannot be coerced to mode (Record (: val (NonNegativeInteger)))
However, I do not want to delay next release, so we should fix it
after release.
--
Waldek Hebisch
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
