diff options
| author | dos-reis <gdr@axiomatics.org> | 2011-10-16 09:43:42 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2011-10-16 09:43:42 +0000 |
| commit | f699415cce3f73d0f2b63ecb3b1fdc7084ba4cea (patch) | |
| tree | 744cd817af434417c8bbcc64123029f4e42ae7a3 /src/algebra/boolean.spad.pamphlet | |
| parent | 39982663dc44f7b44c63af6ae4182f8d60d7d341 (diff) | |
| download | open-axiom-f699415cce3f73d0f2b63ecb3b1fdc7084ba4cea.tar.gz | |
* algebra/boolean.spad.pamphlet (Boolean): Implement default
Boolean operators in terms of Logic operators.
(PropositionalFormula): Implement Logic operators instead of
Boolean operators.
* algebra/exposed.lsp.pamphlet: Expose
PropositionalFormulaFunctions1 and PropositionalFormulaFunctions2.
Diffstat (limited to 'src/algebra/boolean.spad.pamphlet')
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index 4e307819..3e604095 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -29,7 +29,9 @@ BooleanLogic(): Category == Logic with or: (%,%) -> % ++ \spad{x or y} returns the disjunction of \spad{x} and \spad{y}. add - ~ x == not x + not x == ~ x + x and y == x /\ y + x or y == x \/ y @ <<category PROPLOG PropositionalLogic>>= @@ -126,18 +128,18 @@ PropositionalFormula(T: SetCategory): Public == Private where false == per constantKernel FALSE true == per constantKernel TRUE - not p == + ~ 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 and q == conjunction(p,q) + p /\ q == conjunction(p,q) disjunction(p,q) == per kernel(operator(OR, 2), [p, q], 1 + max(level p, level q)) - p or q == disjunction(p,q) + p \/ q == disjunction(p,q) implies(p,q) == per kernel(operator(IMP, 2), [p, q], 1 + max(level p, level q)) @@ -230,11 +232,14 @@ PropositionalFormula(T: SetCategory): Public == Private where primaryFormula(p: %): OutputForm == p' := rep p p' case T => p'@T::OutputForm - 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 + 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 |