Logic and Proof in Computer Science: Categories and Limits of Proof Techniques

Logic and Proof in Computer Science: Categories and Limits of Proof Techniques

John W. Coffey
Copyright: © 2018 |Pages: 23
DOI: 10.4018/978-1-5225-2443-4.ch007
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

Computer software pervades our lives today. Nevertheless, software is one of the few products for which producers generally provide no express or implied warranties, a truly striking fact since peoples' lives depend in such fundamental ways on these products. This article addresses why such an unintuitive (and undesirable) situation might exist. It will catalog a range of computer science proof techniques and their historical antecedents, the purposes they serve, and several foundational concerns that elude proof techniques of any kind. Along the way, the concept of intractability and its role in computing will be explored as it pertains to algorithmic complexity and to proofs of the meanings of computer programs.
Chapter Preview
Top

Background: The Evolution Of Proof Techniques Used In Computer Science

Many resources pertaining to proof techniques in computer science are available. Numerous scholarly articles describe seminal (but now well-understood and accepted) work in defining foundational knowledge in the field. Other scholarly articles have been published pertaining to aspects of open or unresolved issues while trying to get traction on aspects of the problems which might lead to a final resolution. Additionally, many educational resources are available online and in hardcopy that describe the importance of proof techniques in the field and their applications. This literature review will contain a summary of some of these major results and resources.

Proof techniques in computer science run the gamut from highly mathematical and formal, to quite informal but still persuasive. Lehman, Leighton and Meyer (2016) state that proofs entail various methods of establishing truth, and that these methods take different forms in different fields. They cite different forms that search for the truth might entail including legal truth (that determined by a judge or jury) authoritative truth (established by an expert), probability truth (established by statistics) and philosophical truth, generally in the form of deductive reasoning, established by “careful exposition and persuasion.” They go on to provide a good overview of techniques employed in computer science.

Complete Chapter List

Search this Book:
Reset