-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A system for propositional logic with default and fast instances of propositional algebras.
--   
--   A system for propositional logic with default and fast instances of
--   propositional algebras.
@package PropLogic
@version 0.9.0.2


-- | An <a>Olist</a> is an <i>ordered list</i>. The main function of this
--   module is the implementation of the finite subset structure of a given
--   type <tt>a</tt>. Finite sets are represented as ordered lists and the
--   basic set functions and relations like <a>union</a>,
--   <a>intersection</a>, <a>included</a> etc. are provided.
module Olist
type Olist a = [a]
olist :: Ord a => [a] -> Olist a
isOlist :: Ord a => [a] -> Bool
empty :: Ord a => Olist a
isEmpty :: Ord a => Olist a -> Bool
member :: Ord a => a -> Olist a -> Bool
insert :: Ord a => a -> Olist a -> Olist a
delete :: Ord a => a -> Olist a -> Olist a
included :: Ord a => Olist a -> Olist a -> Bool
properlyIncluded :: Ord a => Olist a -> Olist a -> Bool
disjunct :: Ord a => Olist a -> Olist a -> Bool
properlyDisjunct :: Ord a => Olist a -> Olist a -> Bool
equal :: Ord a => Olist a -> Olist a -> Bool
union :: Ord a => Olist a -> Olist a -> Olist a
intersection :: Ord a => Olist a -> Olist a -> Olist a
difference :: Ord a => Olist a -> Olist a -> Olist a
opposition :: Ord a => Olist a -> Olist a -> Olist a
unionList :: Ord a => [Olist a] -> Olist a
intersectionList :: Ord a => [Olist a] -> Olist a


-- | This module comprises the abstract definition of two core concepts of
--   propositional logic:
--   
--   <ul>
--   <li>The data type <tt>(<a>PropForm</a> a)</tt> of <i>propositional
--   formulas</i>, based on a given <i>atom</i> type <tt>a</tt>.</li>
--   <li>The two-parameter type class <tt>(<a>PropAlg</a> a p)</tt> of a
--   <i>propositional algebra</i>, where <tt>a</tt> is the <i>atom</i> type
--   and <tt>p</tt> the type of <i>propositions</i>. Operations of such a
--   structure include a decision if two propositions are
--   <a>equivalent</a>, if a given proposition is <a>satisfiable</a>, a
--   converter <a>toPropForm</a> and the inverse <a>fromPropForm</a>, which
--   turns a propositional formula into a proposition.</li>
--   </ul>
module PropLogicCore
data PropForm a
A :: a -> PropForm a
F :: PropForm a
T :: PropForm a
N :: (PropForm a) -> PropForm a
CJ :: [PropForm a] -> PropForm a
DJ :: [PropForm a] -> PropForm a
SJ :: [PropForm a] -> PropForm a
EJ :: [PropForm a] -> PropForm a
stringToProp :: String -> PropForm String
class Ord a => PropAlg a p | p -> a
at :: PropAlg a p => a -> p
false :: PropAlg a p => p
true :: PropAlg a p => p
neg :: PropAlg a p => p -> p
conj :: PropAlg a p => [p] -> p
disj :: PropAlg a p => [p] -> p
subj :: PropAlg a p => [p] -> p
equij :: PropAlg a p => [p] -> p
valid :: PropAlg a p => p -> Bool
satisfiable :: PropAlg a p => p -> Bool
contradictory :: PropAlg a p => p -> Bool
subvalent :: PropAlg a p => p -> p -> Bool
equivalent :: PropAlg a p => p -> p -> Bool
covalent :: PropAlg a p => p -> p -> Bool
disvalent :: PropAlg a p => p -> p -> Bool
properSubvalent :: PropAlg a p => p -> p -> Bool
properDisvalent :: PropAlg a p => p -> p -> Bool
atoms :: PropAlg a p => p -> Olist a
redAtoms :: PropAlg a p => p -> Olist a
irrAtoms :: PropAlg a p => p -> Olist a
nullatomic :: PropAlg a p => p -> Bool
subatomic :: PropAlg a p => p -> p -> Bool
equiatomic :: PropAlg a p => p -> p -> Bool
coatomic :: PropAlg a p => p -> p -> Bool
disatomic :: PropAlg a p => p -> p -> Bool
properSubatomic :: PropAlg a p => p -> p -> Bool
properDisatomic :: PropAlg a p => p -> p -> Bool
ext :: PropAlg a p => p -> [a] -> p
infRed :: PropAlg a p => p -> [a] -> p
supRed :: PropAlg a p => p -> [a] -> p
infElim :: PropAlg a p => p -> [a] -> p
supElim :: PropAlg a p => p -> [a] -> p
biequivalent :: PropAlg a p => p -> p -> Bool
pointwise :: PropAlg a p => (p -> Bool) -> [p] -> Bool
pairwise :: PropAlg a p => (p -> p -> Bool) -> [p] -> Bool
toPropForm :: PropAlg a p => p -> PropForm a
fromPropForm :: PropAlg a p => PropForm a -> p
instance Show a => Show (PropForm a)
instance Read a => Read (PropForm a)
instance Eq a => Eq (PropForm a)
instance Display a => Display (PropForm a)


