PropLogicCore
 Contents Propositional formulas Parsing propositional formulas on string atoms Propositional algebras
Description

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

• The data type (PropForm a) of propositional formulas, based on a given atom type a.
• The two-parameter type class (PropAlg a p) of a 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.
Synopsis
data PropForm a
 = A a | F | T | N (PropForm a) | CJ [PropForm a] | DJ [PropForm a] | SJ [PropForm a] | EJ [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
data PropForm a
Constructors
 A a F T N (PropForm a) CJ [PropForm a] DJ [PropForm a] SJ [PropForm a] EJ [PropForm a] Instances
 Ord a => PropAlg a (PropForm a) Eq a => Eq (PropForm a) Ord a => Ord (PropForm a) Read a => Read (PropForm a) Show a => Show (PropForm a) Display a => Display (PropForm a)

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 display φ then returns

``` [-[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 Read and Show, so String conversion (and displaying results in the interpreter) are well defined. For example

``` 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
stringToProp :: String -> PropForm String
... CONTINUEHERE ....
Propositional algebras
class Ord a => PropAlg a p | p -> a where
Methods
 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 Instances
 PropAlg Void Bool PropAlg Void Bool Ord a => PropAlg a (TruthTable a) Ord a => PropAlg a (PropForm a) Ord a => PropAlg a (MixForm a) Ord a => PropAlg a (XPCNF a) Ord a => PropAlg a (XPDNF a)

PropAlg a p is a structure, made of

a is the atom type

p is the type of propositions

at :: a -> p is the 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, neg :: p-> p and conj, disj, subj, equij :: [p] -> p

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