DefaultPropLogic

Syntactic operations

Formula Deconstructors

juncDeg

juncArgs

juncCons

Size

atomSize

juncSize

size

Linear syntactic order on formulas

Semantics

Valuators and formulas as functions

type LiteralPair a

type Valuator a

correctValuator

valuate

boolEval

boolApply

allValuators

zeroValuators

unitValuators

Truth tables

type TruthTable a

correctTruthTable

truthTable

plainTruthTable

truthTableBy

Multiple truth tables

type MultiTruthTable a

correctMultiTruthTable

multiTruthTable

Mutual converters between syntax and semantics

valuatorToNLC

valuatorToNLD

valuatorListToCNF

valuatorListToDNF

nlcToValuator

nldToValuator

cnfToValuatorList

dnfToValuatorList

truthTableZeroValuators

truthTableUnitValuators

truthTableToDNF

truthTableToCNF

Normal Forms

Normalizations and Canonizations in general

Definition

Normalizations in Propositional Algebras

Default semantic normalizations

Ordered Propositional Formulas

type OrdPropForm a

isOrdPropForm

ordPropForm

Evaluated Normal Forms

type EvalNF a

isEvalNF

Generalized evaluation and application for formulas: eval and apply

eval

apply

Literal Form(ula)s

type LitForm a

isLitForm

litFormAtom

litFormValue

Negation Normal Forms

type NegNormForm a

isNegNormForm

negNormForm

NLCs and NLDs, CNFs and DNFs

type NLC a

isNLC

type NLD a

isNLD

type CNF a

isCNF

type DNF a

isDNF

Natural DNFs and CNFs

type NaturalDNF a

type NaturalCNF a

isNaturalDNF

isNaturalCNF

naturalDNF

naturalCNF

Prime DNFs and CNFs

Formal definition

Prime Disjunctive Normal Forms

Prime Conjunctive Normal Forms

The Haskell types and functions

type PDNF a

type PCNF a

primeDNF

primeCNF

The default and the fast generation of Prime Normal Forms

validates

falsifies

directSubvaluators

allDirectSubvalidators

allDirectSubfalsifiers

primeValuators

coprimeValuators

Reference to the fast generation of Prime Normal Forms

Minimal DNFs and CNFs

type MDNF a

type MCNF a

minimalDNFs

minimalCNFs

Simplified DNFs and CNFs

type SimpleDNF a

type SimpleCNF a

simpleDNF

simpleCNF

Propositional algebras

PropAlg a (PropForm a), the Propositional Formula Algebra

ext'

PropAlg a (PropForm a), the Truth Table Algebra

PropAlg Void Bool, the Boolean Value Algebra