Data.Logic.ATP.Prop

Basic stuff for propositional logic: datatype, parsing and printing. IsPropositional is a subclass of IsLiteral of formula types that support binary combinations.

Propositional formulas

class IsLiteral formula => IsPropositional formula where

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

Minimal complete definition

(.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination

Methods

(.|.) :: formula -> formula -> formula infixl 4

Disjunction/OR

(.&.) :: formula -> formula -> formula infixl 5

Conjunction/AND. x .&. y = (.~.) ((.~.) x .|. (.~.) y)

(.<=>.) :: formula -> formula -> formula infixl 2

Equivalence. x .=. y = (x .=>. y) .&. (y .=>. x)

(.=>.) :: formula -> formula -> formula infixr 3

Implication. x .=>. y = ((.~.) x .|. y)

foldPropositional' :: (formula -> r) -> (formula -> BinOp -> formula -> r) -> (formula -> r) -> (Bool -> r) -> (AtomOf formula -> r) -> formula -> r

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

An alternative fold function for binary combinations of formulas

Instances

IsAtom atom => IsPropositional (PFormula atom)

Methods

(.|.) :: PFormula atom -> PFormula atom -> PFormula atom

(.&.) :: PFormula atom -> PFormula atom -> PFormula atom

(.<=>.) :: PFormula atom -> PFormula atom -> PFormula atom

(.=>.) :: PFormula atom -> PFormula atom -> PFormula atom

foldPropositional' :: (PFormula atom -> r) -> (PFormula atom -> BinOp -> PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r

foldCombination :: (PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> PFormula atom -> r

(IsFormula (QFormula v atom), HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsPropositional (QFormula v atom)

Methods

(.|.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

(.&.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

(.<=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

(.=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

foldPropositional' :: (QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r

foldCombination :: (QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> QFormula v atom -> r

data BinOp

This type is used to construct the first argument of foldPropositional.

Constructors

(:<=>:)

(:=>:)

(:&:)

(:|:)

Instances

Bounded BinOp

Methods

minBound :: BinOp

maxBound :: BinOp

Enum BinOp

Methods

succ :: BinOp -> BinOp

pred :: BinOp -> BinOp

toEnum :: Int -> BinOp

fromEnum :: BinOp -> Int

enumFrom :: BinOp -> [BinOp]

enumFromThen :: BinOp -> BinOp -> [BinOp]

enumFromTo :: BinOp -> BinOp -> [BinOp]

enumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp]

Eq BinOp

Methods

(==) :: BinOp -> BinOp -> Bool

(/=) :: BinOp -> BinOp -> Bool

Data BinOp

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BinOp -> c BinOp

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BinOp

toConstr :: BinOp -> Constr

dataTypeOf :: BinOp -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BinOp)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp)

gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r

gmapQ :: (forall d. Data d => d -> u) -> BinOp -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOp -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp

Ord BinOp

Methods

compare :: BinOp -> BinOp -> Ordering

(<) :: BinOp -> BinOp -> Bool

(<=) :: BinOp -> BinOp -> Bool

(>) :: BinOp -> BinOp -> Bool

(>=) :: BinOp -> BinOp -> Bool

max :: BinOp -> BinOp -> BinOp

min :: BinOp -> BinOp -> BinOp

Show BinOp

Methods

showsPrec :: Int -> BinOp -> ShowS

show :: BinOp -> String

showList :: [BinOp] -> ShowS

binop :: IsPropositional formula => formula -> BinOp -> formula -> formula

Combine formulas with a BinOp, for use building the first argument of foldPropositional.

(⇒) :: IsPropositional formula => formula -> formula -> formula infixr 3

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

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

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

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

If-and-only-if synonyms

(<=>) :: IsPropositional formula => formula -> formula -> formula infixl 2

If-and-only-if synonyms

(↔) :: IsPropositional formula => formula -> formula -> formula infixl 2

If-and-only-if synonyms

(<==>) :: IsPropositional formula => formula -> formula -> formula infixl 2

If-and-only-if synonyms

(∧) :: IsPropositional formula => formula -> formula -> formula infixl 5

And/conjunction synonyms

· :: IsPropositional formula => formula -> formula -> formula infixl 5

And/conjunction synonyms

(∨) :: IsPropositional formula => formula -> formula -> formula infixl 4

Or/disjunction synonyms

foldPropositional

Arguments

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

zipPropositional

Arguments

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

convertPropositional

Arguments

:: (JustPropositional pf1, IsPropositional pf2)

=> (AtomOf pf1 -> AtomOf pf2)

Convert an atomic formula

-> pf1

-> pf2

Convert any instance of JustPropositional to any IsPropositional formula.

convertToPropositional

Arguments

:: (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

Implementation of precedence for any JustPropostional type.

associativityPropositional :: JustPropositional pf => pf -> Associativity

prettyPropositional :: forall pf. JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc

Implementation of pPrint for any JustPropostional type.

showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS

Implementation of show for any JustPropositional type. For clarity, show methods fully parenthesize

onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf

Implementation of onatoms for any JustPropositional type.

overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r

Implementation of overatoms for any JustPropositional type.

Restricted propositional formula class

class IsPropositional formula => JustPropositional formula

Class that indicates a formula type *only* supports Propositional features - it has no way to represent quantifiers.

Instances

IsAtom atom => JustPropositional (PFormula atom)

Interpretation of formulas.

eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool

Interpretation of formulas.

atoms :: IsFormula formula => formula -> Set (AtomOf formula)

Return the set of propositional variables in a formula.

Truth Tables

data TruthTable a

Constructors

TruthTable [a] [TruthTableRow]

Instances

Eq a => Eq (TruthTable a)

Methods

(==) :: TruthTable a -> TruthTable a -> Bool

(/=) :: TruthTable a -> TruthTable a -> Bool

Show a => Show (TruthTable a)

Methods

showsPrec :: Int -> TruthTable a -> ShowS

show :: TruthTable a -> String

showList :: [TruthTable a] -> ShowS

Pretty atom => Pretty (TruthTable atom)

Methods

pPrintPrec :: PrettyLevel -> Rational -> TruthTable atom -> Doc

pPrint :: TruthTable atom -> Doc

pPrintList :: PrettyLevel -> [TruthTable atom] -> Doc

onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r

truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf)

Code to print out truth tables.

Tautologies and related concepts

tautology :: JustPropositional pf => pf -> Bool

Recognizing tautologies.

unsatisfiable :: JustPropositional pf => pf -> Bool

Related concepts.

satisfiable :: JustPropositional pf => pf -> Bool

Substitution

psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula

Substitution operation.

Dualization

dual :: JustPropositional pf => pf -> pf

Dualization.

Simplification

psimplify :: IsPropositional formula => formula -> formula

Routine simplification.

psimplify1 :: IsPropositional formula => formula -> formula

Normal forms

nnf :: JustPropositional pf => pf -> pf

Negation normal form.

nenf :: IsPropositional formula => formula -> formula

list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula

Disjunctive normal form (DNF) via truth tables.

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)

With subsumption checking, done very naively (quadratic).

rawdnf :: IsPropositional formula => formula -> formula

dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf

Mapping back to a formula.

purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)

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)

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

Filtering out trivial disjuncts (in this guise, contradictory).

Instance

data Prop

An instance of IsPredicate.

Constructors

P

Fields

• pname :: String

Instances

Eq Prop

Methods

(==) :: Prop -> Prop -> Bool

(/=) :: Prop -> Prop -> Bool

Ord Prop

Methods

compare :: Prop -> Prop -> Ordering

(<) :: Prop -> Prop -> Bool

(<=) :: Prop -> Prop -> Bool

(>) :: Prop -> Prop -> Bool

(>=) :: Prop -> Prop -> Bool

max :: Prop -> Prop -> Prop

min :: Prop -> Prop -> Prop

Show Prop

Methods

showsPrec :: Int -> Prop -> ShowS

show :: Prop -> String

showList :: [Prop] -> ShowS

IsString Prop

Methods

fromString :: String -> Prop

Pretty Prop

Methods

pPrintPrec :: PrettyLevel -> Rational -> Prop -> Doc

pPrint :: Prop -> Doc

pPrintList :: PrettyLevel -> [Prop] -> Doc

HasFixity Prop

Methods

precedence :: Prop -> Precedence

associativity :: Prop -> Associativity

IsAtom Prop

data PFormula atom

An instance of IsPropositional.

Constructors

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)

Instances

Eq atom => Eq (PFormula atom)

Methods

(==) :: PFormula atom -> PFormula atom -> Bool

(/=) :: PFormula atom -> PFormula atom -> Bool

Data atom => Data (PFormula atom)

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PFormula atom -> c (PFormula atom)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PFormula atom)

