Programming the Logic Lab



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.

  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").

For the Reader

Introduction: the Development of the Logic Lab

A New Implementation
Installing the Logic Lab

Chapter 1 Specifying Logics

The Structure of a Logic
The Syntax of Propositional Calculus
Derivation Rules
Representation in the Logic Lab
Derivation Rules with Parameters
Non Deterministic Rules

Chapter 2 The General Proof Assistant

Valid Inference Rules and Proofs
Saving and Rolling Back Proofs
Saving Theorems

Chapter 3 First Order LPC

Derivation Rules
Derivation Rules in the Logic Lab
A First Order Proof

Chapter 4 Semantic Tableau

The Rules for Semantic Tableau
Decision Procedures
Automating Tableau for First Order Logic
Eliminating the Universal Quantifiers
Rigid and Flexible Variables
Putting It Together
Optimising Automated Tableau
LPC and Tableau

Chapter 5 TT0: Propositions as Types

Propositions as Types
Types and Lambda Functions
Heyting on Propositional Logic
The Curry-Howard Correspondence
Propositional TT0
A Proof in Propositional TT0
Implementation in the Logic Lab
Heytings Semantics for Quantifiers
Logic Lab Rules for Quantificational TT0
Induction and Primitive Recursion
Primitive Recursion in Shen
Mathematical Induction in TT0
Specification and Program Synthesis
Synthesis of the Addition Function
Conversion to a Shen Program


A Note on Modal Logic
Select Bibliography

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