autoproof-0.0.0.0: Propositional logic library
Copyright(c) Artem Mavrin 2021
LicenseBSD3
Maintainerartemvmavrin@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe
LanguageHaskell2010

AutoProof

Description

Propositional logic library.

This top-level module only includes type definitions and functions for the syntactic entities of propositional logic. If you want semantics, then you must first choose either classical or intuitionistic logic, and then use the corresponding module

  1. AutoProof.Classical, for classical logic, or
  2. AutoProof.Intuitionistic, for intuitionistic logic.

Both of the above module expose every symbol in this module, and more.

Synopsis

Formulas

data Formula a where Source #

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\).

Bundled Patterns

pattern Lit :: Bool -> Formula a

Propositional literal/constant. (Lit True) is \(\top\) (i.e., truth, tautology, or top), and (Lit False) is \(\bot\) (i.e., falsity, contradiction, or bottom).

pattern Var :: a -> Formula a

Propositional variable. (Var x) represents a propositional variable \(x\).

pattern Not :: Formula a -> Formula a

Negation. (Not p) represents the formula \(\lnot p\).

pattern Imp :: Formula a -> Formula a -> Formula a

Implication. (Imp p q) represents the formula \(p \rightarrow q\).

pattern Or :: Formula a -> Formula a -> Formula a

Disjunction. (Or p q) represents the formula \(p \lor q\).

pattern And :: Formula a -> Formula a -> Formula a

Conjunction. (And p q) represents the formula \(p \land q\).

pattern Iff :: Formula a -> Formula a -> Formula a

Equivalence. (Iff p q) represents the formula \(p \leftrightarrow q\).

Instances

Instances details
Eq a => Eq (Formula a) Source #

Syntactic equality.

Instance details

Defined in AutoProof.Internal.Formula.Types

Methods

(==) :: Formula a -> Formula a -> Bool #

(/=) :: Formula a -> Formula a -> Bool #

Ord a => Ord (Formula a) Source #

First compare heights, then compare sizes, then resolve using the convention Lit < Var < Not < Imp < Or < And < Iff (on equality, compare children from left to right).

Instance details

Defined in AutoProof.Internal.Formula.Types

Methods

compare :: Formula a -> Formula a -> Ordering #

(<) :: Formula a -> Formula a -> Bool #

(<=) :: Formula a -> Formula a -> Bool #

(>) :: Formula a -> Formula a -> Bool #

(>=) :: Formula a -> Formula a -> Bool #

max :: Formula a -> Formula a -> Formula a #

min :: Formula a -> Formula a -> Formula a #

