|
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.
Errata
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. |
Feedback
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.
|
LATEST NEWS
The support page for Shen/tk - a type secure platform portable interface to TCL/tk.
______________________________
The support page for the text Programming the Logic Lab now includes readable online access to the book.
______________________________
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. |