-- | This module implements the basic operations of propositional logic in
--   a very <i>default</i> way, i.e. the definitions and implementations
--   are very intuitive and the whole module can be seen as a
--   reconstruction and tutorial of propositional logic itself. However,
--   some of these implementations are not feasible for other than very
--   small input, because the intuitive algorithms are sometimes too
--   ineffective.
--   
--   Next to some syntactical tools, we provide a common reconstruction of
--   the semantics with an emphasis on <i>truth tables</i>. As a result, we
--   obtain two default models of a propositional algebra, namely
--   <tt>PropAlg a (PropForm a)</tt> the propositional algebra on
--   propositional formulas <a>PropForm</a> and <tt>PropAlg a (TruthTable
--   a)</tt> the algebra on the so-called <i>truth tables</i>
--   <a>TruthTable</a> (each one on a linearly ordered atom type
--   <tt>a</tt>). Additionally, we also instantiate the predefined boolean
--   value algebra on <a>Bool</a> as a trivial, because atomless
--   propositional algebra.
--   
--   Another important concept is the <i>normalization</i>. We introduce a
--   whole range of <i>normalizers</i> and <i>canonizers</i> of
--   propositional formulas.
module DefaultPropLogic
juncDeg :: PropForm a -> Int
juncArgs :: PropForm a -> [PropForm a]
juncCons :: Int -> [PropForm a] -> PropForm a
atomSize :: PropForm a -> Int
juncSize :: PropForm a -> Int
size :: PropForm a -> Int
type LiteralPair a = (a, Bool)
type Valuator a = Olist (LiteralPair a)
correctValuator :: Ord a => [LiteralPair a] -> Valuator a
valuate :: Ord a => Valuator a -> PropForm a -> PropForm a
boolEval :: PropForm a -> Bool
boolApply :: Ord a => PropForm a -> Valuator a -> Bool
allValuators :: Ord a => [a] -> Olist (Valuator a)
zeroValuators :: Ord a => PropForm a -> Olist (Valuator a)
unitValuators :: Ord a => PropForm a -> Olist (Valuator a)
type TruthTable a = (Olist a, Maybe (PropForm a), [([Bool], Bool)])
correctTruthTable :: Ord a => ([a], Maybe (PropForm a), [([Bool], Bool)]) -> TruthTable a
truthTable :: Ord a => PropForm a -> TruthTable a
plainTruthTable :: Ord a => PropForm a -> TruthTable a
truthTableBy :: Ord a => PropForm a -> [a] -> (Valuator a -> Bool) -> TruthTable a
type MultiTruthTable a = (Olist a, [PropForm a], [([Bool], [Bool])])
correctMultiTruthTable :: Ord a => ([a], [PropForm a], [([Bool], [Bool])]) -> MultiTruthTable a
multiTruthTable :: Ord a => [PropForm a] -> MultiTruthTable a
valuatorToNLC :: Valuator a -> NLC a
valuatorToNLD :: Valuator a -> NLD a
valuatorListToCNF :: [Valuator a] -> CNF a
valuatorListToDNF :: [Valuator a] -> DNF a
nlcToValuator :: NLC a -> Valuator a
nldToValuator :: NLD a -> Valuator a
cnfToValuatorList :: CNF a -> [Valuator a]
dnfToValuatorList :: DNF a -> [Valuator a]
truthTableZeroValuators :: TruthTable a -> [Valuator a]
truthTableUnitValuators :: TruthTable a -> [Valuator a]
truthTableToDNF :: TruthTable a -> NaturalDNF a
truthTableToCNF :: TruthTable a -> NaturalCNF a
type OrdPropForm a = PropForm a
isOrdPropForm :: Ord a => PropForm a -> Bool
ordPropForm :: Ord a => PropForm a -> OrdPropForm a
type EvalNF a = PropForm a
isEvalNF :: PropForm a -> Bool
eval :: PropForm a -> EvalNF a
apply :: Ord a => PropForm a -> Valuator a -> EvalNF a
type LitForm a = PropForm a
isLitForm :: PropForm a -> Bool
litFormAtom :: LitForm a -> a
litFormValue :: LitForm a -> Bool
type NegNormForm a = PropForm a
isNegNormForm :: PropForm a -> Bool
negNormForm :: PropForm a -> NegNormForm a
type NLC a = NegNormForm a
isNLC :: Ord a => PropForm a -> Bool
type NLD a = NegNormForm a
isNLD :: Ord a => PropForm a -> Bool
type CNF a = NegNormForm a
isCNF :: Ord a => PropForm a -> Bool
type DNF a = NegNormForm a
isDNF :: Ord a => PropForm a -> Bool
type NaturalDNF a = DNF a
type NaturalCNF a = CNF a
isNaturalDNF :: Ord a => PropForm a -> Bool
isNaturalCNF :: Ord a => PropForm a -> Bool
naturalDNF :: Ord a => PropForm a -> NaturalDNF a
naturalCNF :: Ord a => PropForm a -> NaturalCNF a
type PDNF a = DNF a
type PCNF a = CNF a
primeDNF :: Ord a => PropForm a -> PDNF a
primeCNF :: Ord a => PropForm a -> PCNF a
validates :: Ord a => Valuator a -> PropForm a -> Bool
falsifies :: Ord a => Valuator a -> PropForm a -> Bool
directSubvaluators :: Valuator a -> [Valuator a]
allDirectSubvalidators :: Ord a => Valuator a -> PropForm a -> [Valuator a]
allDirectSubfalsifiers :: Ord a => Valuator a -> PropForm a -> [Valuator a]
primeValuators :: Ord a => PropForm a -> [Valuator a]
coprimeValuators :: Ord a => PropForm a -> [Valuator a]
type MDNF a = DNF a
type MCNF a = CNF a
minimalDNFs :: Ord a => PropForm a -> [MDNF a]
minimalCNFs :: Ord a => PropForm a -> [MCNF a]
type SimpleDNF a = PropForm a
type SimpleCNF a = PropForm a
simpleDNF :: Ord a => DNF a -> SimpleDNF a
simpleCNF :: Ord a => CNF a -> SimpleCNF a
ext' :: PropForm a -> Olist a -> PropForm a
instance Show Void
instance Read Void
instance Eq Void
instance Ord Void
instance PropAlg Void Bool
instance Ord a => PropAlg a (TruthTable a)
instance Ord a => PropAlg a (PropForm a)
instance Ord a => Ord (PropForm a)
instance Display a => Display (MultiTruthTable a)
instance Display a => Display (TruthTable a)
instance (Ord a, Display a) => Display [Valuator a]
instance Display a => Display (Valuator a)
instance Display a => Display (LiteralPair a)


