|
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
You can download the Logic Lab and the programs in the book from
here.
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").
|
