PropLogic-0.9.0.4: Propositional Logic

PropLogicTest

Synopsis

# Convenient abbreviations and combinations of often used functions

## Various prime form generations

pdnf' :: Ord a => PropForm a -> PDNF aSource

pcnf' :: Ord a => PropForm a -> PCNF aSource

# Random generation

## Auxiliary random functions (probably obsolete)

For example,

``` > randomListMember ['a','b','c','d']
'b'
> randomListMember ['a','b','c','d']
'd'
> randomListMember ['a','b','c','d']
'c'
```

randomChoice :: [a] -> IO (a, [a])Source

Removes one random member from a given list and returns this member and the remaining list. For example,

``` > randomChoice ["a", "b", "c"]
("c",["a","b"])
> randomChoice ["a", "b", "c"]
("b",["a","c"])
> randomChoice ["a", "b", "c"]
("a",["b","c"])
> randomChoice ["a", "b", "c"]
("a",["b","c"])
```

shuffle :: [a] -> IO [a]Source

For example,

``` > shuffle [1,2,3,2,1]
[2,1,3,1,2]
> shuffle [1,2,3,2,1]
[1,2,3,2,1]
> shuffle [1,2,3,2,1]
[2,1,2,3,1]
> shuffle [1,2,3,2,1]
[2,3,1,1,2]
> shuffle [1,2,3,2,1]
[2,1,1,3,2]
> shuffle [1,2,3,2,1]
[1,2,1,3,2]
```

randomSublist :: [a] -> IO [a]Source

`randomSublist xL` deletes a random number of members and returns the result. For example,

``` > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
[4]
> randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
[3,4]
> randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
[2,3,4,5,6,7,7,7,8,8]
> randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
[1,2,5,7,8]
> randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
[4,5,8,8]
> randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
[1,2,3,5,6,7,7,8,8]
```

`nRandomRIO n (lower,upper)` returns an list of n random integers between lower and upper. For example,

``` > nRandomRIO 10 (1,3)
[2,3,3,2,2,3,3,3,3,1]
> nRandomRIO 10 (1,3)
[3,2,1,2,2,3,3,1,1,1]
> nRandomRIO 10 (1,3)
[1,3,2,1,2,1,2,2,1,2]
```

`weightedRandomMember` takes a list `[(x1,n1),...,(xM,nM)]` of `(a,Int)` pairs and selects one of the `x1,...,xM`. The second integer value `ni` in each pair `(xi,ni)` represents the relative likelihood for the choice of `xi` compare to the other values. In the following example and on the long run, `a` is chosen 10 times more often than `b`, and `c` isn't chosen at all.

``` > weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"b"
> weightedRandomMember [("a",10),("b",1),("c",0)]
"a"
```

`appleBasketDistribution n k` distributes `n` apples into `k` baskets in the sense that the result is a random integer list of length `k`, where the sum of its components is `n`.

``` > appleBasketDistribution 10 4
[4,2,2,2]
[2,2,3,3]
[3,2,1,4]
[0,7,0,3]
```

## Random I-Forms and X-Forms

randomXForm :: Ord a => [a] -> Int -> Int -> IO (XForm a)Source

## Random DNFs and CNFs

randomDNF :: Ord a => [a] -> Int -> Int -> IO (DNF a)Source

randomCNF :: Ord a => [a] -> Int -> Int -> IO (CNF a)Source

## Random propositional formulas in general

### Random formulas

Constructors

 T_ F_ N_ CJ_ DJ_ SJ_ EJ_

`randomPropForm aL (aSize,jSize)` returns a randomly generated propositional formula `p` such that

```     atoms p    == aL
atomSize p == aSize
juncSize p == jSize
```

If `atomSize` is smaller than the length of `aL`, an error message is returned. For example,

``` > randomPropForm ["x", "y"] (3,3)
EJ [A "y",T,A "y",A "x",DJ []]
> randomPropForm ["x", "y"] (3,3)
EJ [SJ [A "y",A "y"],DJ [A "x"]]
> randomPropForm ["x", "y"] (3,3)
EJ [EJ [],A "x",CJ [A "y"],A "x"]
> randomPropForm ['x','y','z'] (1,1)
*** Exception: randomPropForm -- atom size smaller than ordered atom list
```

`randomCharProp (aCard,aSize,jSize)` is `randomPropForm aL (aSize,jSize)`, where `aL` is the ordered list of the first `aCard` small characters `a, b, c, ...`. If the atom cardinality is undefined, i.e. if not `0<=aCard<=26`, or if it exceeds `aSize`, an error message is returned. For example,

``` > randomCharProp (3,5,5)
SJ [A 'c',EJ [A 'a',A 'c'],F,T,DJ [A 'b'],A 'c']
> randomCharProp (3,5,5)
SJ [A 'a',A 'c',DJ [T,CJ [A 'b',A 'a',A 'b'],T]]
> randomCharProp (3,5,5)
DJ [F,A 'b',SJ [F],A 'c',DJ [A 'a'],A 'c',A 'a']
```

# Testing

## Testing a propositional algebra

### Axioms of propositional algebras

CONTINUEHERE ..............................................................!!

### The summarized test function for a propositional algebra

test_prop_alg :: (Show a, Show p, PropAlg a p) => IO a -> IO p -> Int -> IO ()Source

## Tests for DefaultPropLogic

### Testing the normalizations

...continuehere...............................

## Tests for FastPropLogic

### Testing of the M- and P-procedure

continuehere ............................

### Correctness of the Prime Normal Form constructions

continuehere ...........................

# Profiling - second version

verboseRandomPrimeTest :: (Int, Int, Int) -> IO (Int, Int, Int, Seconds)Source

`randomPrimeTest (atomNum, formLen, averLineLen) = (atomNum', formLen', vol', secs')`

verboseRandomPrimeTesting :: (Int, Int, Int) -> Int -> IO (Int, Int, Seconds, Seconds, Seconds)Source

`verboseRandomPrimeTesting (atomNum, formLen, averLineLen) numberOfTests = (maxFormLen, averFormLen, maxTime, averTime, standDev)`