LkProver

LkProver calculates the derivation tree from an LK sequent and converts it into a corresponding LaTeX snippet.

GitHub - wasabi315/LkProver

Contribute to wasabi315/LkProver development by creating an account on GitHub.

github.com

Contents

• Usage
• Input format
• Output format
• Inference Rules
• Implementation highlights

Usage

Dune is required to run this tool.

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

The above command will output the following LaTeX snippet:

\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}

Input format

Here is the input syntax of LkProver. The precedence of connectives follows the usual one.

<sequent> ::= <expr> "⊢" <expr>
            | <expr> "|-" <expr>
            | <expr> "⇒" <expr>
            | <expr> "=>" <expr>
<expr>    ::= <var>
            | "⊥" | "_|_"
            | "¬" <expr> | "~" <expr> | "!" <expr>
            | <expr> "∧" <expr> | <expr> "/\" <expr> | <expr> "^" <expr> | <expr> "&" <expr>
            | <expr> "∨" <expr> | <expr> "\/" <expr> | <expr> "|" <expr>
            | <expr> "→" <expr> | <expr> "->" <expr>
            | "(" <expr> ")"
<var>     ::= [A-Za-z][A-Za-z0-9_]*

Output format

Currently, the output LaTeX snippet assumes that bussproofs package is used. I will consider supporting other packages including proof.sty in the future.

Inference Rules

LkProver adopts the following inference rules (what I learned in a logic lecture):

Implementation highlights

LkProver is implemented in OCaml. The implementation is very straightforward, just following the inference rules above.

I used Menhir and sedlex for parsing and lexing input sequents. My experience with sedlex was great because lexer specifications are embedded in regular OCaml source codes, so we can still get the help of OCaml Language Server, unlike Menhir which is written in separate .mly files.

If you are interested, please check out the repository.