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.
‘Contrariwise,’ continued Tweedledee, ‘if it was so, it might be; and if it were so, it would be; but as it isn’t, it ain’t. That’s logic.’
Lewis Carroll, Through the Looking Glass
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
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.
D. van Dalen, Logic and Structure,Springer-Verlag, 3rd edition, 1994.
H. D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic, Springer-Verlag, 1994.
Several books describe a particular deductive theorem prover
R. S. Boyer, J. S. Moore, The Computational Logic Handbook, Academic Press, 1998.
T. F. Melham, M. J. C. Gordon, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.
L. C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge, 1990.
N. Shankar, Mathematics, Machines and Godel’s Proof, Cambridge, 1997.
L. Wos, The Automatic Reasoning: An Experimenter’s Notebook with Otter, Tutorial, Academic Press, 1996.
L. Wos, Automated Reasoning: Introduction and Application, 2nd edition, McGraw-Hill, 1992.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2001 Lucent Technologies
About this chapter
Cite this chapter
Peled, D.A. (2001). Logic and Theorem Proving. In: Software Reliability Methods. Texts in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4757-3540-6_3
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3540-6_3
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4419-2876-4
Online ISBN: 978-1-4757-3540-6
eBook Packages: Springer Book Archive