Martin Baker <ax87...@martinb.com> 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 ------------------------------------------------------------------------------ EditLive Enterprise is the world's most technically advanced content authoring tool. Experience the power of Track Changes, Inline Image Editing and ensure content is compliant with Accessibility Checking. http://p.sf.net/sfu/ephox-dev2dev _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
