PropLogic-0.9.0.4: Propositional Logic

FastPropLogic

Description

This module defines three altenative representations for certain propositional normal forms, namely

``` data XPDNF a          -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a
data XPCNF a          -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a
data MixForm a        -- a type made of pairwise minimal DNF's and CNF's on a given atom type a
```

For each of these types there is a converter from and a converter to propositional formulas

```    fromXPDNF :: Ord a => XPDNF a -> PropForm a             toXPDNF :: Ord a => PropForm a -> XPDNF a
fromXPCNF :: Ord a => XPCNF a -> PropForm a             toXPCNF :: Ord a => PropForm a -> XPCNF a
fromMixForm :: Ord a => MixForm a -> PropForm a         toMixForm :: Ord a => PropForm a -> MixForm a
```

Each of these three types is turned into a propositional algebra `PropAlg`, i.e. for every ordered type `a` of atoms we have three instances

``` PropAlg a (XPDNF a)
PropAlg a (XPCNF a)
PropAlg a (MixForm a)
```

Different to the two default propositional algebras on propositional formulas and truth tables, these three algebras comprise fast function implementations and thus provide practical versions for propositional algebras, where propositions of arbitrary size are processed in reasonable time. In more detail the involved complexities are given in the table below (see ......). It also explains, which of the three algebras should be chosen in an actual application.

Actually, this module is essentially a re-implementation of already explained concepts from PropLogicCore and DefaultPropLogic and for the user it shouldn't be necessary to further explain how the algorithms work. The remainder of this document is an attempt to do just that. However, if you at least want an idea of what is going on here, it may suffice to read the first section with the introductory example below.

Synopsis

# Introductory example

## Generating a Prime Disjunctive Normal Form, the default and the fast way

Recall, that we already defined Disjunctive Normal Forms and Prime Disjunctive Normal Forms in DefaultPropLogic as special versions of propositional formulas, along with a canonizer `pdnf` to obtain these normal forms

``` type DNF a = PropForm a
type PDNF a = DNF a
pdnf :: PropForm a -> PDNF a
```

For a simple example formula `p`, given by

``` > p = DJ [EJ [A "x", A "y"], N (A "z")]  ::  PropForm String
```

more conveniently displayed by

``` > display p
[[x <-> y] + -z]
```

the PDNF of `p` is then generated by

``` > pdnf p
DJ [CJ [EJ [A "x",F],EJ [A "y",F]],CJ [EJ [A "x",T],EJ [A "y",T]],CJ [EJ [A "z",F]]]
> display (pdnf p)
[[[x <-> false] * [y <-> false]] + [[x <-> true] * [y <-> true]] + [* [z <-> false]]]
```

or more conveniently displayed in its evaluated form

``` > display (eval (pdnf p))
[[-x * -y] + [x * y] + -z]
```

.............!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!..............................

(Actually, each converter pair is also part of each of the given algebras. For example, in the XPDNF instance holds: `fromXPDNF` = `toPropForm` and `toXPDNF` = `fromPropForm`.)

## XPDNF as a propositional algebra

,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,

# Syntax

type XLit a = (Olist a, ILit)Source

type XLine a = (Olist a, ILine)Source

type XForm a = (Olist a, IForm)Source

data XPDNF a Source

Constructors

 XPDNF (XForm a)

Instances

 Ord a => PropAlg a (XPDNF a) Eq a => Eq (XPDNF a) Read a => Read (XPDNF a) Show a => Show (XPDNF a) Display a => Display (XPDNF a)

data XPCNF a Source

Constructors

 XPCNF (XForm a)

Instances

 Ord a => PropAlg a (XPCNF a) Eq a => Eq (XPCNF a) Read a => Read (XPCNF a) Show a => Show (XPCNF a) Display a => Display (XPCNF a)

data MixForm a Source

Constructors

 M2DNF (XForm a) M2CNF (XForm a) PDNF (XForm a) PCNF (XForm a)

Instances

 Ord a => PropAlg a (MixForm a) Eq a => Eq (MixForm a) Read a => Read (MixForm a) Show a => Show (MixForm a) Display a => Display (MixForm a)

# Conversions

## IdxPropForm -- indexed propositional formulas

tr :: (s -> t) -> PropForm s -> PropForm tSource

`tr f form` replaces each atom form occurrence `(A x)` in the formula `form` by the new atom `(A (f x))`. Everything else remains.

`iTr [i_1,...,i_n] iform` replaces each index `j` in `iform` by `i_j`. For example,

``` > let iform =  iForm [[-1,3,-4,5],[-2,-3,4,6]] :: IForm
> iform
COSTACK [COSTACK [-1,3,-4,5],COSTACK [-2,-3,4,6]]
> iTr [7,8,9,10,11,12,13] iform
COSTACK [COSTACK [-7,9,-10,11],COSTACK [-8,-9,10,12]]
> iTr [2,4] iform
-- error, because the index list [2,4] must at least be of length 6 to cover the indices 1,..,6 of iform.
```

idx :: Ord a => Olist a -> a -> IAtomSource

`idx [i_1,...,i_n] i_k` returns `k`, i.e. the index of the index in the given index list. Note, that the first member of the list starts with index 1, not 0. For example,

``` > idx [2,4,6,8] 6
3
```

nth :: Ord a => Olist a -> IAtom -> aSource

`nth [i_1,...,i_n] k` returns `i_k`, i.e. the `k`'s element in the list `[i_1,...,i_n]`, counting from `1`. For example,

``` > nth [2,4,6,8] 3
6
```

itr :: Ord a => Olist a -> Olist a -> Maybe (Olist IAtom)Source

iUni :: Ord a => [Olist a] -> (Olist a, [Maybe (Olist IAtom)])Source

unifyXForms :: Ord a => [XForm a] -> (Olist a, [IForm])Source

## Purely syntactical conversions to propositional formulas

xLIT :: Ord a => XLit a -> PropForm aSource

xNLC :: Ord a => XLine a -> PropForm aSource

xNLD :: Ord a => XLine a -> PropForm aSource

xCNF :: Ord a => XForm a -> PropForm aSource

xDNF :: Ord a => XForm a -> PropForm aSource

# The IForm algebra

## Generation of pairwise minimal, minimal and prime forms

### Generation of prime and pairwise minimal forms of two lines

data CaseSymbol Source

Constructors

 NOOO NOOP NOPO NOPP NIOO NIOP NIPO NIPP NMNN

Instances

 Eq CaseSymbol Ord CaseSymbol Read CaseSymbol Show CaseSymbol

### Implementation of the M- and the P-Procedure

allPairs :: [a] -> [(a, a)]Source

# Complexities and choice of a algebra

```                                         DefaultPropLogic.                               FastPropLogic
--------------------------------------         -----------------------------------
PropForm            TruthTable                 XPDNF       XPCNF          MixForm
--------------------------------------------------------------------------------------------------------------------------
at
false
true
neg
conj, disj, subj, equij
valid
satisfiable
subvalent
equivalent
covalent, disvalent,
properSubvalent, properDisvalent
atoms
redAtoms, irrAtoms
nullatomic
subatomic, equiatomic
.........
.........
```