toConstr :: PFormula atom -> Constr

dataTypeOf :: PFormula atom -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (PFormula atom))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PFormula atom))

gmapT :: (forall b. Data b => b -> b) -> PFormula atom -> PFormula atom

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PFormula atom -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PFormula atom -> r

gmapQ :: (forall d. Data d => d -> u) -> PFormula atom -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PFormula atom -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PFormula atom -> m (PFormula atom)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PFormula atom -> m (PFormula atom)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PFormula atom -> m (PFormula atom)

Ord atom => Ord (PFormula atom)

Methods

compare :: PFormula atom -> PFormula atom -> Ordering

(<) :: PFormula atom -> PFormula atom -> Bool

(<=) :: PFormula atom -> PFormula atom -> Bool

(>) :: PFormula atom -> PFormula atom -> Bool

(>=) :: PFormula atom -> PFormula atom -> Bool

max :: PFormula atom -> PFormula atom -> PFormula atom

min :: PFormula atom -> PFormula atom -> PFormula atom

Read atom => Read (PFormula atom)

Methods

readsPrec :: Int -> ReadS (PFormula atom)

readList :: ReadS [PFormula atom]

readPrec :: ReadPrec (PFormula atom)

readListPrec :: ReadPrec [PFormula atom]

(IsPropositional (PFormula atom), Show atom) => Show (PFormula atom)

