LkProver

LkProverはLKシーケントから導出木を計算し，対応するLaTeXスニペットに変換します．

GitHub - wasabi315/LkProver

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

github.com

目次

• 使い方
• 入力形式
• 出力形式
• 推論規則
• 実装のハイライト

使い方

Duneが必要です.

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

上のコマンドは以下のLaTeXスニペットを出力します．

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

入力形式

LkProverの入力となるシーケントの文法です．

<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_]*

出力形式

現在はbusproofsパッケージを使ったコードを出力します． proof.styなど他のパッケージへの対応も検討しています．

推論規則

LkProverは僕が論理学の講義で習った以下の推論規則を採用しています．

実装のハイライト

LkProverはOCamlで実装されています．実装は，上記の推論規則をなぞっていくだけで，非常に素直です．

レキサーとパーサーにはそれぞれsedlexとMenhirを使っています． sedlexは初めて使ったのですが，体験がとても良かったです．Menhirと違って，sedlexはOCamlファイルの中に直接字句解析を書くスタイルのライブラリなので，OCaml Language Serverが効きます．