Read a => Read (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Show a => Show (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Methods

showsPrec :: Int -> Formula a -> ShowS #

show :: Formula a -> String #

showList :: [Formula a] -> ShowS #

AST (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Associated Types

type Root (Formula a) Source #

PrettyPrintable a => PrettyPrintable (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

type Root (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

type Root (Formula a) = Maybe a

Operations on formulas

subformulas :: Ord a => Formula a -> Set (Formula a) Source #

Get the set of subformulas of a propositional formula.

Examples

Expand
>>> 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 :: Eq a => Formula a -> a -> Formula a -> Formula a Source #

(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

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

getAnyVariable :: Formula a -> Maybe a Source #

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

Examples

Expand
>>> getAnyVariable (Or (Var "a") (Var "b"))
Just "a"
>>> getAnyVariable (Lit False :: Formula String)
Nothing

Judgements

type Context a = Set (Formula a) Source #

A set of propositional formulas, used as antecedents of a judgement.

data Judgement a Source #

(Judgement c a) represents the judgement or sequent \(c \vdash a\).

>>> Judgement Set.empty (Imp (And (Var 'a') (Var 'b')) (Var 'a'))
[] |- Imp (And (Var 'a') (Var 'b')) (Var 'a')

Constructors

Judgement 

Fields

Instances

Instances details
Eq a => Eq (Judgement a) Source # 
Instance details

Defined in AutoProof.Internal.Judgement

Methods

(==) :: Judgement a -> Judgement a -> Bool #

(/=) :: Judgement a -> Judgement a -> Bool #

Ord a => Ord (Judgement a) Source # 
Instance details

Defined in AutoProof.Internal.Judgement

(Ord a, Read a) => Read (Judgement a) Source # 
Instance details

Defined in AutoProof.Internal.Judgement

Show a => Show (Judgement a) Source # 
Instance details

Defined in AutoProof.Internal.Judgement

PrettyPrintable a => PrettyPrintable (Judgement a) Source # 
Instance details

Defined in AutoProof.Internal.Judgement

Judgement constructor

(|-) :: (Ord a, Foldable f) => f (Formula a) -> Formula a -> Judgement a infix 5 Source #

Infix judgement constructor. (c |- a) represents the judgement \(c \vdash a\).

>>> [Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b'
[Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'b'

Note: If c is already a Set, then it is recommended to use (Judgement c a) in favor of (c |- a), since the latter will create a new set and fill it with the values in c.

Operations on judgements

weakenJudgement :: Ord a => Judgement a -> Formula a -> Judgement a Source #

Weaken a judgement by inserting a formula into its hypotheses.

>>> weakenJudgement ([Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b') (Var 'c')
[Var 'a',Var 'c',Imp (Var 'a') (Var 'b')] |- Var 'b'

Proofs

data Proof a where Source #

A proof tree for propositional logic.

Bundled Patterns

pattern Axiom :: Judgement a -> Proof a

An axiom (Axiom (g |- a)) represents the inference of the judgement \(g \vdash a\), where \(a \in g\):

\[ \frac{}{ g \vdash a } \, (\text{Axiom}) \]

pattern FalseElim :: Judgement a -> Proof a -> Proof a

Falsity elimination (principle of explosion). (FalseElim (g |- a) p) represents the inference of the judgement \(g \vdash a\) given a proof \(p\) of \(g \vdash \bot\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash \bot } }{ g \vdash a } \, ({\bot}\text{E}) \]

pattern TrueIntr :: Judgement a -> Proof a

Truth introduction. (TrueIntr (g |- Lit True)) represents the vacuous inference of the judgement \(g \vdash \top\):

\[ \frac{}{ g \vdash \top } \, (\top\text{I}) \]

pattern NotElim :: Judgement a -> Proof a -> Proof a -> Proof a

Negation elimination. (NotElim (g |- Lit False) p q) represents the inference of the judgement \(g \vdash \bot\) given a proof \(p\) of \(g_1 \vdash \lnot a\) and a proof \(q\) of \(g_2 \vdash a\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash \lnot a } \qquad \displaystyle\frac{ q }{ g_2 \vdash a } }{ g \vdash \bot } \, ({\lnot}\text{E}) \]

pattern NotIntr :: Judgement a -> Proof a -> Proof a

Negation introduction. (NotIntr (g |- (Not a)) p) represents the inference of the judgement \(g \vdash \lnot a\) given a proof \(p\) of \(g, a \vdash \bot\):

\[ \frac{ \displaystyle\frac{ p }{ g, a \vdash \bot } }{ g \vdash \lnot a } \, ({\lnot}\text{I}) \]

pattern ImpElim :: Judgement a -> Proof a -> Proof a -> Proof a

Implication elimination (modus ponens). (ImpElim (g |- b) p q) represents the inference of the judgement \(g \vdash b\) given a proof \(p\) of \(g_1 \vdash a \rightarrow b\) and a proof \(q\) of \(g_2 \vdash a\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \rightarrow b } \qquad \displaystyle\frac{ q }{ g_2 \vdash a } }{ g \vdash b } \, ({\rightarrow}\text{E}) \]

pattern ImpIntr :: Judgement a -> Proof a -> Proof a

Implication introduction. (ImpIntr (g |- (Imp a b) p) represents the inference of the judgement \(g \vdash a \rightarrow b\) given a proof \(p\) of \(g, a \vdash b\):

\[ \frac{ \displaystyle\frac{ p }{ g, a \vdash b } }{ g \vdash a \rightarrow b } \, ({\rightarrow}\text{I}) \]

pattern OrElim :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a

Disjunction elimination. (OrElim (g |- c) p q r) represents the inference of the judgement \(g \vdash c\) given proofs \(p\) of \(g_1 \vdash a \lor b\), \(q\) of \(g_2, a \vdash c\), and \(r\) of \(g_3, b \vdash c\), where \(g = g_1 \cup g_2 \cup g_3\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \lor b } \qquad \displaystyle\frac{ q }{ g_2, a \vdash c } \qquad \displaystyle\frac{ r }{ g_3, b \vdash c } }{ g \vdash c } \, ({\lor}\text{E}) \]

pattern OrIntrL :: Judgement a -> Proof a -> Proof a

Left disjunction introduction. (OrIntrL (g |- (Or a b)) p) represents the inference of the judgement \(g \vdash a \lor b\) given a proof \(p\) of \(g \vdash a\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a } }{ g \vdash a \lor b } \, ({\lor}\text{IL}) \]

pattern OrIntrR :: Judgement a -> Proof a -> Proof a

Right disjunction introduction. (OrIntrR (g |- (Or a b)) p) represents the inference of the judgement \(g \vdash a \lor b\) given a proof \(p\) of \(g \vdash b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash b } }{ g \vdash a \lor b } \, ({\lor}\text{IR}) \]