-- | This module defines three altenative representations for certain
--   propositional normal forms, namely
--   
--   <pre>
--   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
--   </pre>
--   
--   For each of these types there is a converter from and a converter to
--   propositional formulas
--   
--   <pre>
--     fromXPDNF :: Ord a =&gt; XPDNF a -&gt; PropForm a             toXPDNF :: Ord a =&gt; PropForm a -&gt; XPDNF a
--     fromXPCNF :: Ord a =&gt; XPCNF a -&gt; PropForm a             toXPCNF :: Ord a =&gt; PropForm a -&gt; XPCNF a
--   fromMixForm :: Ord a =&gt; MixForm a -&gt; PropForm a         toMixForm :: Ord a =&gt; PropForm a -&gt; MixForm a
--   </pre>
--   
--   Each of these three types is turned into a propositional algebra
--   <a>PropAlg</a>, i.e. for every ordered type <tt>a</tt> of <i>atoms</i>
--   we have three instances
--   
--   <pre>
--   PropAlg a (XPDNF a)
--   PropAlg a (XPCNF a)
--   PropAlg a (MixForm a)
--   </pre>
--   
--   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 <a>PropLogicCore</a> and
--   <a>DefaultPropLogic</a> 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.
module FastPropLogic
type IAtom = Int
type ILit = Int
type ILine = Costack ILit
type IForm = Costack ILine
type XLit a = (Olist a, ILit)
type XLine a = (Olist a, ILine)
type XForm a = (Olist a, IForm)
data XPDNF a
XPDNF :: (XForm a) -> XPDNF a
data XPCNF a
XPCNF :: (XForm a) -> XPCNF a
data MixForm a
M2DNF :: (XForm a) -> MixForm a
M2CNF :: (XForm a) -> MixForm a
PDNF :: (XForm a) -> MixForm a
PCNF :: (XForm a) -> MixForm a
type IdxPropForm a = (Olist a, PropForm IAtom)
tr :: (s -> t) -> PropForm s -> PropForm t
iTr :: Olist IAtom -> IForm -> IForm
idx :: Ord a => Olist a -> a -> IAtom
nth :: Ord a => Olist a -> IAtom -> a
itr :: Ord a => Olist a -> Olist a -> Maybe (Olist IAtom)
iUni :: Ord a => [Olist a] -> (Olist a, [Maybe (Olist IAtom)])
unifyIdxPropForms :: Ord a => [IdxPropForm a] -> (Olist a, [PropForm IAtom])
unifyXForms :: Ord a => [XForm a] -> (Olist a, [IForm])
fromIdxPropForm :: Ord a => IdxPropForm a -> PropForm a
toIdxPropForm :: Ord a => PropForm a -> IdxPropForm a
newAtomsXForm :: Ord a => XForm a -> Olist a -> XForm a
iLIT :: ILit -> PropForm IAtom
iNLC :: ILine -> PropForm IAtom
iNLD :: ILine -> PropForm IAtom
iCNF :: IForm -> PropForm IAtom
iDNF :: IForm -> PropForm IAtom
xLIT :: Ord a => XLit a -> PropForm a
xNLC :: Ord a => XLine a -> PropForm a
xNLD :: Ord a => XLine a -> PropForm a
xCNF :: Ord a => XForm a -> PropForm a
xDNF :: Ord a => XForm a -> PropForm a
toXPDNF :: Ord a => PropForm a -> XPDNF a
toXPCNF :: Ord a => PropForm a -> XPCNF a
toM2DNF :: Ord a => PropForm a -> MixForm a
toM2CNF :: Ord a => PropForm a -> MixForm a
fromXPDNF :: Ord a => XPDNF a -> PropForm a
fromXPCNF :: Ord a => XPCNF a -> PropForm a
fromMixForm :: Ord a => MixForm a -> PropForm a
isIAtom :: Int -> Bool
isILit :: Int -> Bool
isILine :: Costack Int -> Bool
isIForm :: Costack (Costack Int) -> Bool
iLine :: [Int] -> ILine
iForm :: [[Int]] -> IForm
iAtom :: ILit -> IAtom
iBool :: ILit -> Bool
negLit :: ILit -> ILit
lineIndices :: ILine -> Olist IAtom
formIndices :: IForm -> Olist IAtom
lineLength :: ILine -> Int
formLength :: IForm -> Int
volume :: IForm -> Int
isOrderedForm :: IForm -> Bool
orderForm :: IForm -> IForm
atomForm :: IAtom -> IForm
botForm :: IForm
topForm :: IForm
formJoinForm :: IForm -> IForm -> IForm
formListJoin :: [IForm] -> IForm
lineMeetLine :: ILine -> ILine -> IForm
lineMeetForm :: ILine -> IForm -> IForm
formMeetForm :: IForm -> IForm -> IForm
formListMeet :: [IForm] -> IForm
dualLine :: ILine -> IForm
dualForm :: IForm -> IForm
invertLine :: ILine -> ILine
invertForm :: IForm -> IForm
negLine :: ILine -> IForm
negForm :: IForm -> IForm
formCojoinLine :: IForm -> ILine -> IForm
formCojoinForm :: IForm -> IForm -> IForm
formAntijoinLine :: IForm -> ILine -> IForm
formAntijoinForm :: IForm -> IForm -> IForm
elimLine :: ILine -> Olist IAtom -> ILine
elimForm :: IForm -> Olist IAtom -> IForm
lineCovLine :: ILine -> ILine -> Bool
lineCovForm :: ILine -> IForm -> Bool
formCovForm :: IForm -> IForm -> Bool
pairPartition :: ILine -> ILine -> (ILine, ILine, ILine, ILine)
data CaseSymbol
NOOO :: CaseSymbol
NOOP :: CaseSymbol
NOPO :: CaseSymbol
NOPP :: CaseSymbol
NIOO :: CaseSymbol
NIOP :: CaseSymbol
NIPO :: CaseSymbol
NIPP :: CaseSymbol
NMNN :: CaseSymbol
caseSymbol :: ILine -> ILine -> CaseSymbol
pairPrim' :: ILine -> ILine -> IForm
pairMin' :: ILine -> ILine -> IForm
xprim' :: ILine -> ILine -> (CaseSymbol, IForm)
xmin' :: ILine -> ILine -> (CaseSymbol, IForm)
xprim :: ILine -> ILine -> (CaseSymbol, IForm)
xmin :: ILine -> ILine -> (CaseSymbol, IForm)
pairPrim :: ILine -> ILine -> IForm
pairMin :: ILine -> ILine -> IForm
isMinimalPair :: ILine -> ILine -> Bool
allPairs :: [a] -> [(a, a)]
isPairwiseMinimal :: IForm -> Bool
cPrime :: ILine -> ILine -> Maybe ILine
cPrimes :: IForm -> IForm
mrec :: (IForm, IForm, IForm) -> IForm
m2form :: IForm -> IForm
iformJoinM2form :: IForm -> IForm -> IForm
primForm :: IForm -> IForm
iformJoinPrimForm :: IForm -> IForm -> IForm
xformAtoms :: Ord a => XForm a -> Olist a
xformRedAtoms :: Ord a => XForm a -> Olist a
xformIrrAtoms :: Ord a => XForm a -> Olist a
mixToPDNF :: Ord a => MixForm a -> MixForm a
mixToPCNF :: Ord a => MixForm a -> MixForm a
instance Show a => Show (XPDNF a)
instance Read a => Read (XPDNF a)
instance Eq a => Eq (XPDNF a)
instance Show a => Show (XPCNF a)
instance Read a => Read (XPCNF a)
instance Eq a => Eq (XPCNF a)
instance Show a => Show (MixForm a)
instance Read a => Read (MixForm a)
instance Eq a => Eq (MixForm a)
instance Show CaseSymbol
instance Read CaseSymbol
instance Eq CaseSymbol
instance Ord CaseSymbol
instance Ord a => PropAlg a (MixForm a)
instance Ord a => PropAlg a (XPCNF a)
instance Ord a => PropAlg a (XPDNF a)
instance Ord IForm
instance Ord ILine
instance Display a => Display (MixForm a)
instance Display a => Display (XPCNF a)
instance Display a => Display (XPDNF a)
instance Display a => Display (XForm a)
instance Display IForm

