Safe Haskell | None |
---|---|
Language | Haskell98 |
Basic stuff for propositional logic: datatype, parsing and
printing. IsPropositional
is a subclass of IsLiteral
of
formula types that support binary combinations.
- class IsLiteral formula => IsPropositional formula where
- data BinOp
- binop :: IsPropositional formula => formula -> BinOp -> formula -> formula
- (⇒) :: IsPropositional formula => formula -> formula -> formula
- (==>) :: IsPropositional formula => formula -> formula -> formula
- (⊃) :: IsPropositional formula => formula -> formula -> formula
- (→) :: IsPropositional formula => formula -> formula -> formula
- (⇔) :: IsPropositional formula => formula -> formula -> formula
- (<=>) :: IsPropositional formula => formula -> formula -> formula
- (↔) :: IsPropositional formula => formula -> formula -> formula
- (<==>) :: IsPropositional formula => formula -> formula -> formula
- (∧) :: IsPropositional formula => formula -> formula -> formula
- · :: IsPropositional formula => formula -> formula -> formula
- (∨) :: IsPropositional formula => formula -> formula -> formula
- foldPropositional :: JustPropositional pf => (pf -> BinOp -> pf -> r) -> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
- zipPropositional :: (JustPropositional pf1, JustPropositional pf2) => (pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r) -> (pf1 -> pf2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf pf1 -> AtomOf pf2 -> Maybe r) -> pf1 -> pf2 -> Maybe r
- convertPropositional :: (JustPropositional pf1, IsPropositional pf2) => (AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
- convertToPropositional :: (IsPropositional formula, JustPropositional pf) => (formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
- precedencePropositional :: JustPropositional pf => pf -> Precedence
- associativityPropositional :: JustPropositional pf => pf -> Associativity
- prettyPropositional :: forall pf. JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc
- showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS
- onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf
- overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r
- class IsPropositional formula => JustPropositional formula
- eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool
- atoms :: IsFormula formula => formula -> Set (AtomOf formula)
- data TruthTable a = TruthTable [a] [TruthTableRow]
- onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
- truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf)
- tautology :: JustPropositional pf => pf -> Bool
- unsatisfiable :: JustPropositional pf => pf -> Bool
- satisfiable :: JustPropositional pf => pf -> Bool
- psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula
- dual :: JustPropositional pf => pf -> pf
- psimplify :: IsPropositional formula => formula -> formula
- psimplify1 :: IsPropositional formula => formula -> formula
- nnf :: JustPropositional pf => pf -> pf
- nenf :: IsPropositional formula => formula -> formula
- list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
- list_disj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
- mk_lits :: (JustPropositional pf, Ord pf) => Set pf -> (AtomOf pf -> Bool) -> pf
- allsatvaluations :: Ord atom => ((atom -> Bool) -> Bool) -> (atom -> Bool) -> Set atom -> [atom -> Bool]
- dnfSet :: (JustPropositional pf, Ord pf) => pf -> pf
- purednf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
- simpdnf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
- rawdnf :: IsPropositional formula => formula -> formula
- dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
- purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
- simpcnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
- cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
- cnf_ :: (IsPropositional pf, Ord pf, JustLiteral lit) => (AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf
- trivial :: (Ord lit, IsLiteral lit) => Set lit -> Bool
- data Prop = P {}
- data PFormula atom
- testProp :: Test
Propositional formulas
class IsLiteral formula => IsPropositional formula where Source #
A type class for propositional logic. If the type we are writing an instance for is a zero-order (aka propositional) logic type there will generally by a type or a type parameter corresponding to atom. For first order or predicate logic types, it is generally easiest to just use the formula type itself as the atom type, and raise errors in the implementation if a non-atomic formula somehow appears where an atomic formula is expected (i.e. as an argument to atomic or to the third argument of foldPropositional.)
(.|.) :: formula -> formula -> formula infixl 4 Source #
Disjunction/OR
(.&.) :: formula -> formula -> formula infixl 5 Source #
Conjunction/AND. x .&. y = (.~.) ((.~.) x .|. (.~.) y)
(.<=>.) :: formula -> formula -> formula infixl 2 Source #
Equivalence. x .=. y = (x .=>. y) .&. (y .=>. x)
(.=>.) :: formula -> formula -> formula infixr 3 Source #
Implication. x .=>. y = ((.~.) x .|. y)
foldPropositional' :: (formula -> r) -> (formula -> BinOp -> formula -> r) -> (formula -> r) -> (Bool -> r) -> (AtomOf formula -> r) -> formula -> r Source #
A fold function that distributes different sorts of formula to its parameter functions, one to handle binary operators, one for negations, and one for atomic formulas. See examples of its use to implement the polymorphic functions below.
foldCombination :: (formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> formula -> r Source #
An alternative fold function for binary combinations of formulas
This type is used to construct the first argument of foldPropositional
.
binop :: IsPropositional formula => formula -> BinOp -> formula -> formula Source #
Combine formulas with a BinOp
, for use building the first
argument of foldPropositional
.
(⇒) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #
Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.
(==>) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #
Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.
(⊃) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #
Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.
(→) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #
Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.
(⇔) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #
If-and-only-if synonyms
(<=>) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #
If-and-only-if synonyms
(↔) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #
If-and-only-if synonyms
(<==>) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #
If-and-only-if synonyms
(∧) :: IsPropositional formula => formula -> formula -> formula infixl 5 Source #
And/conjunction synonyms
· :: IsPropositional formula => formula -> formula -> formula infixl 5 Source #
And/conjunction synonyms
(∨) :: IsPropositional formula => formula -> formula -> formula infixl 4 Source #
Or/disjunction synonyms
:: JustPropositional pf | |
=> (pf -> BinOp -> pf -> r) | fold on a binary operation formula |
-> (pf -> r) | fold on a negated formula |
-> (Bool -> r) | fold on a boolean formula |
-> (AtomOf pf -> r) | fold on an atomic formula |
-> pf | |
-> r |
Deconstruct a JustPropositional
formula.
:: (JustPropositional pf1, JustPropositional pf2) | |
=> (pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r) | Combine two binary operation formulas |
-> (pf1 -> pf2 -> Maybe r) | Combine two negated formulas |
-> (Bool -> Bool -> Maybe r) | Combine two boolean formulas |
-> (AtomOf pf1 -> AtomOf pf2 -> Maybe r) | Combine two atomic formulas |
-> pf1 | |
-> pf2 | |
-> Maybe r | Result is Nothing if the formulas don't unify |
Combine two JustPropositional
formulas if they are similar.
:: (JustPropositional pf1, IsPropositional pf2) | |
=> (AtomOf pf1 -> AtomOf pf2) | Convert an atomic formula |
-> pf1 | |
-> pf2 |
Convert any instance of JustPropositional
to any IsPropositional
formula.
convertToPropositional Source #
:: (IsPropositional formula, JustPropositional pf) | |
=> (formula -> pf) | Convert a higher order formula |
-> (AtomOf formula -> AtomOf pf) | Convert an atomic formula |
-> formula | |
-> pf |
Convert any instance of IsPropositional
to a JustPropositional
formula. Typically the
ho (higher order) argument calls error if it encounters something it can't handle.
precedencePropositional :: JustPropositional pf => pf -> Precedence Source #
Implementation of precedence
for any JustPropostional
type.
associativityPropositional :: JustPropositional pf => pf -> Associativity Source #
prettyPropositional :: forall pf. JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc Source #
Implementation of pPrint
for any JustPropostional
type.
showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS Source #
Implementation of show
for any JustPropositional
type. For clarity, show methods fully parenthesize
onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf Source #
Implementation of onatoms
for any JustPropositional
type.
overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r Source #
Implementation of overatoms
for any JustPropositional
type.
Restricted propositional formula class
class IsPropositional formula => JustPropositional formula Source #
Class that indicates a formula type *only* supports Propositional features - it has no way to represent quantifiers.
IsAtom atom => JustPropositional (PFormula atom) Source # | |
Interpretation of formulas.
eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool Source #
Interpretation of formulas.
atoms :: IsFormula formula => formula -> Set (AtomOf formula) Source #
Return the set of propositional variables in a formula.
Truth Tables
data TruthTable a Source #
TruthTable [a] [TruthTableRow] |
Eq a => Eq (TruthTable a) Source # | |
Show a => Show (TruthTable a) Source # | |
Pretty atom => Pretty (TruthTable atom) Source # | |
onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r Source #
truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf) Source #
Code to print out truth tables.
Tautologies and related concepts
tautology :: JustPropositional pf => pf -> Bool Source #
Recognizing tautologies.
unsatisfiable :: JustPropositional pf => pf -> Bool Source #
Related concepts.
satisfiable :: JustPropositional pf => pf -> Bool Source #
Substitution
psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula Source #
Substitution operation.
Dualization
dual :: JustPropositional pf => pf -> pf Source #
Dualization.
Simplification
psimplify :: IsPropositional formula => formula -> formula Source #
Routine simplification.
psimplify1 :: IsPropositional formula => formula -> formula Source #
Normal forms
nnf :: JustPropositional pf => pf -> pf Source #
Negation normal form.
nenf :: IsPropositional formula => formula -> formula Source #
list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula Source #
Disjunctive normal form (DNF) via truth tables.
list_disj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula Source #
allsatvaluations :: Ord atom => ((atom -> Bool) -> Bool) -> (atom -> Bool) -> Set atom -> [atom -> Bool] Source #
dnfSet :: (JustPropositional pf, Ord pf) => pf -> pf Source #
purednf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #
simpdnf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #
With subsumption checking, done very naively (quadratic).
rawdnf :: IsPropositional formula => formula -> formula Source #
dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf Source #
Mapping back to a formula.
purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #
Conjunctive normal form (CNF) by essentially the same code. (p. 60)
simpcnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #
cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf Source #
cnf_ :: (IsPropositional pf, Ord pf, JustLiteral lit) => (AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf Source #
trivial :: (Ord lit, IsLiteral lit) => Set lit -> Bool Source #
Filtering out trivial disjuncts (in this guise, contradictory).
Instance
An instance of IsPredicate.
An instance of IsPropositional.
F | |
T | |
Atom atom | |
Not (PFormula atom) | |
And (PFormula atom) (PFormula atom) | |
Or (PFormula atom) (PFormula atom) | |
Imp (PFormula atom) (PFormula atom) | |
Iff (PFormula atom) (PFormula atom) |
Eq atom => Eq (PFormula atom) Source # | |
Data atom => Data (PFormula atom) Source # | |
Ord atom => Ord (PFormula atom) Source # | |
Read atom => Read (PFormula atom) Source # | |
(IsPropositional (PFormula atom), Show atom) => Show (PFormula atom) Source # | |
IsAtom atom => Pretty (PFormula atom) Source # | |
IsAtom atom => HasFixity (PFormula atom) Source # | |
IsAtom atom => IsFormula (PFormula atom) Source # | |
IsAtom atom => IsLiteral (PFormula atom) Source # | |
IsAtom atom => JustPropositional (PFormula atom) Source # | |
IsAtom atom => IsPropositional (PFormula atom) Source # | |
type AtomOf (PFormula atom) Source # | |