Safe Haskell | Safe-Infered |
---|

This module comprises the abstract definition of two core concepts of propositional logic:

- The data type
`(`

of`PropForm`

a)*propositional formulas*, based on a given*atom*type`a`

. - The two-parameter type class
`(`

of a`PropAlg`

a p)*propositional algebra*, where`a`

is the*atom*type and`p`

the type of*propositions*. Operations of such a structure include a decision if two propositions are`equivalent`

, if a given proposition is`satisfiable`

, a converter`toPropForm`

and the inverse`fromPropForm`

, 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 `at`

:: a -> p*atomic proposition* constructor, similar to the constructor `A`

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-> p`conj`

, `disj`

, `subj`

, `equij`

:: [p] -> p

There the set of ......................................................................