Methods

showsPrec :: Int -> PFormula atom -> ShowS

show :: PFormula atom -> String

showList :: [PFormula atom] -> ShowS

IsAtom atom => Pretty (PFormula atom)

Methods

pPrintPrec :: PrettyLevel -> Rational -> PFormula atom -> Doc

pPrint :: PFormula atom -> Doc

pPrintList :: PrettyLevel -> [PFormula atom] -> Doc

IsAtom atom => HasFixity (PFormula atom)

Methods

precedence :: PFormula atom -> Precedence

associativity :: PFormula atom -> Associativity

IsAtom atom => IsFormula (PFormula atom)

Associated Types

type AtomOf (PFormula atom) :: *

Methods

true :: PFormula atom

false :: PFormula atom

asBool :: PFormula atom -> Maybe Bool

atomic :: AtomOf (PFormula atom) -> PFormula atom

overatoms :: (AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r

onatoms :: (AtomOf (PFormula atom) -> AtomOf (PFormula atom)) -> PFormula atom -> PFormula atom

IsAtom atom => IsLiteral (PFormula atom)

Methods

naiveNegate :: PFormula atom -> PFormula atom

foldNegation :: (PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r

foldLiteral' :: (PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r

IsAtom atom => JustPropositional (PFormula atom)

IsAtom atom => IsPropositional (PFormula atom)

Methods

(.|.) :: PFormula atom -> PFormula atom -> PFormula atom

(.&.) :: PFormula atom -> PFormula atom -> PFormula atom

(.<=>.) :: PFormula atom -> PFormula atom -> PFormula atom

(.=>.) :: PFormula atom -> PFormula atom -> PFormula atom

foldPropositional' :: (PFormula atom -> r) -> (PFormula atom -> BinOp -> PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r

foldCombination :: (PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> PFormula atom -> r

type AtomOf (PFormula atom)

type AtomOf (PFormula atom) = atom

Tests

testProp :: Test