Data.Logic.Propositional
Description
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 String
- | Negation Expr
- | Conjunction Expr Expr
- | Disjunction Expr Expr
- | Conditional Expr Expr
- | Biconditional Expr Expr
- type Mapping = Map String Bool
- equivalent :: Expr -> Expr -> Bool
- interpret :: Expr -> Mapping -> Bool
- assignments :: Expr -> [Mapping]
- 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
- variables :: Expr -> [String]
Documentation
Constructors
| Variable String | |
| Negation Expr | |
| Conjunction Expr Expr | |
| Disjunction Expr Expr | |
| Conditional Expr Expr | |
| Biconditional Expr Expr |
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.
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:
"(φ <-> ψ)"
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.