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

AutoProof.Internal.Proof.Types

Description

Defines the Proof type.

Synopsis

Documentation

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

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

Get a pretty-printed representation of a proof.