module PropLogicTest
pdnf' :: Ord a => PropForm a -> PDNF a
pcnf' :: Ord a => PropForm a -> PCNF a
spdnf' :: Ord a => PropForm a -> SimpleDNF a
spcnf' :: Ord a => PropForm a -> SimpleCNF a
xpdnf' :: Ord a => PropForm a -> XPDNF a
xpcnf' :: Ord a => PropForm a -> XPCNF a
pdnf :: String -> IO ()
pcnf :: String -> IO ()
spdnf :: String -> IO ()
spcnf :: String -> IO ()
xpdnf :: String -> IO ()
xpcnf :: String -> IO ()
randomListMember :: [a] -> IO a
randomChoice :: [a] -> IO (a, [a])
shuffle :: [a] -> IO [a]
randomSublist :: [a] -> IO [a]
nRandomRIO :: Int -> (Int, Int) -> IO [Int]
weightedRandomMember :: [(a, Int)] -> IO a
appleBasketDistribution :: Int -> Int -> IO [Int]
averageLineLength :: IForm -> Float
randomILine :: Int -> Int -> IO ILine
randomIForm :: Int -> Int -> Int -> IO IForm
randomXForm :: Ord a => [a] -> Int -> Int -> IO (XForm a)
randomDNF :: Ord a => [a] -> Int -> Int -> IO (DNF a)
randomCNF :: Ord a => [a] -> Int -> Int -> IO (CNF a)
randomCharDNF :: Int -> IO (DNF Char)
randomCharCNF :: Int -> IO (CNF Char)
randomIntDNF :: Int -> IO (DNF Int)
randomIntCNF :: Int -> IO (CNF Int)
type SizeTriple = (Int, Int, Int)
sizeTriple :: Ord a => PropForm a -> SizeTriple
data JunctorSymbol
T_ :: JunctorSymbol
F_ :: JunctorSymbol
N_ :: JunctorSymbol
CJ_ :: JunctorSymbol
DJ_ :: JunctorSymbol
SJ_ :: JunctorSymbol
EJ_ :: JunctorSymbol
type JunctorWeighting = [(JunctorSymbol, Int)]
defaultJunctorWeighting :: JunctorWeighting
weightedRandomPropForm :: JunctorWeighting -> Olist a -> (Int, Int) -> IO (PropForm a)
randomPropForm :: Olist a -> (Int, Int) -> IO (PropForm a)
randomCharProp :: SizeTriple -> IO (PropForm Char)
randomIntProp :: SizeTriple -> IO (PropForm Int)
axiom_reflexivity_of_subvalence :: PropAlg a p => p -> Bool
axiom_transitivity_of_subvalence :: PropAlg a p => (p, p, p) -> Bool
axiom_criterion_for_equivalence :: PropAlg a p => (p, p) -> Bool
test_prop_alg :: (Show a, Show p, PropAlg a p) => IO a -> IO p -> Int -> IO ()
total_test :: Int -> IO ()
type Msec = Integer
type CanonPerformance = (SizeTriple, (Msec, SizeTriple), (Msec, SizeTriple))
type Verbose = Bool
pnfCorrect :: (Display a, Show a, Ord a) => Verbose -> PropForm a -> IO (Either (PropForm a) CanonPerformance)
pnfCorrectRepeat :: Verbose -> (Int, Int, Int) -> IO (PropForm Char)
pnfPerform :: (Display a, Show a, Ord a) => PropForm a -> IO CanonPerformance
pnfPerformRandom :: SizeTriple -> IO CanonPerformance
pnfPerformRepeat :: SizeTriple -> IO ()
type Seconds = Double

