| Safe Haskell | None |
|---|
Language.Boogie.NormalForm
Description
Various normal forms of Boolean expressions
- negationNF :: Expression -> Expression
- prenexNF :: Expression -> Expression
- normalize :: Expression -> Expression
Documentation
negationNF :: Expression -> ExpressionSource
Negation normal form of a Boolean expression:
no negation above boolean connectives, quantifiers or relational operators;
no boolean connectives except && and ||
prenexNF :: Expression -> ExpressionSource
Prenex normal form of a Boolean expression: all quantifiers are pushed to the outside and any two quantifiers of the same kind in a row are glued together. Requires expression to be in the negation normal form.
normalize :: Expression -> ExpressionSource
Negation and prenex normal form of a Boolean expression