* algebra/logic.spad.pamphlet: New file.

	* algebra/boolean.spad.pamphlet (Logic): Move there.
	(BooleanLogic): Likewise.
	(PropositionalLogic): Likewise.
	(PropositionalFormula): Likewise.
	(PropositionalFormulaFunctions1): Likewise.
	(PropositionalFormulaFunctions2): Likewise.
	(KleeneTrivalentLogic): Likewise.

4 files changed, 558 insertions, 497 deletions

diff --git a/src/algebra/Makefile.am b/src/algebra/Makefile.am
index 536cbed8..ae00743b 100644
--- a/src/algebra/Makefile.am
+++ b/src/algebra/Makefile.am
@@ -1091,7 +1091,7 @@ SPADFILES= \
  $(OUTSRC)/lie.spad $(OUTSRC)/limitps.spad $(OUTSRC)/lindep.spad \
  $(OUTSRC)/lingrob.spad $(OUTSRC)/liouv.spad $(OUTSRC)/listgcd.spad \
  $(OUTSRC)/list.spad $(OUTSRC)/lmdict.spad $(OUTSRC)/lodof.spad \
- $(OUTSRC)/lodop.spad $(OUTSRC)/lodo.spad \
+ $(OUTSRC)/lodop.spad $(OUTSRC)/lodo.spad $(OUTSRC)/logic.spad \
  $(OUTSRC)/manip.spad $(OUTSRC)/mappkg.spad $(OUTSRC)/matcat.spad \
  $(OUTSRC)/matfuns.spad $(OUTSRC)/mathml.spad \
  $(OUTSRC)/matrix.spad $(OUTSRC)/matstor.spad \
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index dcdf0562..3ad4b2ff 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -12,386 +12,6 @@
 \tableofcontents
 \eject
 
