Logic, Proof and Computation



Welcome to the support page for the text Logic, Proof and Computation 3rd edition; henceforth LPC.

What is in the Book?

Beginning with a review of formal languages and their syntax and semantics, LPC conducts a computer assisted course in formal reasoning and the relevance of logic to mathematical proof, information processing and philosophy.

Topics covered include formal grammars, semantics of formal languages, sequent systems, truth-tables, propositional and first order logic, identity, proof heuristics, regimentation, set theory, Tarskiís semantic theory of truth, databases, modal logic, possible world semantics, Herbrandís proof, automated deduction, proof by induction, model theory and Skolemís paradox, Turing machines, undecidability and a computer illustration of the reasoning underpinning GŲdelís incompleteness proof.

Logic proofs for the student are supported by computer-assisted proofs and the programs are freely available from this page. LPC is designed as a multidisciplinary reader for students in computing, philosophy and mathematics.


How to Get the Book?

Currently review copies of LPC are available from the Great British Bookshop. The distribution extends to the UK, the EC countries and the USA. You may be pleasantly surprised to find the GBB can reach you if you are outside those countries; so do enquire if so.

Installing the Programs for Logic, Proof and Computation

For Windows Users

If you are a Windows user then this executable contains all the programs used in LPC.

For Non-Windows Users

If you are not a Windows user then you need to install these programs. You need a working image of Shen. I recommend Shen-Scheme by Bruno Defferari which can be found on the Shen download page.

Look under 'Binaries'. Select the link 'Scheme' in that table. You will be directed to a GitHub page. Bruno has supplied executables for Linux and OS/X as well as Windows. Download the one you need and install it.

Now download the LPC software from here. Unzip the compressed file and place the working image of Shen into the directory LPC. Enter Shen-Scheme (or whatever installation you have chosen) and type (load "loadme.shen") into the top level. You are now set up to run the programs from this book.

As of June 2023, there is no facility to save an image under Shen-Scheme, so you will have to repeat (load "loadme.shen") every time you login to run LPC programs. This may change, so check this page.


LPC was publically available on the 26th May, 2023 and went through a number of changes becoming 'stable' on the 6th June. Here follows a list of errata.

Page Error
57 The proof, which is inherited from the second edition, is valid, but in the new support software the ordering of assumptions has changed. In the second edition, the support program was slightly different. Call this change zero.
58, 61 Ditto change zero.
141 The text (R Philip Tully Catiline) should be (R Philip Cicero Catiline) and vice versa.
141 In a prepublication preprint. You will not find this error in your text. 'if rendered in first-order logic ... Bush' should be cut. A paste error.
228-231 The type 'valid' is replaced by 'step'. This is a naming convention.
266 'then under v' bottom of page, v should be italicised.
293 Second example of unification x -> a should be x -> (g y).
302 Installation routine; this changed somewhat prior to general release.


This is a review version and is subject to change, but post June 3rd 2023 the changes have been very minor. Do post if you have an issue and errors will be corrected and you will be placed in the acknowledgements.


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