Logic and Theorem Proving

  • Doron A. Peled
Part of the Texts in Computer Science book series (TCS)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Further Reading

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

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

Several books describe a particular deductive theorem prover

  1. R. S. Boyer, J. S. Moore, The Computational Logic Handbook, Academic Press, 1998.Google Scholar
  2. T. F. Melham, M. J. C. Gordon, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.Google Scholar
  3. L. C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge, 1990.Google Scholar
  4. N. Shankar, Mathematics, Machines and Godel’s Proof, Cambridge, 1997.Google Scholar
  5. L. Wos, The Automatic Reasoning: An Experimenter’s Notebook with Otter, Tutorial, Academic Press, 1996.Google Scholar
  6. L. Wos, Automated Reasoning: Introduction and Application, 2nd edition, McGraw-Hill, 1992.Google Scholar

Copyright information

© Lucent Technologies 2001

Authors and Affiliations

  • Doron A. Peled
    • 1
  1. 1.Computing SciencesBell Labs/Lucent TechnologiesMurray HillUSA

Personalised recommendations