nach oben

1997 | Buch

Kapitel lesen Erstes Kapitel lesen

Logic for Applications

verfasst von: Anil Nerode, Richard A. Shore

Verlag: Springer New York

Buchreihe : Texts in Computer Science

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten

Über dieses Buch

In writing this book, our goal was to produce a text suitable for a first course in mathematical logic more attuned than the traditional textbooks to the re cent dramatic growth in the applications oflogic to computer science. Thus, our choice oftopics has been heavily influenced by such applications. Of course, we cover the basic traditional topics: syntax, semantics, soundnes5, completeness and compactness as well as a few more advanced results such as the theorems of Skolem-Lowenheim and Herbrand. Much ofour book, however, deals with other less traditional topics. Resolution theorem proving plays a major role in our treatment of logic especially in its application to Logic Programming and PRO LOG. We deal extensively with the mathematical foundations ofall three ofthese subjects. In addition, we include two chapters on nonclassical logics - modal and intuitionistic - that are becoming increasingly important in computer sci ence. We develop the basic material on the syntax and semantics (via Kripke frames) for each of these logics. In both cases, our approach to formal proofs, soundness and completeness uses modifications of the same tableau method in troduced for classical logic. We indicate how it can easily be adapted to various other special types of modal logics. A number of more advanced topics (includ ing nonmonotonic logic) are also briefly introduced both in the nonclassical logic chapters and in the material on Logic Programming and PROLOG.

Inhaltsverzeichnis

Frontmatter

Introduction

Abstract

In 1020 logic was mostly a There were also a few mathe’ maticians there, cultivating the logical roots of the mathematical tree. Today, Re ooraiou Theory, Set Theory, Model and Proof Theory, logic’s major subdisciplines, have become full—fledged branches of mathematics. Since the 1970o, the winds of change have been blowing new seeds into the logic garden from computer scienceAIand linguistics. These winds have also uncovered a new topography with many prominences and depths, fertile soil for new logical subjects. These days, if you survey international meetings in computer science and linguistics, you will find that the language of mathematical logic is a lingua franca, that methods of mathematical logic are ubiquitous and that understanding new logics and finding feasible algorithms for implementing their inference procedures play a central role in many disciplines. The emerging areas with an important logic component include inupwrmtivo, declarative and functional programming; verification of programs; ioteraotbm, concurrent, distributed, fault tolerant and real time computing; knowledge—based systems; deductive databases; and VLSI design. Various types of logi are now also playing key roles in the modeling of reasoning in special fields from law to medicine.

Anil Nerode, Richard A. Shore

I. Propositional Logic

Abstract

Before starting on the basic material of this book, we introduce a general representation scheme which is one of the most important types of structures in logic and computer science: trees.

Anil Nerode, Richard A. Shore

II. Predicate Logic

Abstract

The logic of predicate encompasses much of the reasoning in the mathematical sciences. We are already familiar with the informal idea of a property holding of an object or a relation holding between objects. Any such property or relation is an example of apredicate. The difference between a property and a relation is just in the arity of the predicate. Unary predicates are simply properties of objects, binary ones are relations between pairs of objects and in general n-ary predicates express relations among n-tuples of objects. A reasonable answer to the question of what are 0-ary predicates might well be that they are propositions. The point here is that they are simply statements of facts independent of any variables. Thus, for example, if we are discussing the natural numbers we may let φ(x, y) denote the binary relation (predicate) “x is less than y”. In this case φ(3, y) denotes the property (unary predicate) of y “3 is less than y” and φ (3,4) denotes the (true) proposition (0-ary predicate) that 3 is less than 4.

Anil Nerode, Richard A. Shore

III. Prolog

Abstract

In this chapter we consider the full PROLOG language for logic programmin in predicate logic. Much of the basic terminology is simply the predicate logic version of that introduced in I.10. We, nonetheless, restate the basic definitions in a form suitable for resolution theorem proving in the predicate calculus. PROLOG employs a refinement of linear resolution but we have made the presentation independent of the (rather difficult) completeness theorem for linear resolution (Theorem II.14.4). We do, however, assume familiarity with the definitions for linear resolution in Definitions 11.14.1-3. Thus our proofs are based on the analysis of the propositional version of PROLOG discussed in I.l0, together with Herbrand’s theorem (II.10.4) and the reduction of predicate logic to propositional logic that it entails. At times when a knowledge of II.14 would illuminate certain ideas or simplify proofs, we mark such alternate results or proofs with an *.

Anil Nerode, Richard A. Shore

IV. Modal Logic

Abstract

Formal modal logics were developed to make precise the mathematical properties of differing conceptions of such notions as possibility, necessity, belief, knowledge and temporal progression which arise in philosophy and natural languages. In the last twenty-five years modal logics have emerged as useful tools for expressing essential ideas in computer science and artificial intelligence.

Anil Nerode, Richard A. Shore

V. Intuitionistic Logic

Abstract

During the past century, a majo debate in the philosophy of mathematics has centered on the question of how to regard noneffective or nonconstructive proofs in mathematics. Is it legitimate to claim to have proven the existence of a number with some property without actually being able, even in pöontplo, to produce one? Is it legitimate to claim to have proven the existence of a function without providing any way to calculate it? L. E. J. Brouwer is perhaps the best known early proponent of an extreme constructivist point of view. He rejected much of early twentieth century mathematics on the grounds that it did not provide acceptable existence proofs. He held that a proof of p ⋁ q must consist of either a proof of p or one of q and that a proof of ∃xP(x) must contain a construction of a witness c and a proof that P(c) is true. At the heart of most nonconstructive proofs lies the law of the excluded middle: For every sentence A, A ⋁ ⌝A is true. Based on this law of classical logic one can prove that ∃xP(x) by showing that its negation leads to a contradiction without providing any hint as to how to find an x Satisfying P. Similarly, one can prove ⌝ (⌝p ⋁ q by proving ⌝(⌝p ⋀ ⌝q) without knowing which of p and q is true.

Anil Nerode, Richard A. Shore

VI. Elements of Set Theory

Abstract

This book, like almost every other modern mathematics book, develops its subject matter assuming a knowledge of elementary set theory. This assumption is often not justified. In this chapter we offer an informal exposition of set theory. In §1–6, we present the axioms for set theory and develop enough of elementary set theory to formalize basic number theory including, for example, the uniqueness of the natural numbers up to isomorphism as a structure satisfying Peano’s famous axioms for successor as well as the existence and uniqueness of functions defined by induction or recursion on the natural numbers. We also present the basic set-theoretic notions such as functions, sequences and orders needed elsewhere in this book. In §7, we develop the basic notions of cardinality (size) for finite and countable sets. The remaining sections (8–11) establish the principle of transfinite induction and develop the basic theory of infinite ordinals and cardinals, the cumulative hierarchy of sets that forms the natural model of set theory, as well as some of the usual variants of the axiom of choice. Together, this material should supply a sufficient background in set theory for almost any graduate course of studies in computer science or mathematics. The exposition is independent of the rest of the book and repeats a small amount of material fromI.1and the historical appendix.

Anil Nerode, Richard A. Shore

Backmatter

Titel: Logic for Applications
verfasst von: Anil Nerode
Richard A. Shore
Verlag: Springer New York
Electronic ISBN: 978-1-4612-0649-1
Print ISBN: 978-1-4612-6855-0
DOI: https://doi.org/10.1007/978-1-4612-0649-1

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Introduction

I. Propositional Logic

II. Predicate Logic

III. Prolog

IV. Modal Logic

V. Intuitionistic Logic

VI. Elements of Set Theory

Backmatter