DA.Logic

Logic - Propositional calculus.

Data Types

data Formula t

A Formula t is a formula in propositional calculus with propositions of type t.

Proposition t

Proposition p is the formula p

Negation (Formula t)

For a formula f, Negation f is ¬f

Conjunction [Formula t]

For formulas f1, ..., fn, Conjunction [f1, ..., fn] is f1 ∧ ... ∧ fn

Disjunction [Formula t]

For formulas f1, ..., fn, Disjunction [f1, ..., fn] is f1 ∨ ... ∨ fn

instance Action Formula

instance Applicative Formula

instance Functor Formula

instance Eq t => Eq (Formula t)

instance Ord t => Ord (Formula t)

instance Show t => Show (Formula t)

Functions

(&&&)

: Formula t -> Formula t -> Formula t

&&& is the ∧ operation of the boolean algebra of formulas, to be read as "and"

(|||)

: Formula t -> Formula t -> Formula t

||| is the ∨ operation of the boolean algebra of formulas, to be read as "or"

true

: Formula t

true is the 1 element of the boolean algebra of formulas, represented as an empty conjunction.

false

: Formula t

false is the 0 element of the boolean algebra of formulas, represented as an empty disjunction.

neg

: Formula t -> Formula t

neg is the ¬ (negation) operation of the boolean algebra of formulas.

conj

: [Formula t] -> Formula t

conj is a list version of &&&, enabled by the associativity of ∧.

disj

: [Formula t] -> Formula t

disj is a list version of |||, enabled by the associativity of ∨.

fromBool

: Bool -> Formula t

fromBool converts True to true and False to false.

toNNF

: Formula t -> Formula t

toNNF transforms a formula to negation normal form (see https://en.wikipedia.org/wiki/Negation_normal_form).

toDNF

: Formula t -> Formula t

toDNF turns a formula into disjunctive normal form. (see https://en.wikipedia.org/wiki/Disjunctive_normal_form).

traverse

: Applicative f => (t -> f s) -> Formula t -> f (Formula s)

An implementation of traverse in the usual sense.

zipFormulas

: Formula t -> Formula s -> Formula (t, s)

zipFormulas takes to formulas of same shape, meaning only propositions are different and zips them up.

substitute

: (t -> Optional Bool) -> Formula t -> Formula t

substitute takes a truth assignment and substitutes True or False into the respective places in a formula.

reduce

: Formula t -> Formula t

reduce reduces a formula as far as possible by:

1. Removing any occurrences of true and false;

2. Removing directly nested Conjunctions and Disjunctions;

3. Going to negation normal form.

isBool

: Formula t -> Optional Bool

isBool attempts to convert a formula to a bool. It satisfies isBool true == Some True and isBool false == Some False. Otherwise, it returns None.

interpret

: (t -> Optional Bool) -> Formula t -> Either (Formula t) Bool

interpret is a version of toBool that first substitutes using a truth function and then reduces as far as possible.

substituteA

: Applicative f => (t -> f (Optional Bool)) -> Formula t -> f (Formula t)

substituteA is a version of substitute that allows for truth values to be obtained from an action.

interpretA

: Applicative f => (t -> f (Optional Bool)) -> Formula t -> f (Either (Formula t) Bool)

interpretA is a version of interpret that allows for truth values to be obtained form an action.