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

PropLogicTest

Contents

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

Various prime form generations with combined parsing and display

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]
 > appleBasketDistribution 10 4
 [2,2,3,3]
 > appleBasketDistribution 10 4
 [3,2,1,4]
 > appleBasketDistribution 10 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

Size parameter

Random formulas

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...............................

Testing the default propositional algebras

Tests for FastPropLogic

Testing of the M- and P-procedure

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

Correctness of the Prime Normal Form constructions

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

Test for the total package

Profiling - first version

Measures

correctness tests (move these correctness tests)--!!!!!!!!!!1

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)