|
Welcome to the support page for the text 'Programming the Logic Lab' (PLL). You can buy the text from
here or read it online
using the side bar.
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.
- First order logic as presented in chapter 3. Contained in the folder FOL.
- Semantic tableau as presented in chapter 4. Contained in the folder Tableau.
- 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").
|