-\section{Categories an domains for logic}
-
-<<category BOOLE BooleanLogic>>=
-)abbrev category BOOLE BooleanLogic
-++ Author: Gabriel Dos Reis
-++ Date Created: April 04, 2010
-++ Date Last Modified: April 04, 2010
-++ Description:
-++   This is the category of Boolean logic structures.
-BooleanLogic(): Category == Logic with
-    not: % -> %
-      ++ \spad{not x} returns the complement or negation of \spad{x}.
-    and: (%,%) -> %
-      ++ \spad{x and y} returns the conjunction of \spad{x} and \spad{y}.
-    or: (%,%) -> %
-      ++ \spad{x or y} returns the disjunction of \spad{x} and \spad{y}.
-  add
-    not x == ~ x
-    x and y == x /\ y
-    x or y == x \/ y
-@
-
-<<category PROPLOG PropositionalLogic>>=
-)abbrev category PROPLOG PropositionalLogic
-++ Author: Gabriel Dos Reis
-++ Date Created: Januray 14, 2008
-++ Date Last Modified: May 27, 2009
-++ Description: This category declares the connectives of
-++ Propositional Logic.
-PropositionalLogic(): Category == Join(BooleanLogic,SetCategory) with
-  true: %
-    ++ true is a logical constant.
-  false: %
-    ++ false is a logical constant.
-  implies: (%,%) -> %
-    ++ implies(p,q) returns the logical implication of `q' by `p'.
-  equiv: (%,%) -> %
-    ++ equiv(p,q) returns the logical equivalence of `p', `q'.
-@
-
-\section{domain PROPFRML PropositionalFormula}
-<<domain PROPFRML PropositionalFormula>>=
-)set mess autoload on
-)abbrev domain PROPFRML PropositionalFormula
-++ Author: Gabriel Dos Reis
-++ Date Created: Januray 14, 2008
-++ Date Last Modified: February, 2011
-++ Description: This domain implements propositional formula build
-++ over a term domain, that itself belongs to PropositionalLogic
-PropositionalFormula(T: SetCategory): Public == Private where
-  Public == Join(PropositionalLogic, CoercibleFrom T) with
-    isAtom : % -> Maybe T
-      ++ \spad{isAtom f} returns a value \spad{v} such that
-      ++ \spad{v case T} holds if the formula \spad{f} is a term.
-
-    isNot : % -> Maybe %
-      ++ \spad{isNot f} returns a value \spad{v} such that
-      ++ \spad{v case %} holds if the formula \spad{f} is a negation.
-
-    isAnd : % -> Maybe Pair(%,%)
-      ++ \spad{isAnd f} returns a value \spad{v} such that 
-      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
-      ++ is a conjunction formula.
-
-    isOr : % -> Maybe Pair(%,%)
-      ++ \spad{isOr f} returns a value \spad{v} such that 
-      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
-      ++ is a disjunction formula.
-
-    isImplies : % -> Maybe Pair(%,%)
-      ++ \spad{isImplies f} returns a value \spad{v} such that 
-      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
-      ++ is an implication formula.
-
-    isEquiv : % -> Maybe Pair(%,%)
-      ++ \spad{isEquiv f} returns a value \spad{v} such that 
-      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
-      ++ is an equivalence formula.
-
-    conjunction: (%,%) -> %
-      ++ \spad{conjunction(p,q)} returns a formula denoting the
-      ++ conjunction of \spad{p} and \spad{q}.
-
-    disjunction: (%,%) -> %
-      ++ \spad{disjunction(p,q)} returns a formula denoting the
-      ++ disjunction of \spad{p} and \spad{q}.
-
-  Private == add
-    Rep == Union(T, Kernel %)
-    import Kernel %
-    import BasicOperator
-    import KernelFunctions2(Identifier,%)
-    import List %
-
-    -- Local names for proposition logical operators
-    macro FALSE == '%false
-    macro TRUE == '%true
-    macro NOT == '%not
-    macro AND == '%and
-    macro OR == '%or
-    macro IMP == '%implies
-    macro EQV == '%equiv
-
-    -- Return the nesting level of a formula
-    level(f: %): NonNegativeInteger ==
-      f' := rep f
-      f' case T => 0
-      height f'
-
-    -- A term is a formula
-    coerce(t: T): % == 
-      per t
-
-    false == per constantKernel FALSE
-    true == per constantKernel TRUE
-
-    ~ p ==
-      per kernel(operator(NOT, 1::Arity), [p], 1 + level p)
-
-    conjunction(p,q) ==
-      per kernel(operator(AND, 2), [p, q], 1 + max(level p, level q))
-
-    p /\ q == conjunction(p,q)
-
-    disjunction(p,q) ==
-      per kernel(operator(OR, 2), [p, q], 1 + max(level p, level q))
-
-    p \/ q == disjunction(p,q)
-
-    implies(p,q) ==
-      per kernel(operator(IMP, 2), [p, q], 1 + max(level p, level q))
-
-    equiv(p,q) ==
-      per kernel(operator(EQV, 2), [p, q], 1 + max(level p, level q))
-
-    isAtom f ==
-      f' := rep f
-      f' case T => just(f'@T)
-      nothing
-
-    isNot f ==
-      f' := rep f
-      f' case Kernel(%) and is?(f', NOT) => just(first argument f')
-      nothing
-
-    isBinaryOperator(f: Kernel %, op: Symbol): Maybe Pair(%, %) ==
-      not is?(f, op) => nothing
-      args := argument f
-      just pair(first args, second args)
-
-    isAnd f ==
-      f' := rep f
-      f' case Kernel % => isBinaryOperator(f', AND)
-      nothing
-
-    isOr f ==
-      f' := rep f
-      f' case Kernel % => isBinaryOperator(f', OR)
-      nothing
-
-    isImplies f ==
-      f' := rep f
-      f' case Kernel % => isBinaryOperator(f', IMP)
-      nothing
-
-
-    isEquiv f ==
-      f' := rep f
-      f' case Kernel % => isBinaryOperator(f', EQV)
-      nothing
-
-    -- Unparsing grammar.
-    --
-    -- Ideally, the following syntax would the external form
-    -- Formula:
-    --   EquivFormula
-    --
-    -- EquivFormula:
-    --   ImpliesFormula
-    --   ImpliesFormula <=> EquivFormula
-    --
-    -- ImpliesFormula:
-    --   OrFormula
-    --   OrFormula => ImpliesFormula
-    --
-    -- OrFormula:
-    --   AndFormula
-    --   AndFormula or OrFormula 
-    -- 
-    -- AndFormula
-    --   NotFormula
-    --   NotFormula and AndFormula
-    --
-    -- NotFormula:
-    --   PrimaryFormula
-    --   not NotFormula
-    --
-    -- PrimaryFormula:
-    --   Term
-    --   ( Formula )
-    --
-    -- Note: Since the token '=>' already means a construct different
-    --       from what we would like to have as a notation for
-    --       propositional logic, we will output the formula `p => q'
-    --       as implies(p,q), which looks like a function call.
-    --       Similarly, we do not have the token `<=>' for logical
-    --       equivalence; so we unparser `p <=> q' as equiv(p,q).
-    --
-    --       So, we modify the nonterminal PrimaryFormula to read
-    --       PrimaryFormula:
-    --         Term
-    --         implies(Formula, Formula)
-    --         equiv(Formula, Formula)
-    formula: % -> OutputForm
-    coerce(p: %): OutputForm ==
-      formula p
-
-    primaryFormula(p: %): OutputForm ==
-      p' := rep p
-      p' case T => p'@T::OutputForm
-      case constantIfCan p' is
-        c@Identifier => c::OutputForm
-        otherwise =>
-          is?(p', IMP) or is?(p', EQV) =>
-            args := argument p'
-            elt(operator(p')::OutputForm, 
-                  [formula first args, formula second args])$OutputForm
-          paren(formula p)$OutputForm
-
-    notFormula(p: %): OutputForm ==
-      case isNot p is
-        f@% => elt(outputForm 'not, [notFormula f])$OutputForm
-        otherwise => primaryFormula p
-
-    andFormula(f: %): OutputForm ==
-      case isAnd f is
-	p@Pair(%,%) =>
-          -- ??? idealy, we should be using `and$OutputForm' but
-          -- ??? a bug in the compiler currently prevents that.
-          infix(outputForm 'and, notFormula first p,
-             andFormula second p)$OutputForm
-        otherwise => notFormula f
-
-    orFormula(f: %): OutputForm ==
-      case isOr f is
-        p@Pair(%,%) => 
-          -- ??? idealy, we should be using `or$OutputForm' but
-          -- ??? a bug in the compiler currently prevents that.
-          infix(outputForm 'or, andFormula first p, 
-             orFormula second p)$OutputForm
-        otherwise => andFormula f
-
-    formula f ==
-      -- Note: this should be equivFormula, but see the explanation above.
-      orFormula f
-
-@
-
-<<package PROPFUN1 PropositionalFormulaFunctions1>>=
-)abbrev package PROPFUN1 PropositionalFormulaFunctions1
-++ Author: Gabriel Dos Reis
-++ Date Created: April 03, 2010
-++ Date Last Modified: April 03, 2010
-++ Description:
-++   This package collects unary functions operating on propositional
-++   formulae.
-PropositionalFormulaFunctions1(T): Public == Private where
-  T: SetCategory
-  Public == Type with
-    dual: PropositionalFormula T -> PropositionalFormula T
-      ++ \spad{dual f} returns the dual of the proposition \spad{f}.
-    atoms: PropositionalFormula T -> Set T
-      ++ \spad{atoms f} ++ returns the set of atoms appearing in
-      ++ the formula \spad{f}.
-    simplify: PropositionalFormula T -> PropositionalFormula T
-      ++ \spad{simplify f} returns a formula logically equivalent
-      ++ to \spad{f} where obvious tautologies have been removed.
-  Private == add
-    macro F == PropositionalFormula T
-    inline Pair(F,F)
-
-    dual f ==
-      f = true$F => false$F
-      f = false$F => true$F
-      isAtom f case T => f
-      (f1 := isNot f) case F => not dual f1
-      (f2 := isAnd f) case Pair(F,F) =>
-         disjunction(dual first f2, dual second f2)
-      (f2 := isOr f) case Pair(F,F) =>
-         conjunction(dual first f2, dual second f2)
-      error "formula contains `equiv' or `implies'"
-
-    atoms f ==
-      (t := isAtom f) case T => { t }
-      (f1 := isNot f) case F => atoms f1
-      (f2 := isAnd f) case Pair(F,F) =>
-         union(atoms first f2, atoms second f2)
-      (f2 := isOr f) case Pair(F,F) =>
-         union(atoms first f2, atoms second f2)
-      empty()$Set(T)
-
-    -- one-step simplification helper function
-    simplifyOneStep(f: F): F ==
-      (f1 := isNot f) case F =>
-        f1 = true$F => false$F
-        f1 = false$F => true$F
-        (f1' := isNot f1) case F => f1'         -- assume classical logic
-        f
-      (f2 := isAnd f) case Pair(F,F) =>
-        first f2 = false$F or second f2 = false$F => false$F
-        first f2 = true$F => second f2
-        second f2 = true$F => first f2
-        f
-      (f2 := isOr f) case Pair(F,F) =>
-        first f2 = false$F => second f2
-        second f2 = false$F => first f2
-        first f2 = true$F or second f2 = true$F => true$F
-        f
-      (f2 := isImplies f) case Pair(F,F) =>
-        first f2 = false$F or second f2 = true$F => true$F
-        first f2 = true$F => second f2
-        second f2 = false$F => not first f2
-        f
-      (f2 := isEquiv f) case Pair(F,F) =>
-        first f2 = true$F => second f2
-        second f2 = true$F => first f2
-        first f2 = false$F => not second f2
-        second f2 = false$F => not first f2
-        f
-      f
-
-    simplify f ==
-      (f1 := isNot f) case F => simplifyOneStep(not simplify f1)
-      (f2 := isAnd f) case Pair(F,F) =>
-        simplifyOneStep(conjunction(simplify first f2, simplify second f2))
-      (f2 := isOr f) case Pair(F,F) =>
-        simplifyOneStep(disjunction(simplify first f2, simplify second f2))
-      (f2 := isImplies f) case Pair(F,F) =>
-        simplifyOneStep(implies(simplify first f2, simplify second f2))
-      (f2 := isEquiv f) case Pair(F,F) =>
-        simplifyOneStep(equiv(simplify first f2, simplify second f2))
-      f
-@
-
-<<package PROPFUN2 PropositionalFormulaFunctions2>>=
-)abbrev package PROPFUN2 PropositionalFormulaFunctions2
-++ Author: Gabriel Dos Reis
-++ Date Created: April 03, 2010
-++ Date Last Modified: April 03, 2010
-++ Description:
-++   This package collects binary functions operating on propositional
-++   formulae.
-PropositionalFormulaFunctions2(S,T): Public == Private where
-  S: SetCategory
-  T: SetCategory
-  Public == Type with
-    map: (S -> T, PropositionalFormula S) -> PropositionalFormula T
-      ++ \spad{map(f,x)} returns a propositional formula where
-      ++ all atoms in \spad{x} have been replaced by the result
-      ++ of applying the function \spad{f} to them.
-  Private == add
-    macro FS == PropositionalFormula S
-    macro FT == PropositionalFormula T
-    map(f,x) ==
-      x = true$FS => true$FT
-      x = false$FS => false$FT
-      (t := isAtom x) case S => f(t)::FT
-      (f1 := isNot x) case FS => not map(f,f1)
-      (f2 := isAnd x) case Pair(FS,FS) =>
-         conjunction(map(f,first f2), map(f,second f2))
-      (f2 := isOr x) case Pair(FS,FS) =>
-         disjunction(map(f,first f2), map(f,second f2))
-      (f2 := isImplies x) case Pair(FS,FS) =>
-         implies(map(f,first f2), map(f,second f2))
-      (f2 := isEquiv x) case Pair(FS,FS) =>
-         equiv(map(f,first f2), map(f,second f2))
-      error "invalid propositional formula"
-
-@
-
 \section{domain REF Reference}
 <<domain REF Reference>>=
 )abbrev domain REF Reference
