On Monday 20 Jun 2011 18:49:32 Waldek Hebisch wrote: > The quotes look correct. Consider: > > x -> --x (Doble negation introduction) means that > > T -> --T which in turn means T = --T > > OTOH if you know that --x = T you can not infer that x is T > (this is another way of saying that you can not eliminate > double negation). > > To say this differently: --T = T but there are x such that > --x ~= x.
OK, Thanks for you patience, I am with you now. So, just to summarise, I think that the version of computation.spad.pamphlet at: https://github.com/martinbaker/multivector/ that I uploaded yesterday is 'correct' (no longer has ?) but does not have all simplifications. I think that I can implement the following simplification rules today: ~T -> _|_ ~(~T) -> T ~x /\ x -> _|_ x /\ ~x -> _|_ x /\ x -> x _|_ /\ x -> _|_ x /\ _|_ -> _|_ T \/ x -> T x \/ T -> T but it would take me a lot longer to work out and implement a complete list of simplification rules without help. >From what Gaby says, there seems to be scope to integrate this with boolean.spad.pamphlet code but that would be a very long term project. Martin -- 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.
