Truth, Deduction, and Computation: Logic and Semantics for Computer Science (Principles of Computer Science Series)

By R.E. Davis

Truth, Deduction, and Computation Logic and Semantics for Computer Science. Ruth E. Davis. Copyright 1989, Computer Science Press, NY. ISBN/ASIN/LOC 0716782014. Hardcover in very good condition.... This description may be from another edition of this product.

• Format: Hardcover
• Language: English
• ISBN: 0716782014
• ISBN13: 9780716782018
• Release Date: January 1989
• Publisher: Computer Science Pr
• Length: 224 Pages
• Weight: 1.60 lbs.
• Dimensions: 10.0" x 0.8" x 7.0"

Customer Reviews

Good introduction

Having used this book to teach courses in elementary model theory, I can attest to its utility. It serves this purpose well, and the book is short enough to allow covering most of the material in the span of a semester. After finishing it, readers will be well prepared to tackle more advanced books in mathematical logic and model theory, or move into areas of artificial intelligence or logic programming. The most popular languages in artificial intelligence, namely LISP and PROLOG are based on the concepts in this book. Some of the areas that are not treated but can be accessed after reading the book include nonmonotonic logics, inductive logic programming, formal learning theory, higher-order languages, automated deduction, and the theory of object-oriented languages. The author discusses four languages in the book, namely propositional logic, predicate calculus, elementary number theory, and lambda calculus. The author's strategy in discussing each of these languages is to first discuss the syntax, and then move on to treat the truth, deduction, and computational aspects of them. As expected, propositional logic is the "cleanest" of the four languages, for its model theory is constructed via the use of truth tables. The computation, ground resolution is used, which gives a decision procedure for the language. The author shows that truth tables can be generated effectivey for a given well-formed formula, and thus the truth of the language is established. Completeness then implies the language is provable. Thus for propositional logic, the notions of truth, deduction, and computation are equivalent. For predicate calculus the situation is more complicated, requiring the use of general resolution. The author's treatment is very contemporary, in that it makes use of Horn clauses to implement the computation scheme. She again shows that truth, deduction, and computation are equivalent for predicate calculus, but that one cannot decide if a computation will yield a result. Given a sentence in the language, if it is provable, then the computation will terminate. Conversely, if the computation terminates successfully, then the sentence is provable. One cannot however put an upper bound on the computation, and so there is no gaurantee a priori that the program will terminate. The author tightens this situation even further by showing that the predicate calculus is undecidable. In the language of elementary number theory, the author clarifies the notion of an algorithm, and shows that this language is undecidable. She also overviews the famous Godel incompleteness theorems, which show the existence of a sentence that is true under the standard interpretation but which is not provable. Thus elementary number theory is not complete. In the language of lambda calculus, the author shows, interestingly, that expressions involving normal forms are not semantically distinguishable from expressions without normal forms. This forces a red