An automated LK deduction. The resulting proof is emitted as a Latex snippet that uses bussproofs.
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}
- variables :
[A-Za-z][A-Za-z0-9_]* - bottom:
⊥,_|_ - not :
¬,~,! - and :
∧,/\,^,& - or :
∨,\/,| - implication :
→,-> - proves :
⇒,=>,⊢,|- - parentheses :
(,)