This module comprises the abstract definition of two core concepts of propositional logic:
- The data type
(
of propositional formulas, based on a given atom typePropForm
a)a
. - The two-parameter type class
(
of a propositional algebra, wherePropAlg
a p)a
is the atom type andp
the type of propositions. Operations of such a structure include a decision if two propositions areequivalent
, if a given proposition issatisfiable
, a convertertoPropForm
and the inversefromPropForm
, which turns a propositional formula into a proposition.
- data PropForm a
- stringToProp :: String -> PropForm String
- class Ord a => PropAlg a p | p -> a where
- at :: a -> p
- false :: p
- true :: p
- neg :: p -> p
- conj :: [p] -> p
- disj :: [p] -> p
- subj :: [p] -> p
- equij :: [p] -> p
- valid :: p -> Bool
- satisfiable :: p -> Bool
- contradictory :: p -> Bool
- subvalent :: p -> p -> Bool
- equivalent :: p -> p -> Bool
- covalent :: p -> p -> Bool
- disvalent :: p -> p -> Bool
- properSubvalent :: p -> p -> Bool
- properDisvalent :: p -> p -> Bool
- atoms :: p -> Olist a
- redAtoms :: p -> Olist a
- irrAtoms :: p -> Olist a
- nullatomic :: p -> Bool
- subatomic :: p -> p -> Bool
- equiatomic :: p -> p -> Bool
- coatomic :: p -> p -> Bool
- disatomic :: p -> p -> Bool
- properSubatomic :: p -> p -> Bool
- properDisatomic :: p -> p -> Bool
- ext :: p -> [a] -> p
- infRed :: p -> [a] -> p
- supRed :: p -> [a] -> p
- infElim :: p -> [a] -> p
- supElim :: p -> [a] -> p
- biequivalent :: p -> p -> Bool
- pointwise :: (p -> Bool) -> [p] -> Bool
- pairwise :: (p -> p -> Bool) -> [p] -> Bool
- toPropForm :: p -> PropForm a
- fromPropForm :: PropForm a -> p
Propositional formulas
A typical example of a propositional formula φ in standard mathematical notation is given by
¬(rain ∧ snow) ∧ (wet ↔ (rain ∨ snow)) ∧ (rain → hot) ∧ (snow → ¬ hot)
The primitive elements hot
, rain
, snow
and wet
are the atoms of φ.
In Haskell, we define propositional formulas as members of the data type (PropForm a
), where the type parameter a
is the
chosen atom type. A suitable choice for our example would be the atom type String
and φ becomes a member of
PropForm String
type, namely
CJ [N (CJ [A "rain", A "snow"]), EJ [A "wet", DJ [A "rain", A "snow"]], SJ [A "rain", A "hot"], SJ [A "snow", N (A "hot")]]
This Haskell version is more tedious and we introduce a third notation for nicer output by making PropForm
an instance of the
Display
type class. A call of
then returns
display
φ
[-[rain * snow] * [wet <-> [rain + snow]] * [rain -> hot] * [snow -> -hot]]
The following overview compares the different representations:
Haskell displayed as kind of formula -------------------------------------------------------------------- A x x (without quotes) atomic formula F false the boolean zero value T true the boolean unit value N p -p negation CJ [p1,...,pN] [p1 * ... * pN] conjunction DJ [p1,...,pN] [p1 + ... + pN] disjunction SJ [p1,...,pN] [p1 -> ... -> pN] subjunction EJ [p1,...,pN] [p1 <-> ... <-> pN] equijunction
Note, that the negation is unary, as usual, but the last four constructors are all multiary junctions, i.e. the list [p1,...,pN]
may have any number N
of arguments, including N=0
and N=1
.
PropForm a
is an instance of Eq
and Ord
, two formulas can be compared for linear order with <
or compare
and
PropForm a
alltogther is linearly ordered, provided that a
itself is.
But note, that this order is a pure formal expression order does neither reflect the atomical quasi-order structure
(induced by the subatomic
relation; see below) nor the semantical quasi-order structure (induced by subvalent
).
So this is not the order that reflects the idea of propositional logic.
But we do use it however for the sorting and order of formulas to reduce ambiguities and increase
the efficiency of algorithmes on certain normal forms.
In DefaultPropLogic we introduce the normal forms OrdPropForm
and the normalizer ordPropForm
.
PropForm a
is also an instance of
and Read
, so String conversion (and displaying results in the interpreter) are
well defined. For example
Show
show (CJ [A 3, N (A 7), A 4]) == "CJ [A 3,N (A 7),A 4]"
Note, that reading a formula, e.g.
read "SJ [A 3, A 4, T]"
issues a complaint due to the ambiguity of the atom type. But that can be fixed, e.g. by stating the type explicitely, as in
(read "SJ [A 3, A 4, T]") :: PropForm Integer
Parsing propositional formulas on string atoms
... CONTINUEHERE ....
Propositional algebras
class Ord a => PropAlg a p | p -> a whereSource
satisfiable :: p -> BoolSource
contradictory :: p -> BoolSource
subvalent :: p -> p -> BoolSource
equivalent :: p -> p -> BoolSource
covalent :: p -> p -> BoolSource
disvalent :: p -> p -> BoolSource
properSubvalent :: p -> p -> BoolSource
properDisvalent :: p -> p -> BoolSource
redAtoms :: p -> Olist aSource
irrAtoms :: p -> Olist aSource
nullatomic :: p -> BoolSource
subatomic :: p -> p -> BoolSource
equiatomic :: p -> p -> BoolSource
coatomic :: p -> p -> BoolSource
disatomic :: p -> p -> BoolSource
properSubatomic :: p -> p -> BoolSource
properDisatomic :: p -> p -> BoolSource
infElim :: p -> [a] -> pSource
supElim :: p -> [a] -> pSource
biequivalent :: p -> p -> BoolSource
pointwise :: (p -> Bool) -> [p] -> BoolSource
pairwise :: (p -> p -> Bool) -> [p] -> BoolSource
toPropForm :: p -> PropForm aSource
fromPropForm :: PropForm a -> pSource
PropAlg a p
is a structure, made of
a
is the atom type
p
is the type of propositions
is the atomic proposition constructor, similar to the constructor at
:: a -> pA
for atomic formulas.
Similar to the definition of PropForm
, we have the same set of boolean junctors on propositions:
, false
, true
:: p
and neg
:: p-> pconj
, disj
, subj
, equij
:: [p] -> p
There the set of ......................................................................