Safe Haskell | None |
---|

The Data.Logic.Propositional module provides a set of functions for parsing, manipulating and generating truth tables for expressions in classical propositional logic.

The core of the API is the `Expr`

data type, which has constructors for all
the usual expression forms: variables, standing for atomic propositions;
negation, the only unary connective; and the binary connectives of
conjunction, disjunction, material implication and logical equivalence.

- data Expr
- = Variable Var
- | Negation Expr
- | Conjunction Expr Expr
- | Disjunction Expr Expr
- | Conditional Expr Expr
- | Biconditional Expr Expr

- newtype Var = Var Char
- type Mapping = Map Var Bool
- equivalent :: Expr -> Expr -> Bool
- interpret :: Expr -> Mapping -> Bool
- assignments :: Expr -> [Mapping]
- values :: Expr -> [Bool]
- variables :: Expr -> [Var]
- isContingent :: Expr -> Bool
- isContradiction :: Expr -> Bool
- isTautology :: Expr -> Bool
- parseExpr :: SourceName -> String -> Either ParseError Expr
- show :: Show a => a -> String
- showAscii :: Expr -> String
- truthTable :: Expr -> String
- truthTableP :: Printer -> Expr -> String

# Documentation

equivalent :: Expr -> Expr -> BoolSource

Determines whether two expressions are extensionally equivalent (that is, have the same values under all interpretations).

interpret :: Expr -> Mapping -> BoolSource

In order to interpret an expression, a mapping from variables to truth
values needs to be provided. Truth values are compositional; that's to say,
the value of a composite expression (any expression which is not atomic)
depends on the truth values of its component parts. For example, the Haskell
expression below would evaluate to `False`

.

interpret (Conjunction (Variable "A") (Variable "B")) (fromList [("A", True), ("B", False)])

assignments :: Expr -> [Mapping]Source

Generates the possible assignments of variables in an expression.

values :: Expr -> [Bool]Source

Lists the values of an expression under all interpretations (that is, all assignments of values to variables).

isContingent :: Expr -> BoolSource

Determines whether an expression is contingent (that is, true in at least one interpretation and false in at least one interpretation).

isContradiction :: Expr -> BoolSource

Determines whether an expression is contradictory.

isTautology :: Expr -> BoolSource

Determines whether an expression is tautological.

parseExpr :: SourceName -> String -> Either ParseError ExprSource

The `parseExpr`

function accepts the name of a source, and a string to be
parsed, and attempts to parse the string as a logical expression of the
following forms, where `φ`

and `ψ`

are metalinguistic variables
standing for any valid expression.

- Variables:
`"P"`

,`"Q"`

,`"a"`

,`"b"`

etc.; basically anything in the character class`[a-zA-Z]`

- Negation:
`"~φ"`

- Conjunction:
`"(φ & ψ)"`

- Disjunction:
`"(φ | ψ)"`

- Conditional:
`"(φ -> ψ)"`

- Biconditional:
`"(φ <-> ψ)"`

Top-level expressions where the primary connective is a binary one do not
need to be parenthesised. For example, `"p -> (q & r)"`

is a valid
expression, although `"(p -> (q & r))"`

is also fine.

showAscii :: Expr -> StringSource

Represents expressions using only ASCII characters (the `show`

function
pretty-prints expressions using logical symbols only present in extended
character sets).

truthTable :: Expr -> StringSource

The `truthTable`

function produces a truth table for the given expression.

truthTableP :: Printer -> Expr -> StringSource

The `truthTableP`

is a configurable version of `truthTable`

which allows a
printer function to be selected, so for example one can print ASCII truth
tables by passing `showAscii`

to `truthTableP`

instead of `show`

.