Data.Logic.Propositional

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.

Documentation

data Expr

Constructors

Variable Var

Negation Expr

Conjunction Expr Expr

Disjunction Expr Expr

Conditional Expr Expr

Biconditional Expr Expr

Instances

Eq Expr

Show Expr

Arbitrary Expr

newtype Var

Constructors

Var Char

Instances

Eq Var

Ord Var

Show Var

Arbitrary Var

type Mapping = Map Var Bool

equivalent :: Expr -> Expr -> Bool

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

interpret :: Expr -> Mapping -> Bool

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]

Generates the possible assignments of variables in an expression.

values :: Expr -> [Bool]

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

variables :: Expr -> [Var]

Lists the names of variables present in an expression.

isContingent :: Expr -> Bool

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

isContradiction :: Expr -> Bool

Determines whether an expression is contradictory.

isTautology :: Expr -> Bool

Determines whether an expression is tautological.

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

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.

show :: Show a => a -> String

A specialised variant of showsPrec, using precedence context zero, and returning an ordinary String.

showAscii :: Expr -> String

Represents expressions using only ASCII characters (the show function pretty-prints expressions using logical symbols only present in extended character sets).

truthTable :: Expr -> String

The truthTable function produces a truth table for the given expression.

truthTableP :: Printer -> Expr -> String

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.