Subject Area: CS Basics (Logics, Discrete Mathematics)
in CIDEC Library.

### FIRST-ORDER LOGIC AND AUTOMATED THEOREM PROVING

2nd ed

Melvin **FITTING**, 1942- , The City of New York University, Bronx, NY, USA
Series:
Graduate Texts in Computer Science.

Eds.: D. Gries; F. Schneider. (Springer-Verlag New York Inc.)

**Publisher : **
Springer-Verlag - New York

**Bibliographic : **

- Hardcover (alk. paper)
- ISBN: 0-387-94593-8
- 2nd ed. © 1996
- xvi, 326 p. : ill. 15 figs.; 25 cm.
- Dewey No.: 511.3 20

- Automatic theorem proving. * Logic, Symbolic and mathematical.
- I16048 Mathematical Logic and Formal Languages
- I1603X Logics and Meanings of Programs
- I19012 Artificial Intelligence

**DESCRIPTION: **

This graduate-level text presents fundamental concepts and results of classical logic in a rigorous
mathematical style. Applications to automated theorem proving are considered and usable Prolog programs
provided. It will serve both as a first text in formal logic and an introduction to automation issues for students
in computer science or mathematics. The book treats propositional logic, first-order logic, and first-order
logic with equality. In each case the initial presentation is semantic, to define the intended subjects
independently of the choice of proof mechanism. Then many kinds of proof procedure are introduced.
Results such as completeness, compactness, and interpolation are established, and theorem provers are
implemented in Prolog. This new edition includes material on AE calculus, Herbrand's Theorem, Gentzen's
Theorem, and related topics.
**CONTENTS: **

Includes bibliographical references (p. [315]-318) and index.

**BOOK CATEGORY: ** Advanced Textbook

Changed 20/01/1997. Comments: monika@cs.ioc.ee