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


-- | An implementation of propositional logic in Haskell
--   
--   Proper is both an executable theorem prover for Propositional logic
--   and a library for incorporating propositional logic into other Haskell
--   programs. See the github repo for examples of theorem files for the
--   executable.
@package Proper
@version 0.5.2.0

module Proper.Utils
type Name = String
data Error a
Succeeded :: a -> Error a
Failed :: String -> Error a
extractValue :: Error a -> a
instance Show a => Show (Error a)
instance Monad Error

module Proper.Clause
data Atom a
atom :: Atom t -> t
negation :: Atom a -> Atom a
lit :: a -> Atom a
nLit :: a -> Atom a
literal :: Atom a -> Atom a
type Clause c = Set (Atom c)
clause :: Ord a => [Atom a] -> Clause a
concatClause :: Ord c => Clause c -> Clause c -> Clause c
assignTruthVal :: Atom l -> Bool
instance Eq a => Eq (Atom a)
instance Ord a => Ord (Atom a)
instance Show a => Show (Atom a)

module Proper.CNF
type CNF c = Set (Clause c)
type SatisfyingAssignment l = Map l Bool
cnf :: Ord c => [Clause c] -> CNF c
mergeCNFFormulas :: Ord c => [CNF c] -> CNF c
naiveSAT :: Ord c => CNF c -> Maybe (SatisfyingAssignment c)
naiveSATBool :: Ord c => CNF c -> Bool

module Proper.BDD
data BDD p
trueBDD :: BDD p
falseBDD :: BDD p
singletonBDD :: p -> BDD p
negBDD :: Eq p => BDD p -> BDD p
disBDD :: Ord p => BDD p -> BDD p -> BDD p
conBDD :: Ord p => BDD p -> BDD p -> BDD p
impBDD :: Ord p => BDD p -> BDD p -> BDD p
bicBDD :: Ord p => BDD p -> BDD p -> BDD p
isTaut :: BDD t -> Bool
instance Eq p => Eq (BDD p)
instance Show p => Show (BDD p)

module Proper.Formula
data Formula s
checkTheorem :: (Ord s, Show s) => Theorem s -> Bool
neg :: Formula s -> Formula s
con :: Formula s -> Formula s -> Formula s
dis :: Formula s -> Formula s -> Formula s
val :: s -> Formula s
bic :: Formula s -> Formula s -> Formula s
imp :: Formula s -> Formula s -> Formula s
truthAssignment :: Ord s => [s] -> [Bool] -> TruthAssignment s
evalFormula :: (Ord s, Show s) => TruthAssignment s -> Formula s -> Bool
isValidByTruthTable :: (Ord s, Show s) => Formula s -> Bool
toCNF :: (Ord s, Show s) => Formula s -> CNF s
theorem :: [Formula s] -> Formula s -> Theorem s
bddCheckTaut :: Ord s => Formula s -> Bool
instance Eq s => Eq (Formula s)
instance Ord s => Ord (Formula s)
instance Eq s => Eq (Theorem s)
instance Show s => Show (Theorem s)
instance Show s => Show (Formula s)
instance Foldable Formula
instance Functor Formula