Proof and Disproof in Formal Logic: An Introduction for programmers by Richard BornatProof and Disproof in Formal Logic: An Introduction for programmers by Richard Bornat

Proof and Disproof in Formal Logic: An Introduction for programmers

byRichard Bornat

Paperback | July 21, 2005

Pricing and Purchase Info

$109.50 online 
$126.00 list price save 13%
Earn 548 plum® points

Prices and offers may vary in store


Ships within 1-3 weeks

Ships free on orders over $25

Not available in stores


iProof and Disproof in Formal Logic/i is a lively and entertaining introduction to formal logic providing an excellent insight into how a simple logic works. Formal logic allows you to check a logical claim without considering what the claim means. This highly abstracted idea is an essentialand practical part of computer science. The idea of a formal system--a collection of rules and axioms which define a universe of logical proofs--is what gives us programming languages and modern-day programming.This book concentrates on using logic as a tool: making and using formal proofs and disproofs of particular logical claims. The logic it uses--natural deduction--is very small and very simple; working with it helps you see how large mathematical universes can be built on small foundations.The book is divided into four parts:DT Part I "Basics" gives an introduction to formal logic with a short history of logic and explanations of some technical words.DT Part II "Formal syntactic proof" show you how to do calculations in a formal system where you are guided by shapes and never need to think about meaning. Your experiments are aided by Jape, which can operate as both inquisitor and oracle.DT Part III "Formal semantic disproof" shows you how to construct mathematical counterexamples to show that proof is impossible. Jape can check the counterexamples you build.DT Part IV "Program specification and proof" describes how to apply your logical understanding to a real computer science problem, the accurate description and verification of programs. Jape helps, as far as arithmetic allows.Aimed at undergraduates and graduates in computer science, logic, mathematics, and philosophy, the text includes reference to and exercises based on the computer software package Jape, an interactive teaching and research tool designed and hosted by the author that is freely available on theweb.
Richard Bornat is at School of Computing Science, Middlesex University.
Title:Proof and Disproof in Formal Logic: An Introduction for programmersFormat:PaperbackDimensions:264 pages, 9.45 × 6.61 × 0.65 inPublished:July 21, 2005Publisher:Oxford University PressLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:0198530277

ISBN - 13:9780198530275


Table of Contents

PrefacePART I BASICS1. A Rough History of Logic2. How to speak and read logicPART II FORMAL PROOF3. Connectives4. Rule shapes and formula shapes5. Proof with connectives6. The logical quantifiers7. Proofs with quantifiersPART III DISPROOF8. Disproof in a mathematical model9. Constructive semantics10. Classical semantics11. Disproof calculationPART IV PROOF OF PROGRAMS12. Specification and Verification13. A simple programming language14. Loops15. ArraysIndex