LKalculus project page

Presentation

LKalculus is a theorem prover for LK theory (classic logic) written in Common LISP. Its algorithm is based on the Oiva Ketonen's rules which are a variant of the Gentzen's sequents method.

The current version release is 0.1, so LKalculus is very basilar now and needs a parser to simplify expressions. It should work for any Common LISP implementation, but it is tested to run on CLISP. It requires ASDF too.

Syntax

The LKalculus sintax is very simple: you can write propositions, variables and constants by a list containing symbols and numbers according to the following rules:

a proposition is a list delimited by brackets and preceded by apostrophe;
the first symbol is the proposition identifier;
the rest is made out of symbols (variables) and numbers (constants).

So if P(x,y,c) is a proposition in which x,y are variables and c is a constant, its translation into LKalculus is '(P x y 1). The sintax is very flexible so that variables like x1, foo, x57 and constants like 2, 3, 671 are admitted. Connectives are used by lists too, they are "non" for "not", "et" for "and", "vel" for "or", "implies" for "implies", "forall" for "for all", "exist" for "there exists". The translations for

$\neg P(x),\qquad P(x)\wedge Q(x),\qquad P(x) \vee Q(x), \\ P(x)\rightarrow Q(x),\qquad \forall x P(x),\quad \exists x P(x)$

are, respectively,

     '(non '(P x))

     '(et '(P x) '(Q x))

     '(vel '(P x) '(Q x))

     '(implies '(P x) '(Q x))

     '(forall x '(P x))

     '(exist x '(P x))

Et and vel admit any number of arguments while non and implies only one and two respectively. The forall and exist operators admit one (bound) variable and one proposition. Finally the proof function gets two list of statements (ipothesis and thesis) and searches for a proof.

Example

We want to demostrate the famous Socrates syllogism: all men are mortals, Socrates is a men, then Socrates is mortal. If we write P(x) for "x is a man", M(x) for "x is mortal" and 1 for Socrates, than the ipotesis-thesis scheme is

$\forall x (P(x)\rightarrow M(x)), \qquad P(1)\qquad \vdash \qquad M(1)$

Now we search for a proof in a Common LISP implementation, for example in CLISP:

bash-3.1$ clisp
[1]> (load "lkalculus.lisp")
;; Loading file lkalculus.lisp ...
;; Loading file asdf.lisp ...
;; Loaded file asdf.lisp
;; Loading file lkalculus.asd ...
;; Loaded file lkalculus.asd
;; Loading file /home/raffaele/programmi/lkalculus-0.1/utility.fas ...
;; Loaded file /home/raffaele/programmi/lkalculus-0.1/utility.fas
;; Loading file /home/raffaele/programmi/lkalculus-0.1/operators.fas ...
;; Loaded file /home/raffaele/programmi/lkalculus-0.1/operators.fas
0 errors, 0 warnings
;; Loaded file lkalculus.lisp
T
[2]> (in-package :operators)
#<PACKAGE OPERATORS>
OPERATORS[3]> (proof '('(forall x '(implies '(P x) '(M x))) '(P 1)) '('(M 1)))
a proof is found!!
NIL

License

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.