Re: [open-axiom-devel] [fricas-devel] Re: computation framework

[Gabriel D. R. <gd...@cs...>]

Martin Baker <ax...@ma...> 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