LkProver

An automated LK deduction. The resulting proof is emitted as a Latex snippet that uses bussproofs.

Example

dune exec bin/main.exe '|- ((p -> q) -> p) -> p'

\begin{prooftree}
\AxiomC{}
\RightLabel{(axiom)}
\UnaryInfC{$p \vdash p, q$}
\RightLabel{($\rightarrow R$)}
\UnaryInfC{$\vdash p, p \rightarrow q$}
\AxiomC{}
\RightLabel{(axiom)}
\UnaryInfC{$p \vdash p$}
\RightLabel{($\rightarrow L$)}
\BinaryInfC{$(p \rightarrow q) \rightarrow p \vdash p$}
\RightLabel{($\rightarrow R$)}
\UnaryInfC{$\vdash ((p \rightarrow q) \rightarrow p) \rightarrow p$}
\end{prooftree}

Available Symbols

• variables : [A-Za-z][A-Za-z0-9_]*
• bottom: ⊥, _|_
• not : ¬, ~, !
• and : ∧, /\, ^, &
• or : ∨, \/, |
• implication : →, ->
• proves : ⇒, =>, ⊢, |-
• parentheses : (, )