LK is a sequent calculus, used in order to automate proofs. Given a logic formula (so far only prepositional formulas are implemented), the system should be able to deduce whether or not the formula is valid. It relies on the idea that if there is no way to falsify the formula, then it must always hold true, meaning it’s valid.
The project is a means to learn more about proof systems, Haskell and in particular it’s type system.
The program has a useful feature, namely that it outputs a derivation tree in LaTeX markup for a given sequent.
Compile the program:
[larstvei LK/] λ ghc LK.hs
The program reads two lines of input, where each line may contain space separated WFFs.
Definition WFF (well formed formula):
- p, q, r, s, t ∈ WFF
- if w ∈ WFF then Nw ∈ WFF
- if w, x ∈ WFF then Owx, Awx, Iwx ∈ WFF
Example run:
[larstvei LK/] λ ./LK Enter Γ: Opq Np Enter Δ: q
Output:
\begin{prooftree}
\AxiomC{$Q \stackrel{\times}{\vdash} P, Q$}
\AxiomC{$P \stackrel{\times}{\vdash} P, Q$}
\RightLabel{\scriptsize{L$\lor$}}
\BinaryInfC{$(P \lor Q) \vdash P, Q$}
\RightLabel{\scriptsize{L$\neg$}}
\UnaryInfC{$(P \lor Q), \neg P \vdash Q$}
\end{prooftree}
The rendered output looks like this:
The code may look clunky, but when used with the wonderful
prettify-symbols-mode in Emacs it looks a lot better. The
prettify-symbols-alist have been configured in the following way:
(setq-default prettify-symbols-alist '(("lambda" . ?λ)
("delta" . ?Δ)
("gamma" . ?Γ)
("phi" . ?φ)
("psi" . ?ψ)))