Proof and Disproof in Formal Logic. An Introduction for Programmers
One of the intentions of this book is to present formal logic as a useful tool for computer science. It is done at a basic level; a small and simple component of mathematical logic is presented but an elementary and useful application is then developed. The material was lectured in a first-year university class. Part I ‘Basics’ is an introduction to the idea of formal (mathematical) logic. Part II presents the notion of formal (syntactic) proof. Part III treats formal (semantic) disproof (i.e. how to construct counter-examples), including explanations of notions such as mathematical modeling and constructive and classical semantics. Part IV ‘Proof of programs’ gives some applications to precise description and verification of programs; a simple programming language is introduced for logically based study of loops and arrays. The text is written in a reasonably informal but sufficiently precise manner and, moreover, it is very lively.