Martin Baker <[email protected]> writes: [...]
| In other words they seem to be saying that the addition of either Law | of the excluded middle or Double negation elimination have the same | effect of converting intuitionistic logic to classical logic. If you want to support intuitionistic logic, you cannot simplify double negation. See my comment in the definition of simplifyOneStep in the package PropositionalFormulaFunctions1 http://svn.open-axiom.org/viewvc/open-axiom/trunk/src/algebra/boolean.spad.pamphlet?revision=2022&view=markup -- Gaby -- 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.
