PropLogic-0.9.0.1: A system for propositional logic with default and fast instances of propositional algebras.

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.

[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 - first version

## performance tests

pnfPerform :: (Display a, Show a, Ord a) => PropForm a -> IO CanonPerformanceSource

# 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)