Logic
is an old interest of mine. My first introduction
was Lemmon's Beginning Logic which gave
a natural deduction presentation. Subsequently I
redisovered logic, in the shape of Prolog, when I
moved to computer science. Prolog influenced my
work in high-performance automated reasoning
which in turn led to the grandfather of Shen,
SEQUEL (SEQUEnt processing Language), in 1993.
SEQUEL united two themes; my interest in the
high-level specification of inference rules in
sequent calculus and
the compilation of those rules into efficient
code. SEQUEL was followed by Qi (2005) and Shen
(2011). You can find an exposition of sequent
calculus in chapter 18 of The Book
of Shen.In 2003 I taught
discrete maths at Stony Brook and in 2004, wrote
up my class notes into a text Logic, Proof and
Computation. This went through a
number of revisions and the third edition was
issued in May of 2023. LPC is designed as a
multidisciplinary reader for students in
philosophy and computing who are approaching
logic for the first time. LPC uses
computer-assisted proof in first-order logic and
the code for this was specified using the Logic Lab; a program that
allows the user to enter deduction rules direct
to the machine, which are then compiled into
efficient code.
I'm
also working, on and off, on a hobby project, THORN (Theorem
prover based on HORN clause
logic) which uses Prolog technology, specifically
Shen Prolog, to compile first-order axioms into
efficient code.
|
 Logic, Proof and
Computation (3rd edition)
|