@@ -429,32 +49,6 @@ Reference(S:Type): SetCategory with
 
 @
 
-\section{category LOGIC Logic}
-
-<<category LOGIC Logic>>=
-)abbrev category LOGIC Logic
-++ Author: 
-++ Date Created:
-++ Date Last Changed: May 27, 2009
-++ Basic Operations: ~, /\, \/
-++ Related Constructors:
-++ Keywords: boolean
-++ Description:  
-++ `Logic' provides the basic operations for lattices,
-++ e.g., boolean algebra.
-
-
-Logic: Category == Type with
-       ~:        % -> %
-	++ ~(x) returns the logical complement of x.
-       /\:       (%, %) -> %
-	++ \spadignore { /\ }returns the logical `meet', e.g. `and'.
-       \/:       (%, %) -> %
-	++ \spadignore{ \/ } returns the logical `join', e.g. `or'.
-  add
-    x \/ y == ~(~x /\ ~y)
-
-@
 \section{domain BOOLEAN Boolean}
 <<domain BOOLEAN Boolean>>=
 )abbrev domain BOOLEAN Boolean
@@ -605,81 +199,6 @@ Bits(): Exports == Implementation where
 
 @
 
-
-\section{Kleene's Three-Valued Logic}
-<<domain KTVLOGIC KleeneTrivalentLogic>>=
-)abbrev domain KTVLOGIC KleeneTrivalentLogic
-++ Author: Gabriel Dos Reis
-++ Date Created: September 20, 2008
-++ Date Last Modified: January 14, 2012
-++ Description: 
-++   This domain implements Kleene's 3-valued propositional logic.
-KleeneTrivalentLogic(): Public == Private where
-  Public == Join(PropositionalLogic,Finite) with
-    unknown: %     ++ the indefinite `unknown' 
-    case: (%,[| false |]) -> Boolean
-      ++ x case false holds if the value of `x' is `false'
-    case: (%,[| unknown |]) -> Boolean
-      ++ x case unknown holds if the value of `x' is `unknown'
-    case: (%,[| true |]) -> Boolean
-      ++ s case true holds if the value of `x' is `true'.
-  Private == Maybe Boolean add
-    false == per just(false@Boolean)
-    unknown == per nothing
-    true == per just(true@Boolean)
-    x = y == rep x = rep y
-    x case true == x = true@%
-    x case false == x = false@%
-    x case unknown == x = unknown
-
-    not x ==
-      x case false => true
-      x case unknown => unknown
-      false
-
-    x and y ==
-      x case false => false
-      x case unknown =>
-        y case false => false
-        unknown
-      y
-
-    x or y ==
-      x case false => y
-      x case true => x
-      y case true => y
-      unknown
-
-    implies(x,y) ==
-      x case false => true
-      x case true => y
-      y case true => true
-      unknown
-
-    equiv(x,y) ==
-      x case unknown => x
-      x case true => y
-      not y
-
-    coerce(x: %): OutputForm ==
-      case rep x is
-        y@Boolean => y::OutputForm
-        otherwise => outputForm 'unknown
-
-    size() == 3
-
-    index n ==
-      n > 3 => error "index: argument out of bound"
-      n = 1 => false
-      n = 2 => unknown
-      true
-
-    lookup x ==
-      x = false => 1
-      x = unknown => 2
-      3
-@
-
 \section{License}
 
 <<license>>=