pattern AndElimL :: Judgement a -> Proof a -> Proof a

Left conjunction elimination. (AndElimL (g |- a) p) represents the inference of the judgement \(g \vdash a\) given a proof \(p\) of \(g \vdash a \land b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \land b } }{ g \vdash a } \, ({\land}\text{EL}) \]

pattern AndElimR :: Judgement a -> Proof a -> Proof a

Right conjunction elimination. (AndElimR (g |- b) p) represents the inference of the judgement \(g \vdash b\) given a proof \(p\) of \(g \vdash a \land b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \land b } }{ g \vdash b } \, ({\land}\text{ER}) \]

pattern AndIntr :: Judgement a -> Proof a -> Proof a -> Proof a

Conjunction introduction. (AndIntr (g |- (And a b)) p) represents the inference of the judgement \(g \vdash a \land b\) given a proof \(p\) of \(g_1 \vdash a\) and a proof \(q\) of \(g_2 \vdash b\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a } \qquad \displaystyle\frac{ q }{ g_2 \vdash b } }{ g \vdash a \land b } \, ({\land}\text{I}) \]

pattern IffElimL :: Judgement a -> Proof a -> Proof a

Left equivalence elimination. (IffElimL (g |- (Imp a b)) p) represents the inference of the judgement \(g \vdash a \rightarrow b\) given a proof \(p\) of \(g \vdash a \leftrightarrow b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \leftrightarrow b } }{ g \vdash a \rightarrow b } \, ({\leftrightarrow}\text{EL}) \]

pattern IffElimR :: Judgement a -> Proof a -> Proof a

Right equivalence elimination. (IffElimR (g |- (Imp b a)) p) represents the inference of the judgement \(g \vdash b \rightarrow a\) given a proof \(p\) of \(g \vdash a \leftrightarrow b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \leftrightarrow b } }{ g \vdash b \rightarrow a } \, ({\leftrightarrow}\text{ER}) \]

pattern IffIntr :: Judgement a -> Proof a -> Proof a -> Proof a

Equivalence introduction. (IffIntr (g |- (Iff a b)) p) represents the inference of the judgement \(g \vdash a \leftrightarrow b\) given a proof \(p\) of \(g_1 \vdash a \rightarrow b\) and a proof \(q\) of \(g_2 \vdash b \rightarrow a\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \rightarrow b } \qquad \displaystyle\frac{ q }{ g_2 \vdash b \rightarrow a } }{ g \vdash a \leftrightarrow b } \, ({\leftrightarrow}\text{I}) \]

Instances

