diff options
| author | dos-reis <gdr@axiomatics.org> | 2010-02-28 15:46:39 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2010-02-28 15:46:39 +0000 |
| commit | 6dc0a8a511253741245a48bd02d4f6861b1a938b (patch) | |
| tree | 0a5a18145281f4ad3ec6cf107d3520eaec9f187f /src | |
| parent | d80dc0d3c5aca58f51d18132005c39a4358e32ae (diff) | |
| download | open-axiom-6dc0a8a511253741245a48bd02d4f6861b1a938b.tar.gz | |
* algebra/boolean.spad.pamphlet
(conjunction$PropositionalFormula): New exported function.
(disjunction$PropositionalFormula): Likewise.
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)) |