diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ChangeLog | 6 | ||||
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 18 |
2 files changed, 21 insertions, 3 deletions
diff --git a/src/ChangeLog b/src/ChangeLog index f0a29e16..3b5cef38 100644 --- a/src/ChangeLog +++ b/src/ChangeLog @@ -1,3 +1,9 @@ +2010-02-28 Gabriel Dos Reis <gdr@cs.tamu.edu> + + * algebra/boolean.spad.pamphlet + (conjunction$PropositionalFormula): New exported function. + (disjunction$PropositionalFormula): Likewise. + 2010-02-27 Gabriel Dos Reis <gdr@cs.tamu.edu> * interp/modemap.boot (augModemapsFromCategoryRep): Remove diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index 032655ee..15071693 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -76,6 +76,14 @@ PropositionalFormula(T: SetCategory): Public == Private where ++ \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 % @@ -85,7 +93,7 @@ PropositionalFormula(T: SetCategory): Public == Private where -- Local names for proposition logical operators macro NOT == '%not macro AND == '%and - macro OR == '%OR + macro OR == '%or macro IMP == '%implies macro EQV == '%equiv @@ -102,12 +110,16 @@ PropositionalFormula(T: SetCategory): Public == Private where not p == per kernel(operator(NOT, 1::Arity), [p], 1 + level p) - p and q == + conjunction(p,q) == per kernel(operator(AND, 2), [p, q], 1 + max(level p, level q)) - p or q == + p and 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) + implies(p,q) == per kernel(operator(IMP, 2), [p, q], 1 + max(level p, level q)) |