Instances details
Eq a => Eq (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

Methods

(==) :: Proof a -> Proof a -> Bool #

(/=) :: Proof a -> Proof a -> Bool #

Ord a => Ord (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

Methods

compare :: Proof a -> Proof a -> Ordering #

(<) :: Proof a -> Proof a -> Bool #

(<=) :: Proof a -> Proof a -> Bool #

(>) :: Proof a -> Proof a -> Bool #

(>=) :: Proof a -> Proof a -> Bool #

max :: Proof a -> Proof a -> Proof a #

min :: Proof a -> Proof a -> Proof a #

(Ord a, Read a) => Read (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

Show a => Show (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

Methods

showsPrec :: Int -> Proof a -> ShowS #

show :: Proof a -> String #

showList :: [Proof a] -> ShowS #

AST (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

Associated Types

type Root (Proof a) Source #

PrettyPrintable a => PrettyPrintable (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

type Root (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

type Root (Proof a) = Judgement a

Abstract syntax trees

class AST t where Source #

Abstract syntax tree class.

Minimal complete definition

root, children, metadata

Associated Types

type Root t Source #

The type of the values annotating AST nodes.

Methods

root :: t -> Root t Source #

The value at the AST's root node.

children :: t -> [t] Source #

The AST's child ASTs.

height :: t -> Int Source #

Number of edges on the longest path from the root of the AST to a leaf.

size :: t -> Int Source #

Number of nodes in the AST.

Instances

Instances details
AST (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Associated Types

type Root (Formula a) Source #

AST (Proof a) Source # 
Instance details

Defined in AutoProof.Internal.Proof.Types

Associated Types

type Root (Proof a) Source #

subtrees :: (AST t, Ord t) => t -> Set t Source #

(subtrees t) is the set of all subtrees of an AST t (including t itself).

properSubtrees :: (AST t, Ord t) => t -> Set t Source #

(properSubtrees t) is the the set of all proper subtrees of an AST t (i.e., not including t itself).

Parsing

parseFormula :: String -> Maybe (Formula String) Source #

(parseFormula s) parses a string s as a propositional formula, returning a Just a on success, where a is the parsed formula.

For a version of parseFormula that does not return a wrapped formula but also throws an error when it cannot parse, see unsafeParseFormula.

Conventions

Expand
  • Supported connective symbols:

    • Negation: "~", "¬".
    • Implication: "->", "=>", "→", "⇾", "⇒" "⊃".
    • Disjunction: "|", "\/", "∨", "+"
    • Conjunction: "&", "/\", "∧", "^", "*"
    • Equivalence: "<->", "↔", "⇿", "⇔"
  • Implication is right-associative and has lower precedence than the other connectives.
  • Equivalence is left-associative and has higher precedence than implication but lower precedence than conjunction and disjunction.
  • Disjunction is left-associative and has higher precedence than equivalence but lower precedence than conjunction.
  • Conjunction is left-associative and has highest precedence out of the binary connectives.
  • Negation binds most tightly, and must immediately precede its argument (i.e., there should not be a space between a negation symbol and the proposition that follows).
  • Valid variable names begin with a letter (uppercase or lowercase) or an underscore, and may be followed by a letter, underscore, digit, or single quote (a "prime" symbol). The exceptions are the strings "false" and "true", which are parsed as the propositional literals \(\bot\) and \(\top\), respectively.

Examples

Expand
>>> parseFormula "a -> b -> c"
Just (Imp (Var "a") (Imp (Var "b") (Var "c")))
>>> parseFormula "~a | b -> c"
Just (Imp (Or (Not (Var "a")) (Var "b")) (Var "c"))
>>> parseFormula "(a -> b) & ~c"
Just (And (Imp (Var "a") (Var "b")) (Not (Var "c")))

parseJudgement :: String -> Maybe (Judgement String) Source #

(parseJudgement s) parses a string s as a propositional judgement.

A valid judgement is made up of an antecedent, a turnstile symbol, and a consequent (in that order). The antecedents are a (potentially empty) comma-separated list of formulas, the turnstile symbol is either "|-" or "⊢", and the consequent is another formula.

See parseFormula for the specification of valid formulas.

Examples

Expand
>>> parseJudgement "a, a -> b |- b"
Just ([Var "a",Imp (Var "a") (Var "b")] |- Var "b")
>>> parseJudgement "a |- a | b"
Just ([Var "a"] |- Or (Var "a") (Var "b"))

Pretty-printing

pretty :: PrettyPrintable a => a -> String Source #

Pretty-print a value.

prettyFormula :: PrettyPrintable a => Formula a -> String Source #

Get a pretty-printed representation of a propositional formula.

Examples

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

prettyJudgement :: PrettyPrintable a => Judgement a -> String Source #

Get a pretty-printed representation of a judgement.

Examples

Expand
>>> prettyJudgement $ [Var "a", Imp (Var "a") (Var "b")] |- Var "b"
"a, a → b ⊢ b"

prettyProof :: PrettyPrintable a => Proof a -> String Source #

Get a pretty-printed representation of a proof.