# Module 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 p` is the formula p
For a formula f, `Negation f` is ¬f
For formulas f1, …, fn, `Conjunction [f1, ..., fn]` is f1 ∧ … ∧ fn
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 == Right True` and `toBool false == Right False`. Otherwise, it returns `Left x`, where `x` is the input.

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.