Logic for Computer Science: Foundations of Automatic Theorem Proving, Second Edition
528
Logic for Computer Science: Foundations of Automatic Theorem Proving, Second Edition
528eBook
Available on Compatible NOOK devices, the free NOOK App and in My Digital Library.
Related collections and offers
Overview
Topics include propositional logic and its resolution, first-order logic, Gentzen's cut elimination theorem and applications, and Gentzen's sharpened Hauptsatz and Herbrand's theorem. Additional subjects include resolution in first-order logic; SLD-resolution, logic programming, and the foundations of PROLOG; and many-sorted first-order logic. Numerous problems appear throughout the book, and two Appendixes provide practical background information.
Product Details
| ISBN-13: | 9780486805085 |
|---|---|
| Publisher: | Dover Publications |
| Publication date: | 04/20/2015 |
| Series: | Dover Books on Computer Science |
| Sold by: | Barnes & Noble |
| Format: | eBook |
| Pages: | 528 |
| File size: | 68 MB |
| Note: | This product may take a few minutes to download. |
Read an Excerpt
Logic for Computer Science
Foundations of Automatic Theorem Proving
By Jean H. Gallier
Dover Publications, Inc.
Copyright © 2015 Jean H. GallierAll rights reserved.
ISBN: 978-0-486-80508-5
CHAPTER 1
Introduction
Logic is concerned mainly with two concepts: truth and provability. These concepts have been investigated extensively for centuries, by philosophers, linguists, and mathematicians. The purpose of this book is by no means to give a general account of such studies. Instead, the purpose of this book is to focus on a mathematically well defined logical system known as first-order logic (and, to some extent, many-sorted logic), and prove some basic properties of this system. In particular, we will focus on algorithmic methods for proving theorems (often referred to as automatic theorem proving).
Every logical system consists of a language used to write statements also called propositions or formulae. Normally, when one writes a formula, one has some intended interpretation of this formula in mind. For example, a formula may assert a true property about the natural numbers, or some property that must be true in a data base. This implies that a formula has a well-defined meaning or semantics. But how do we define this meaning precisely? In logic, we usually define the meaning of a formula as its truth value. A formula can be either true (or valid) or false.
Defining rigorously the notion of truth is actually not as obvious as it appears. We shall present a concept of truth due to Tarski. Roughly speaking, a formula is true if it is satisfied in all possible interpretations. So far, we have used the intuitive meaning of such words as truth, interpretation, etc. One of the objectives of this book is to define these terms rigorously, for the language of first-order logic (and many-sorted first-order logic). The branch of logic in which abstract structures and the properties true in these structures are studied is known as model theory.
Once the concept of truth has been defined rigorously, the next question is to investigate whether it is possible to find methods for deciding in a finite number of steps whether a formula is true (or valid). This is a very difficult task. In fact, by a theorem due to Church, there is no such general method for first-order logic.
However, there is another familiar method for testing whether a formula is true: to give a proof of this formula.
Of course, to be of any value, a proof system should be sound, which means that every provable formula is true.
We will also define rigorously the notion of proof, and proof system for first-order logic (and many-sorted first-order logic). The branch of logic concerned with the study of proof is known as proof theory.
Now, if we have a sound proof system, we know that every provable formula is true. Is the proof system strong enough that it is also possible to prove every true formula (of first-order logic)?
A major theorem of Gödel shows that there are logical proof systems in which every true formula is provable. This is referred to as the completeness of the proof system.
To summarize the situation, if one is interested in algorithmic methods for testing whether a formula of first-order logic is valid, there are two logical results of central importance: one positive (Gödel's completeness theorem), the other one negative (Church's undecidability of validity). Roughly speaking, Gödel's completeness theorem asserts that there are logical calculi in which every true formula is provable, and Church's theorem asserts that there is no decision procedure (procedure which always terminates) for deciding whether a formula is true (valid). Hence, any algorithmic procedure for testing whether a formula is true (or equivalently, by Gödel's completeness theorem, provable in a complete system) must run forever when given certain non-true formulae as input.
This book focuses on Gödel's positive result and its applications to automatic theorem proving. We have attempted to present a coherent approach to automatic theorem proving, following a main thread: Gentzen-like sequent calculi. The restriction to the positive result was dictated mostly by the lack of space. Indeed, it should be stressed that Church's negative result is also important, as well as other fundamental negative results due to Gödel. However, the omission of such topics should not be a severe inconvenience to the reader, since there are many texts covering such material (see the notes at the end of Chapter 5).
In spite of the theoretical limitation imposed by Church's result, the goal of automatic theorem proving (for short, atp) is to find efficient algorithmic methods for finding proofs of those formulae that are true.
A fairly intuitive method for finding such algorithms is the completeness proof for Gentzen-like sequent calculi. This approach yields a complete procedure (the search procedure) for proving valid formulae of first-order logic. However, the search procedure usually requires an enormous amount of space and time and it is not practical. Hence, we will try improve it or find more efficient proof procedures.
For this, we will analyze the structure of proofs carefully. Fundamental results of Gentzen and Herbrand show that if a formula is provable, then it has a proof having a certain form, called a normal form.
The existence of such normal forms can be exploited to reduce the size of the search space that needs to be explored in trying to find a proof. Indeed, it is sufficient to look for proofs in normal form.
The existence of normal forms is also fundamental because it reduces the problem of finding a proof of a first-order formula to the problem of finding a proof of a simpler type of formula, called a proposition. Propositions are much simpler than first-order formulae. Indeed, there are algorithms for deciding truth. One of the methods based on this reduction technique is the resolution method, which will be investigated in Chapters 4 and 8.
Besides looking for general methods applying to the class of all true (first-order) formulae, it is interesting to consider subclasses for which simpler or more efficient proof procedures exist. Indeed, for certain subclasses there may be decision procedures. This is the case for propositions, and for quantifier-free formulae. Such cases are investigated in Chapters 3 and 10 respectively.
Unfortunately, even in cases in which algorithms exist, another difficulty emerges. A decision procedure may take too much time and space to be practical. For example, even testing whether a proposition is true may be very costly. This will be discussed in Chapter 3.
Automatic theorem proving techniques can be used by computer scientists to axiomatize structures and prove properties of programs working on these structures. Another recent and important role that logic plays in computer science, is its use as a programming language and as a model of computation. For example, in the programming language PROLOG, programs are specified by sets of assertions. In such a programming language, a computation is in fact a proof, and the output of a program is extracted from the proof. Promoters of such languages claim that since such programs are essentially logical formulae, establishing their correctness is trivial. This is not quite so, because the concept of correctness is relative, and the semantics of a PROLOG program needs to be expressed in a language other than PROLOG. However, using logic as a vehicle for programming is a very interesting idea and should be a selling point for skeptics. This use of logic will be investigated in Chapter 9.
CHAPTER 2Mathematical Preliminaries
This chapter is devoted to mathematical preliminaries. This fairly lengthy chapter has been included in order to make this book as self-contained as possible. Readers with a firm mathematical background may skim or even skip this chapter entirely. Classroom experience shows that any one who is not acquainted with the material included in Section 2.3 should probably spend some time reading Sections 2.1 to 2.3. In any case, this chapter can be used as a library of useful facts and may be consulted whenever necessary.
Since trees, inductive definitions and the definition of functions by recursion play an important role in logic, they will be defined carefully. First, we review some basic concepts and establish the terminology and notation used in this book. It is assumed that the reader is familiar with the basic properties of sets. For more details, the reader may consult Enderton, 1972; Enderton, 1977; Lewis and Papadimitriou, 1981; or Suppes, 1972.
2.1 Relations, Functions, Partial Orders, Induction
First, we review the concepts of Cartesian product, tuple and relation.
2.1.1 Relations
Given two sets A and B (possibly empty), their Cartesian product denoted by A × B is the set of ordered pairs
{<a, b> | a [member of] A, b [member of] B}.
Given any finite number of sets A1, ..., An, the Cartesian product A1 × ... × An is the set of ordered n-tuples
{a1, ..., an > | ai [member of] Ai, 1 ≤ i [less than or equal to] n}
(An ordered n-tuple <a1, ..., an> is also denoted by (a1, ..., an).)
A binary relation between A and B is any subset R (possibly empty) of A × B.
Given a relation R between A and B, the set
{x [member of] A | [there exists]y [member of] B
is called the domain of R and denoted by dom(R). The set
{y [member of] B | [there exists]x [member of] A
is called the range of R and is denoted by range(R).
When A = B, a relation R between A and A is also called a relation on (or over) A. We will also use the notation xRy as an alternate to (x, y) [member of] R.
2.1.2 Partial Functions, Total Functions
A relation R between two sets A and B is functional iff, for all x [member of] A, and y, z [member of] B, (x, y) [member of] R and (x, z) [member of] R implies that y = z.
A partial function is a triple f = <A, G, B>, where A and B are arbitrary sets (possibly empty) and G is a functional relation (possibly empty) between A and B, called the graph of f.
Hence, a partial function is a functional relation such that every argument has at most one image under f. The graph of a function f is denoted as graph(f). When no confusion can arise, a function f and its graph are usually identified.
A partial function f = <A, G, B> is often denoted as f: A [right arrow] B. For every element x in the domain of a partial function f, the unique element y in the range of f such that (x, y) [member of] graph(f) is denoted by f(x). A partial function f: A [right arrow] B is a total function iff dom(f) = A. It is customary to call a total function simply a function.
2.1.3 Composition of Relations and Functions
Given two binary relations R between A and B, and S between B and C, their composition denoted by R [??] S is a relation between A and C defined by the following set of ordered pairs:
{(a, c) | [there exists]b [member of] B, (a, b) [member of] R and (b, c) [member of] S}.
Given a set A, the identity relation of A is denoted by IA and is the relation {(x, x) | x [member of] A}. Note that IA is also a total function.
Given a relation R between A and B, its converse is the relation between B and A denoted by R-1 defined by the set
{(b, a) [member of] B × A | (a, b) [member of] R}.
Given two partial or total functions f: A [right arrow] B and g: B [right arrow] C, with f = <A, G1, B> and g = <B, G2, C, their composition denoted by f [??] g (or f.g, or fg), is the partial or total function defined by A, G1 [??] G2, C>. Notice that according to our notation, f [??] g(x) = g(f(x)), that is, f is applied first. Note also that composition is associative.
2.1.4 Injections, Surjections, Bijections
A function f: A [right arrow] B is injective (or one to one) iff, for all x, y [member of] A, f(x) = f(y) implies that x = y.
A function f: A [right arrow] B is surjective (or onto) iff, for all y [member of] B, there is some x [member of] A such that f(x) = y. Equivalently, the range of f is the set B.
A function is bijective iff it is both injective and surjective.
It can be shown that a function f is surjective if and only if there exists a function g: B [right arrow] A such that g [??] f = IB. If there exists a function g: B [right arrow] A such that f [??] g = IA, then f: A [right arrow] B is injective. If f: A [right arrow] B is injective and A ≠ 0, then there exists a function g: B [right arrow] A such that f [??] g = IA. As a consequence, it can be shown that a function f: A [right arrow] B is bijective if and only if there is a unique function f-1 called its inverse such that f [??] f-1 = IA and f-1 [??] f = IB.
2.1.5 Direct Image, Inverse Image
Given a (partial) function f: A [right arrow] B, for every subset X of A, the direct image (or for short, image) of X under f is the set
{y [member of] B | [there exists]x [member of] X, f(x) = y}
and is denoted by f(X). For every subset Y of B, the inverse image of Y under f is the set
{x [member of] A | [there exists]y [member of] Y, f(x) = y}
and is denoted by f-1 (Y).
Warning: The function f may not have an inverse. Hence, f-1(Y) should not be confused with f-1 (y) for y [member of] B, which is only defined when f is a bijection.
2.1.6 Sequences
Given two sets I and X, an I-indexed sequence (or sequence) is any function A: I [right arrow] X, usually denoted by (Ai)i]member of]I. The set I is called the index set. If X is a set of sets, (Ai)i]member of]1 is called a family of sets.
2.1.7 Natural Numbers and Countability
The set of natural numbers (or nonnegative integers) is denoted by N and is the set {0, 1, 2, 3, ...}. A set A is countable (or denumerable) iff either A = 0 or there is a surjection h: N [right arrow] A from N onto A, countably infinite iff there is a bijection h: N [right arrow] A. Otherwise, A is said to be uncountable. The cardinality of a countably infinite set is denoted by ω. The set of positive integers is denoted by N+. For every positive integer n [member of] N+, the set {1, ..., n} is denoted as [n], and [0] denotes the empty set. A set A is finite iff there is a bijection h: [n] [right arrow] A for some natural number n [member of] N. The natural number n is called the cardinality of the set A, which is also denoted by |A|. When I is the set N of natural numbers, a sequence (Ai)i]member of]I is called a countable sequence, and when I is some set [n] with n [member of] N, (Ai)i]member of]I is a finite sequence.
(Continues...)
Excerpted from Logic for Computer Science by Jean H. Gallier. Copyright © 2015 Jean H. Gallier. Excerpted by permission of Dover Publications, Inc..
All rights reserved. No part of this excerpt may be reproduced or reprinted without permission in writing from the publisher.
Excerpts are provided by Dial-A-Book Inc. solely for the personal use of visitors to this web site.
Table of Contents
Contents
PREFACE (DOVER EDITION),PREFACE (1985 EDITION),
HOW TO USE THIS BOOK AS A TEXT,
Chapter 1: INTRODUCTION,
Chapter 2: MATHEMATICAL PRELIMINARIES,
Chapter 3: PROPOSITIONAL LOGIC,
Chapter 4: RESOLUTION IN PROPOSITIONAL LOGIC,
Chapter 5: FIRST-ORDER LOGIC,
Chapter 6: GENTZEN'S CUT ELIMINATION THEOREM AND APPLICATIONS,
Chapter 7: GENTZEN'S SHARPENED HAUPTSATZ; HERBRAND'S THEOREM,
Chapter 8: RESOLUTION IN FIRST-ORDER LOGIC,
Chapter 9: SLD-RESOLUTION AND LOGIC PROGRAMMING (PROLOG),
Chapter 10: MANY-SORTED FIRST-ORDER LOGIC,
APPENDIX,
REFERENCES,
INDEX OF SYMBOLS,
INDEX OF DEFINITIONS,
SUBJECT INDEX,