Martin Baker wrote: > > 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. > I am not sure if a "complete" system of simplification rules is known. What is known is an algorithm to determine validity of intuitionistic formula, see for example:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.7751 Using this you can determine equivalence of intuitionistic formulas. But the algorithm does not work via "simplification rules"... -- 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.
