Description

The Logic Lab is a high-level tool for the specification of arbitrary logics in sequent calculus notation. With the aid of the Logic Lab, it is possible for the programmer to implement type secure working derivation systems in minutes and conduct computer-assisted proofs. Starting from assumed foundations, this text shows how to fabricate a working version of propositional calculus and then first-order logic. The book then subsequently goes on to examine more advanced systems, including modal logic, tableau and Martin-Löf type theory. ‘Programming the Logic Lab’ is a companion to the author’s earlier introductory work ‘Logic, Proof and Computation’ which used computer-based proof.