diff --git a/src/algebra/cycles.spad.pamphlet b/src/algebra/cycles.spad.pamphlet
index 7b1b7c0d..0a92b83a 100644
--- a/src/algebra/cycles.spad.pamphlet
+++ b/src/algebra/cycles.spad.pamphlet
@@ -54,15 +54,15 @@ CycleIndicators: Exports == Implementation where
       ++\spad{alternating n} is the cycle index of the
       ++ alternating group of degree n.
  
-    cyclic: PI -> SPOL RN    --cyclic group
+    cyclic: NNI -> SPOL RN    --cyclic group
       ++\spad{cyclic n} is the cycle index of the
       ++ cyclic group of degree n.
  
-    dihedral: PI -> SPOL RN    --dihedral group
+    dihedral: NNI -> SPOL RN    --dihedral group
       ++\spad{dihedral n} is the cycle index of the
       ++ dihedral group of degree n.
  
-    graphs: PI -> SPOL RN
+    graphs: NNI -> SPOL RN
       ++\spad{graphs n} is the cycle index of the group induced on
       ++ the edges of a graph by applying the symmetric function to the
       ++ n nodes.
@@ -100,24 +100,20 @@ CycleIndicators: Exports == Implementation where
     trm: PTN -> SPOL RN
     trm pt == monomial(inv(pdct(pt) :: RN),pt)
  
