Formulae
                             by Gauthier Groult, May 89


          This  code  is  part  of  an  academic project I worked on at the
          University  of  Sciences  of  Paris   7,   Jussieu.   It   is  an
          implementation  of   basic  propositional  formulae  manipulation
          routines in Scheme. An excellent version of Scheme  was ported to
          the Amiga  by Ed  Puckett (MIT  Branch) and  can be found on Fish
          disk #149. Thank you for that, Ed!

          The source file is commented... in french. So  here are  the high
          level functions and what they do:

               empty
                    returns the empty set

               singleton(x)
                    returns a one element set containing x

               add(elem, set)
                    adds the element elem to the set set

               union(set1, set2)
                    returns the union of sets set1 and set2

               inter(set1, set2)
                    returns the intersection of the two sets

               product(set1, set2) 
                    returns  the  cartesian  (Descartes  was french, by the
                    way) product of set1 and set2

               axioms
                    returns a list of  the 14  axioms of  the propositional
                    calculus.  These  are  arbitrary  axioms, they could be
                    replaced by equivalents.

               formula?(f)
                    tests if f is a propositional  formula. See  at the end
                    of this list the conventions used to write formulae.

               vars?(f)
                    Returns a list of the variables contained in f, where f
                    is supposed to be a formula.

               subst(f, v, g)
                    replaces each occurrence of the variable v in  f by the
                    formula g, where f is supposed to be a formula.

               table(varset)
                    returns  the   set  of  all  possible  assignations  of
                    variables in varset to true or false.

               true?(f, a)
                    returns the value of f under a, where f is  supposed to
                    be  a   correct  formula   and  a  correct  assignation
                    (conventions below).

               valid?(f)
                    decides whether  f is  a valid  formula, i.e.  if it is
                    always true.
               refute(f)
                    returns  a  list  of  all  the  assignations refuting f
                    (giving the value false to f), f being a formula.

               sheffer?(f)
                    tests if f satisfies the Sheffer theorem, where  f is a
                    formula.

               shefferize(stroke, name, f)
                    translates any formula f into a formula built only with
                    the new connector  name,  which  itself  represents the
                    Sheffer formula stroke.

          Formulae  are  written  as  postfixed  lists  -  reversed  polish
          notation. The connectors  are  named  "not",  "et",  "ou", "imp",
          "equiv" for  negation, and,  or, implication and equivalency. The
          names can be easily changed to anything else.

          The formula
                              "not a implicates (b and c)" 
          then becomes
                              (imp (non a) (et b c))
          with these rules.

          Assignations are sets (lists)  of two  elements, where  the first
          element is  the variable  and the  second its value: (a #t) is an
          assignation representing the  variable  a  with  the  value true.
          Values can be #t or #f.


          Sheffer formulae  or basically  NANDs and  NORs. You  can try for
          instance "(shefferize '(non (et (a b))) '+ '(ou a b))".


          I hope this will be helpful to someone.