Logic and Theorem Proving
Mathematical logic provides the basis of software verification methods. Like a programming language, a logic combines syntax, dictating how to write legal formulas, with semantics, which gives precise meaning to each formula. Mathematical logic formalizes the notion of a proof. In this chapter, we will survey first order and propositional logic. We will then study the essentials of mechanized theorem proving. Theorem proving tools usually do not provide full automation for obtaining proofs. Rather they are used to assist the user by imposing rigor and providing guidance during the proof process. In later chapters, we will show various logics and proof systems that can be used to prove properties of programs in a manual, computer-assisted or fully automatic way.
KeywordsPropositional Logic Theorem Prover Function Symbol Proof System Order Logic
Unable to display preview. Download preview PDF.
The following books can be used for an excellent introduction to mathematical logic
Several books describe a particular deductive theorem prover
- R. S. Boyer, J. S. Moore, The Computational Logic Handbook, Academic Press, 1998.Google Scholar
- T. F. Melham, M. J. C. Gordon, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.Google Scholar
- L. C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge, 1990.Google Scholar
- N. Shankar, Mathematics, Machines and Godel’s Proof, Cambridge, 1997.Google Scholar
- L. Wos, The Automatic Reasoning: An Experimenter’s Notebook with Otter, Tutorial, Academic Press, 1996.Google Scholar
- L. Wos, Automated Reasoning: Introduction and Application, 2nd edition, McGraw-Hill, 1992.Google Scholar