-- | <pre>
--   randomPrimeTest (atomNum, formLen, averLineLen) = (atomNum', formLen', vol', secs')
--   </pre>
verboseRandomPrimeTest :: (Int, Int, Int) -> IO (Int, Int, Int, Seconds)

-- | <pre>
--   verboseRandomPrimeTesting (atomNum, formLen, averLineLen) numberOfTests = (maxFormLen, averFormLen, maxTime, averTime, standDev)
--   </pre>
verboseRandomPrimeTesting :: (Int, Int, Int) -> Int -> IO (Int, Int, Seconds, Seconds, Seconds)
meanValue :: [Seconds] -> Seconds
standDeviation :: [Seconds] -> Seconds
normSeconds :: Seconds -> Seconds
instance Eq JunctorSymbol
instance Ord JunctorSymbol
instance Show JunctorSymbol
instance Read JunctorSymbol


-- | A powerful system for <i>propositional logic</i>. Defines an abstract
--   concept of a <i>propositional algebra</i> and provides both default
--   and fast instances. Emphasizes the use of <i>(canonic)
--   normalizations</i> in general and so-called <i>Prime Normal Forms</i>
--   in particular.
--   
--   <a>http://www.bucephalus.org/PropLogic/</a>
--   
--   is the homepage with additional information for a variety of users,
--   including short and thorough introductions to the use of
--   <a>PropLogic</a> and the mathematical background of the whole design.
module PropLogic