| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

This module comprises the abstract definition of two core concepts of propositional logic: - The data type
`(`of`PropForm`a)*propositional formulas*, based on a given*atom*type`a`. - The two-parameter type class
`(`of a`PropAlg`a p)*propositional algebra*, where`a`is the*atom*type and`p`the type of*propositions*. Operations of such a structure include a decision if two propositions are`equivalent`, if a given proposition is`satisfiable`, a converter`toPropForm`and the inverse`fromPropForm`, which turns a propositional formula into a proposition.
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Synopsis | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Propositional formulas | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

data PropForm a | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

A typical example of a propositional formula φ in standard mathematical notation is given by ¬(rain ∧ snow) ∧ (wet ↔ (rain ∨ snow)) ∧ (rain → hot) ∧ (snow → ¬ hot) The primitive elements CJ [N (CJ [A "rain", A "snow"]), EJ [A "wet", DJ [A "rain", A "snow"]], SJ [A "rain", A "hot"], SJ [A "snow", N (A "hot")]] This Haskell version is more tedious and we introduce a third notation for nicer output by making [-[rain * snow] * [wet <-> [rain + snow]] * [rain -> hot] * [snow -> -hot]] The following overview compares the different representations: Haskell displayed as kind of formula -------------------------------------------------------------------- A x x (without quotes) atomic formula F false the boolean zero value T true the boolean unit value N p -p negation CJ [p1,...,pN] [p1 * ... * pN] conjunction DJ [p1,...,pN] [p1 + ... + pN] disjunction SJ [p1,...,pN] [p1 -> ... -> pN] subjunction EJ [p1,...,pN] [p1 <-> ... <-> pN] equijunction Note, that the negation is unary, as usual, but the last four constructors are all multiary junctions, i.e. the list
, so String conversion (and displaying results in the interpreter) are
well defined. For example
Showshow (CJ [A 3, N (A 7), A 4]) == "CJ [A 3,N (A 7),A 4]" Note, that reading a formula, e.g. read "SJ [A 3, A 4, T]" issues a complaint due to the ambiguity of the atom type. But that can be fixed, e.g. by stating the type explicitely, as in (read "SJ [A 3, A 4, T]") :: PropForm Integer | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Parsing propositional formulas on string atoms | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

stringToProp :: String -> PropForm String | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

... CONTINUEHERE .... | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Propositional algebras | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

class Ord a => PropAlg a p | p -> a where | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

atomic proposition constructor, similar to the constructor A for atomic formulas.
Similar to the definition of and neg :: p-> pconj, disj, subj, equij :: [p] -> pThere the set of ...................................................................... | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Produced by Haddock version 2.4.2 |