Re: [open-axiom-devel] computation framework

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

Martin Baker <ax...@ma...> writes:

| On Monday 20 Jun 2011 18:57:22 Gabriel Dos Reis wrote:
| > If you want to support intuitionistic logic, you cannot simplify
| > double negation.  See my comment in the definition of simplifyOneStep
| > in the package PropositionalFormulaFunctions1
| 
| Gaby,
| 
| So is boolean.spad.pamphlet general enough to support intuitionistic logic?

OpenAxiom, and I believe all flavours of AXIOM, makes implicit use of
classical logic.  So, to avoid surprises, I assumed classical logic in
the simplifier.  However, for that particular algebra, that is easily
fixed by removing the line

   (f1' := isNot f1) case F => f1' -- assume classical logic 

from simplifyOneStep.  If that is done then boolean.spad.pamphlet
is general enough to support intuitionistic logic.
I believe the rules that `dual' uses are OK.

A long time ago, for the purposes of semantics-based program analysis, I
introduced the domain KleeneTrivalentLogic (also in
boolean.spad.pamphlet) which I views as a fairly good compromise
(from computational perspective).  Because of some misguided parser
simplifications (all flavours of AXIOM affected, OpenAxiom much less),
you have to be careful about how you write logical formulae with values
from the domain KleeneTrivalentLogic.

I do think it is possible to make all flavours of AXIOM support
intuitionistic logic.  But:
  -- it is for the long haul; one has to audit almost of the algebra
     (especially the "symbolic" part)

  -- one would have to educate the audiance.  How many people would not
     bark at 

          simplify(x and not x)

     not being simplified?  (that is a test in all AXIOM testsuites I
     believe)  I have not heard complaints from users, but I and my
     students are probably the only one using it :-p

-- Gaby