Formulas of propositional logic are built inductively from atomic propositions

• truth \(\top\),
• falsity \(\bot\), and
• propositional variables \(a, b, c, \ldots\)

using the unary connective

• negation \(\lnot\)

and the binary connectives

• implication \(\rightarrow\),
• disjunction \(\lor\),
• conjunction \(\land\), and
• equivalence \(\leftrightarrow\).

Get a pretty-printed representation of a propositional formula.

Examples

>>> prettyFormula $ Imp (Var "a") (Or (Var "b") (Lit False))
"a → (b ∨ ⊥)"

Get the set of subformulas of a propositional formula.

Examples

>>> subformulas $ Or (Var 'x') (And (Var 'y') (Var 'z'))
fromList [Var 'x',Var 'y',Var 'z',And (Var 'y') (Var 'z'),Or (Var 'x') (And (Var 'y') (Var 'z'))]

(substitute a x p) represents \(a[p/x]\), the substitution of each occurence of the variable \(x\) in the formula \(a\) by the formula \(p\).

Examples

>>> substitute (Imp (Var 'e') (Var 'e')) 'e' (And (Var 'a') (Var 'a'))
Imp (And (Var 'a') (Var 'a')) (And (Var 'a') (Var 'a'))

Obtain a propositional variable from a formula, if there is one.

Examples

>>> getAnyVariable (Or (Var "a") (Var "b"))
Just "a"

>>> getAnyVariable (Lit False :: Formula String)
Nothing