Programming the Logic Lab



Welcome to the support page for the text 'Programming the Logic Lab' (PLL). You can buy the text from here.

The Logic Lab

The Logic Lab is a collection of tools which allow for rapid prototyping and development of computer-based proof in arbitrary logics. It comprises a proof assistant and a tool for the type secure specification of derivation rules written in single conclusion sequent calculus.

The Logic Lab is covered in three talks on the Shen Education Channel. The first talk deals with the history of the Logic Lab. The second talk deals how to specify logics in the Logic Lab and the third and final talk deals with how to to conduct proofs in the logics so described.

Running the Programs in PLL

First you have to download the Logic Lab and the programs in the book from here. Note you need the Shen Standard Library to run the Logic Lab. There is a binary for Shen under Windows with the Standard Library installed which you can get here.

Unzip the download; the toplevel contains two files, compiler.shen and gpa.shen. Start your Shen image and load compiler.shen with type checking disabled. Now enable type checking and load gpa.shen. Yuo have loaded the Logic Lab itself.

There are three logical systems studied in PLL.

  1. First order logic as presented in chapter 3. Contained in the folder FOL.
  2. Semantic tableau as presented in chapter 4. Contained in the folder Tableau.
  3. Constructive type theory as presented in chapter 5. Contained in the folder TT0.

To load any of these systems, cd to the folder and type (load "loadme.shen").


The support page for the text Logic, Proof and Computation is established.


THORN Theorem prover derived from HORN clause logic is available.


Shen Education Channel starts on Youtube.


Yggdrasil project launched - the grand unification of programming languages.


Want to advertise on this site? Go to the contacts page.

Built by Shen Technology (c) Mark Tarver, September 2021