On Wednesday 22 Jun 2011 19:59:12 Waldek Hebisch wrote: >It seems that: >http://www.philfree.org/IMG/pdf/dyckhoff-ljt.pdf >gives simpler algorithm.
OK thanks, I'll have a read of the Dyckhoff paper. > Using this you can determine equivalence of intuitionistic > formulas. But the algorithm does not work via "simplification > rules"... My idea was to start with a 'free logic algebra' that is an algebra where each combination of inputs to /\ , \/ and ¬ generates a new element. So an expression like T /\ T is just T /\ T and does not simplify. Then by adding what I called "simplification rules" (should I have called them relators?) then other logic algebras could be implemented (intuitional, ternary, many-valued, boolean) just by changing the "rules". These "rules" are hardcoded into the /\ , \/ and ¬ implementations (rather than implementing a true rule based system). I thought that the 'free logic algebra' could be a category, then intuitional, ternary, many-valued, boolean could be domains which overload /\ , \/ and ¬ with their own sets of rules. 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.