-    list: Stream PTN -> L PTN
-    list st == entries complete st
- 
     complete i ==
       i=0 => 1
-      +/[trm pt for pt in list partitions i]
- 
- 
-    even?: PTN -> B
-    even? p == even?( #([i for i in parts p | even? i]))
+      +/[trm pt for pt in entries partitions i]
+  
+    even?: L I -> B
+    even? li == even?( #([i for i in li | even? i]))
  
     alternating i ==
-      2 * _+/[trm p for p in list partitions i | even? p]
+      2 * _+/[trm p for p in entries partitions i | even? p]
 
     elementary i ==
        i=0 => 1
-       +/[(spol := trm pt; even? pt => spol; -spol)
-                          for pt in list partitions i]
+       +/[(spol := trm partition pt; even? pt => spol; -spol)
+                          for pt in entries partitions i]
  
     divisors: I -> L I
     divisors n ==
@@ -161,7 +157,7 @@ CycleIndicators: Exports == Implementation where
         prod := c * prod2 * prod
       xx * prod
  
-    graphs n == +/[trm2 p for p in list(partitions n)]
+    graphs n == +/[trm2 p for p in entries partitions n]
  
     cupp: (PTN,SPOL RN) -> SPOL RN
     cupp(pt,spol) ==
diff --git a/src/algebra/logic.spad.pamphlet b/src/algebra/logic.spad.pamphlet
new file mode 100644
index 00000000..895051f2
--- /dev/null
+++ b/src/algebra/logic.spad.pamphlet
@@ -0,0 +1,546 @@
+\documentclass{article}
+\usepackage{open-axiom}
+
+\title{src/algebra logic.spad}
+\author{Gabriel Dos~Reis}
+
+\section{category LOGIC Logic}
+
+<<category LOGIC Logic>>=
+)abbrev category LOGIC Logic
+++ Author: 
+++ Date Created:
+++ Date Last Changed: May 27, 2009
+++ Basic Operations: ~, /\, \/
+++ Related Constructors:
+++ Keywords: boolean
+++ Description:  
+++   `Logic' provides the basic operations for lattices,
+++   e.g., boolean algebra.
+Logic: Category == Type with
+    ~:        % -> %
+     ++ \spad{~x} returns the logical complement of \spad{x}.
+    /\:       (%, %) -> %
+     ++ \spad {x/\y} returns the logical `meet', e.g. conjunction, of
+     ++ \spad{x} and \spad{y}.
+    \/:       (%, %) -> %
+     ++ \spad{x\/y} returns the logical `join', e.g. disjunction, or
+     ++ \spad{x} and \spad{y}.
+  add
+    x \/ y == ~(~x /\ ~y)
+
+@
+
+\section{Categories an domains for logic}
+
+<<category BOOLE BooleanLogic>>=
+)abbrev category BOOLE BooleanLogic
+++ Author: Gabriel Dos Reis
+++ Date Created: April 04, 2010
+++ Date Last Modified: April 04, 2010
+++ Description:
+++   This is the category of Boolean logic structures.
+BooleanLogic(): Category == Logic with
+    not: % -> %
+      ++ \spad{not x} returns the complement or negation of \spad{x}.
+    and: (%,%) -> %
+      ++ \spad{x and y} returns the conjunction of \spad{x} and \spad{y}.
+    or: (%,%) -> %
+      ++ \spad{x or y} returns the disjunction of \spad{x} and \spad{y}.
+  add
+    not x == ~ x
+    x and y == x /\ y
+    x or y == x \/ y
+@
+
+<<category PROPLOG PropositionalLogic>>=
+)abbrev category PROPLOG PropositionalLogic
+++ Author: Gabriel Dos Reis
+++ Date Created: Januray 14, 2008
+++ Date Last Modified: May 27, 2009
+++ Description: This category declares the connectives of
+++ Propositional Logic.
+PropositionalLogic(): Category == Join(BooleanLogic,SetCategory) with
+  true: %
+    ++ \spad{true} is a logical constant.
+  false: %
+    ++ \spad{false} is a logical constant.
+  implies: (%,%) -> %
+    ++ \spad{implies(p,q)} returns the logical implication of `q' by `p'.
+  equiv: (%,%) -> %
+    ++ \spad{equiv(p,q)} returns the logical equivalence of `p', `q'.
+@
+
+\section{domain PROPFRML PropositionalFormula}
+<<domain PROPFRML PropositionalFormula>>=
+)set mess autoload on
+)abbrev domain PROPFRML PropositionalFormula
+++ Author: Gabriel Dos Reis
+++ Date Created: Januray 14, 2008
+++ Date Last Modified: February, 2011
+++ Description: This domain implements propositional formula build
+++ over a term domain, that itself belongs to PropositionalLogic
+PropositionalFormula(T: SetCategory): Public == Private where
+  Public == Join(PropositionalLogic, CoercibleFrom T) with
+    isAtom : % -> Maybe T
+      ++ \spad{isAtom f} returns a value \spad{v} such that
+      ++ \spad{v case T} holds if the formula \spad{f} is a term.
+
+    isNot : % -> Maybe %
+      ++ \spad{isNot f} returns a value \spad{v} such that
+      ++ \spad{v case %} holds if the formula \spad{f} is a negation.
+
+    isAnd : % -> Maybe Pair(%,%)
+      ++ \spad{isAnd f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is a conjunction formula.
+
+    isOr : % -> Maybe Pair(%,%)
+      ++ \spad{isOr f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is a disjunction formula.
+
+    isImplies : % -> Maybe Pair(%,%)
+      ++ \spad{isImplies f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is an implication formula.
+
+    isEquiv : % -> Maybe Pair(%,%)
+      ++ \spad{isEquiv f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is an equivalence formula.
+
+    conjunction: (%,%) -> %
+      ++ \spad{conjunction(p,q)} returns a formula denoting the
+      ++ conjunction of \spad{p} and \spad{q}.
+
+    disjunction: (%,%) -> %
+      ++ \spad{disjunction(p,q)} returns a formula denoting the
+      ++ disjunction of \spad{p} and \spad{q}.
+
+  Private == add
+    Rep == Union(T, Kernel %)
+    import Kernel %
+    import BasicOperator
+    import KernelFunctions2(Identifier,%)
+    import List %
+
+    -- Local names for proposition logical operators
+    macro FALSE == '%false
+    macro TRUE == '%true
+    macro NOT == '%not
+    macro AND == '%and
+    macro OR == '%or
+    macro IMP == '%implies
+    macro EQV == '%equiv
+
+    -- Return the nesting level of a formula
+    level(f: %): NonNegativeInteger ==
+      f' := rep f
+      f' case T => 0
+      height f'
+
+    -- A term is a formula
+    coerce(t: T): % == 
+      per t
+
+    false == per constantKernel FALSE
+    true == per constantKernel TRUE
+
+    ~ p ==
+      per kernel(operator(NOT, 1::Arity), [p], 1 + level p)
+
+    conjunction(p,q) ==
+      per kernel(operator(AND, 2), [p, q], 1 + max(level p, level q))
+
+    p /\ q == conjunction(p,q)
+
+    disjunction(p,q) ==
+      per kernel(operator(OR, 2), [p, q], 1 + max(level p, level q))
+
+    p \/ q == disjunction(p,q)
+
+    implies(p,q) ==
+      per kernel(operator(IMP, 2), [p, q], 1 + max(level p, level q))
+
+    equiv(p,q) ==
+      per kernel(operator(EQV, 2), [p, q], 1 + max(level p, level q))
+
+    isAtom f ==
+      f' := rep f
+      f' case T => just(f'@T)
+      nothing
+
+    isNot f ==
+      f' := rep f
+      f' case Kernel(%) and is?(f', NOT) => just(first argument f')
+      nothing
+
+    isBinaryOperator(f: Kernel %, op: Symbol): Maybe Pair(%, %) ==
+      not is?(f, op) => nothing
+      args := argument f
+      just pair(first args, second args)
+
+    isAnd f ==
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', AND)
+      nothing
+
+    isOr f ==
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', OR)
+      nothing
+
+    isImplies f ==
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', IMP)
+      nothing
+
+
+    isEquiv f ==
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', EQV)
+      nothing
+
+    -- Unparsing grammar.
+    --
+    -- Ideally, the following syntax would the external form
+    -- Formula:
+    --   EquivFormula
+    --
+    -- EquivFormula:
+    --   ImpliesFormula
+    --   ImpliesFormula <=> EquivFormula
+    --
+    -- ImpliesFormula:
+    --   OrFormula
+    --   OrFormula => ImpliesFormula
+    --
+    -- OrFormula:
+    --   AndFormula
+    --   AndFormula or OrFormula 
+    -- 
+    -- AndFormula
+    --   NotFormula
+    --   NotFormula and AndFormula
+    --
+    -- NotFormula:
+    --   PrimaryFormula
+    --   not NotFormula
+    --
+    -- PrimaryFormula:
+    --   Term
+    --   ( Formula )
+    --
+    -- Note: Since the token '=>' already means a construct different
+    --       from what we would like to have as a notation for
+    --       propositional logic, we will output the formula `p => q'
+    --       as implies(p,q), which looks like a function call.
+    --       Similarly, we do not have the token `<=>' for logical
+    --       equivalence; so we unparser `p <=> q' as equiv(p,q).
+    --
+    --       So, we modify the nonterminal PrimaryFormula to read
+    --       PrimaryFormula:
+    --         Term
+    --         implies(Formula, Formula)
+    --         equiv(Formula, Formula)
+    formula: % -> OutputForm
+    coerce(p: %): OutputForm ==
+      formula p
+
+    primaryFormula(p: %): OutputForm ==
+      p' := rep p
+      p' case T => p'@T::OutputForm
+      case constantIfCan p' is
+        c@Identifier => c::OutputForm
+        otherwise =>
+          is?(p', IMP) or is?(p', EQV) =>
+            args := argument p'
+            elt(operator(p')::OutputForm, 
+                  [formula first args, formula second args])$OutputForm
+          paren(formula p)$OutputForm
+
+    notFormula(p: %): OutputForm ==
+      case isNot p is
+        f@% => elt(outputForm 'not, [notFormula f])$OutputForm
+        otherwise => primaryFormula p
+
+    andFormula(f: %): OutputForm ==
+      case isAnd f is
+	p@Pair(%,%) =>
+          -- ??? idealy, we should be using `and$OutputForm' but
+          -- ??? a bug in the compiler currently prevents that.
+          infix(outputForm 'and, notFormula first p,
+             andFormula second p)$OutputForm
+        otherwise => notFormula f
+
+    orFormula(f: %): OutputForm ==
+      case isOr f is
+        p@Pair(%,%) => 
+          -- ??? idealy, we should be using `or$OutputForm' but
+          -- ??? a bug in the compiler currently prevents that.
+          infix(outputForm 'or, andFormula first p, 
+             orFormula second p)$OutputForm
+        otherwise => andFormula f
+
+    formula f ==
+      -- Note: this should be equivFormula, but see the explanation above.
+      orFormula f
+
+@
+
+<<package PROPFUN1 PropositionalFormulaFunctions1>>=
+)abbrev package PROPFUN1 PropositionalFormulaFunctions1
+++ Author: Gabriel Dos Reis
+++ Date Created: April 03, 2010
+++ Date Last Modified: April 03, 2010
+++ Description:
+++   This package collects unary functions operating on propositional
+++   formulae.
+PropositionalFormulaFunctions1(T): Public == Private where
+  T: SetCategory
+  Public == Type with
+    dual: PropositionalFormula T -> PropositionalFormula T
+      ++ \spad{dual f} returns the dual of the proposition \spad{f}.
+    atoms: PropositionalFormula T -> Set T
+      ++ \spad{atoms f} ++ returns the set of atoms appearing in
+      ++ the formula \spad{f}.
+    simplify: PropositionalFormula T -> PropositionalFormula T
+      ++ \spad{simplify f} returns a formula logically equivalent
+      ++ to \spad{f} where obvious tautologies have been removed.
+  Private == add
+    macro F == PropositionalFormula T
+    inline Pair(F,F)
+
+    dual f ==
+      f = true$F => false$F
+      f = false$F => true$F
+      isAtom f case T => f
+      (f1 := isNot f) case F => not dual f1
+      (f2 := isAnd f) case Pair(F,F) =>
+         disjunction(dual first f2, dual second f2)
+      (f2 := isOr f) case Pair(F,F) =>
+         conjunction(dual first f2, dual second f2)
+      error "formula contains `equiv' or `implies'"
+
+    atoms f ==
+      (t := isAtom f) case T => { t }
+      (f1 := isNot f) case F => atoms f1
+      (f2 := isAnd f) case Pair(F,F) =>
+         union(atoms first f2, atoms second f2)
+      (f2 := isOr f) case Pair(F,F) =>
+         union(atoms first f2, atoms second f2)
+      empty()$Set(T)
+
+    -- one-step simplification helper function
+    simplifyOneStep(f: F): F ==
+      (f1 := isNot f) case F =>
+        f1 = true$F => false$F
+        f1 = false$F => true$F
+        (f1' := isNot f1) case F => f1'         -- assume classical logic
+        f
+      (f2 := isAnd f) case Pair(F,F) =>
+        first f2 = false$F or second f2 = false$F => false$F
+        first f2 = true$F => second f2
+        second f2 = true$F => first f2
+        f
+      (f2 := isOr f) case Pair(F,F) =>
+        first f2 = false$F => second f2
+        second f2 = false$F => first f2
+        first f2 = true$F or second f2 = true$F => true$F
+        f
+      (f2 := isImplies f) case Pair(F,F) =>
+        first f2 = false$F or second f2 = true$F => true$F
+        first f2 = true$F => second f2
+        second f2 = false$F => not first f2
+        f
+      (f2 := isEquiv f) case Pair(F,F) =>
+        first f2 = true$F => second f2
+        second f2 = true$F => first f2
+        first f2 = false$F => not second f2
+        second f2 = false$F => not first f2
+        f
+      f
+
+    simplify f ==
+      (f1 := isNot f) case F => simplifyOneStep(not simplify f1)
+      (f2 := isAnd f) case Pair(F,F) =>
+        simplifyOneStep(conjunction(simplify first f2, simplify second f2))
+      (f2 := isOr f) case Pair(F,F) =>
+        simplifyOneStep(disjunction(simplify first f2, simplify second f2))
+      (f2 := isImplies f) case Pair(F,F) =>
+        simplifyOneStep(implies(simplify first f2, simplify second f2))
+      (f2 := isEquiv f) case Pair(F,F) =>
+        simplifyOneStep(equiv(simplify first f2, simplify second f2))
+      f
+@
+
+<<package PROPFUN2 PropositionalFormulaFunctions2>>=
+)abbrev package PROPFUN2 PropositionalFormulaFunctions2
+++ Author: Gabriel Dos Reis
+++ Date Created: April 03, 2010
+++ Date Last Modified: April 03, 2010
+++ Description:
+++   This package collects binary functions operating on propositional
+++   formulae.
+PropositionalFormulaFunctions2(S,T): Public == Private where
+  S: SetCategory
+  T: SetCategory
+  Public == Type with
+    map: (S -> T, PropositionalFormula S) -> PropositionalFormula T
+      ++ \spad{map(f,x)} returns a propositional formula where
+      ++ all atoms in \spad{x} have been replaced by the result
+      ++ of applying the function \spad{f} to them.
+  Private == add
+    macro FS == PropositionalFormula S
+    macro FT == PropositionalFormula T
+    map(f,x) ==
+      x = true$FS => true$FT
+      x = false$FS => false$FT
+      (t := isAtom x) case S => f(t)::FT
+      (f1 := isNot x) case FS => not map(f,f1)
+      (f2 := isAnd x) case Pair(FS,FS) =>
+         conjunction(map(f,first f2), map(f,second f2))
+      (f2 := isOr x) case Pair(FS,FS) =>
+         disjunction(map(f,first f2), map(f,second f2))
+      (f2 := isImplies x) case Pair(FS,FS) =>
+         implies(map(f,first f2), map(f,second f2))
+      (f2 := isEquiv x) case Pair(FS,FS) =>
+         equiv(map(f,first f2), map(f,second f2))
+      error "invalid propositional formula"
+
+@
+
+
+\section{Kleene's Three-Valued Logic}
+<<domain KTVLOGIC KleeneTrivalentLogic>>=
+)abbrev domain KTVLOGIC KleeneTrivalentLogic
+++ Author: Gabriel Dos Reis
+++ Date Created: September 20, 2008
+++ Date Last Modified: January 14, 2012
+++ Description: 
+++   This domain implements Kleene's 3-valued propositional logic.
+KleeneTrivalentLogic(): Public == Private where
+  Public == Join(PropositionalLogic,Finite) with
+    unknown: %     ++ the indefinite `unknown' 
+    case: (%,[| false |]) -> Boolean
+      ++ x case false holds if the value of `x' is `false'
+    case: (%,[| unknown |]) -> Boolean
+      ++ x case unknown holds if the value of `x' is `unknown'
+    case: (%,[| true |]) -> Boolean
+      ++ s case true holds if the value of `x' is `true'.
+  Private == Maybe Boolean add
+    false == per just(false@Boolean)
+    unknown == per nothing
+    true == per just(true@Boolean)
+    x = y == rep x = rep y
+    x case true == x = true@%
+    x case false == x = false@%
+    x case unknown == x = unknown
+
+    not x ==
+      x case false => true
+      x case unknown => unknown
+      false
+
+    x and y ==
+      x case false => false
+      x case unknown =>
+        y case false => false
+        unknown
+      y
+
+    x or y ==
+      x case false => y
+      x case true => x
+      y case true => y
+      unknown
+
+    implies(x,y) ==
+      x case false => true
+      x case true => y
+      y case true => true
+      unknown
+
+    equiv(x,y) ==
+      x case unknown => x
+      x case true => y
+      not y
+
+    coerce(x: %): OutputForm ==
+      case rep x is
+        y@Boolean => y::OutputForm
+        otherwise => outputForm 'unknown
+
+    size() == 3
+
+    index n ==
+      n > 3 => error "index: argument out of bound"
+      n = 1 => false
+      n = 2 => unknown
+      true
+
+    lookup x ==
+      x = false => 1
+      x = unknown => 2
+      3
+@
+
+\section{License}
+
+<<license>>=
+--Copyright (C) 1991-2002, The Numerical Algorithms Group Ltd.
+--All rights reserved.
+--Copyright (C) 2007-2013, Gabriel Dos Reis.
+--All rights reserved.
+--
+--Redistribution and use in source and binary forms, with or without
+--modification, are permitted provided that the following conditions are
+--met:
+--
+--    - Redistributions of source code must retain the above copyright
+--      notice, this list of conditions and the following disclaimer.
+--
+--    - Redistributions in binary form must reproduce the above copyright
+--      notice, this list of conditions and the following disclaimer in
+--      the documentation and/or other materials provided with the
+--      distribution.
+--
+--    - Neither the name of The Numerical Algorithms Group Ltd. nor the
+--      names of its contributors may be used to endorse or promote products
+--      derived from this software without specific prior written permission.
+--
+--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+@
+<<*>>=
+<<license>>
+
+<<category LOGIC Logic>>
+<<category BOOLE BooleanLogic>>
+
+<<category PROPLOG PropositionalLogic>>
+<<domain PROPFRML PropositionalFormula>>
+<<package PROPFUN1 PropositionalFormulaFunctions1>>
+<<package PROPFUN2 PropositionalFormulaFunctions2>>
+
+<<domain KTVLOGIC KleeneTrivalentLogic>>
+
+@
+
+
+\eject
+\begin{thebibliography}{99}
+\bibitem{1} nothing
+\end{thebibliography}
+\end{document}
+