Software Reliability Methods pp 29-62 | Cite as

# Logic and Theorem Proving

## Abstract

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.

## Keywords

Propositional Logic Theorem Prover Function Symbol Proof System Order Logic## Preview

Unable to display preview. Download preview PDF.

## Further Reading

## The following books can be used for an excellent introduction to mathematical logic

- G. S. Boolos, D. J. Richard,
*Computability and Logic*, Cambridge University Press, (3rd edition), 1989.Google Scholar - D. van Dalen,
*Logic and Structure*,Springer-Verlag, 3rd edition, 1994.Google Scholar - H. D. Ebbinghaus, J. Flum, W. Thomas,
*Mathematical Logic*, Springer-Verlag, 1994.Google Scholar

## 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 - 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