​

DA.Logic

Logic - Propositional calculus.

​

Module Snapshot

​

Data Types

​

data Formula t

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

• 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 Instances:

• 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

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

​

false

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

​

neg

neg : Formula t -> Formula t neg is the ¬ (negation) operation of the boolean algebra of formulas.

​

conj

conj : [Formula t] -> Formula t conj is a list version of &&&, enabled by the associativity of ∧.

​

disj

disj : [Formula t] -> Formula t disj is a list version of |||, enabled by the associativity of ∨.

​

fromBool

fromBool : Bool -> Formula t fromBool converts True to true and False to false.

​

toNNF

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

​

toDNF

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

​

traverse

traverse : Applicative f => (t -> f s) -> Formula t -> f (Formula s) An implementation of traverse in the usual sense.

​

zipFormulas

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

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

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

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

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

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

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.

​

Orphan Typeclass Instances

• instance Eq t => Eq (Formula t)
• instance Ord t => Ord (Formula t)
• instance Show t => Show (Formula t)
• instance Functor Formula
• instance Applicative Formula
• instance Action Formula