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

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'

Arguments

:: (formula -> r)

fold on some higher order formula

-> (formula -> BinOp -> formula -> r)

fold on a binary operation formula. Functions of this type can be constructed using binop.

-> (formula -> r)

fold on a negated formula

-> (Bool -> r)

fold on a boolean formula

-> (AtomOf formula -> r)

fold on an atomic formula

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

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

data BinOp

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

Constructors

(:<=>:)

(:=>:)

(:&:)

(:|:)

Instances

Bounded BinOp

Enum BinOp

Eq BinOp

Data BinOp

Ord BinOp

Show BinOp

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)

Show a => Show (TruthTable a)

Pretty atom => Pretty (TruthTable atom)

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

Ord Prop

Show Prop

IsString Prop

Pretty Prop

HasFixity Prop

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)

Data atom => Data (PFormula atom)

Ord atom => Ord (PFormula atom)

Read atom => Read (PFormula atom)

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

IsAtom atom => Pretty (PFormula atom)

IsAtom atom => HasFixity (PFormula atom)

IsAtom atom => IsFormula (PFormula atom)

IsAtom atom => IsLiteral (PFormula atom)

IsAtom atom => JustPropositional (PFormula atom)

IsAtom atom => IsPropositional (PFormula atom)

type AtomOf (PFormula atom) = atom

Tests

testProp :: Test