First-Order Logic and Automated Theorem Proving

First-Order Logic and Automated Theorem Proving by Melvin Fitting.

There are many kinds of books on formal logic. Some have philosophers as their intended audience, some mathematicians, some computer scientists. Although there is a common core to all such books they will be very dif­ ferent in emphasis, methods, and even appearance. This book is intended for comput...

Full description

Saved in:
Bibliographic Details
Main Author: Fitting, Melvin (Author)
Corporate Author: SpringerLink (Online service)
Format: eBook
Language:English
Published: New York, NY : Springer New York : Imprint: Springer, 1990.
Edition:1st ed. 1990.
Series:Monographs in Computer Science,
Springer eBook Collection.
Subjects:
Mathematical logic.
Computer logic.
Artificial intelligence.
Electronic resources (E-books)
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of Contents:
  • 1 Background
  • 2 Propositional Logic
  • 2.1 Introduction
  • 2.2 Propositional Logic — Syntax
  • 2.3 Propositional Logic — Semantics
  • 2.4 Boolean Valuations
  • 2.5 The Replacement Theorem
  • 2.6 Uniform Notation
  • 2.7 König’s Lemma
  • 2.8 Normal Forms
  • 2.9 Normal Form Implementations
  • 3 Semantic Tableaux and Resolution
  • 3.1 Propositional Semantic Tableaux
  • 3.2 Propositional Tableaux Implementations
  • 3.3 Propositional Resolution
  • 3.4 Soundness
  • 3.5 Hintikka’s Lemma
  • 3.6 The Model Existence Theorem
  • 3.7 Tableau and Resolution Completeness
  • 3.8 Completeness With Restrictions
  • 3.9 Propositional Consequence
  • 4 Other Propositional Proof Procedures
  • 4.1 Hilbert Systems
  • 4.2 Natural Deduction
  • 4.3 The Sequent Calculus
  • 4.4 The Davis-Putnam Procedure
  • 4.5 Computational Complexity
  • 5 First-Order Logic
  • 5.1 First-Order Logic — Syntax
  • 5.2 Substitutions
  • 5.3 First-Order Semantics
  • 5.4 First-Order Uniform Notation
  • 5.5 Hintikka’s Lemma
  • 5.6 Parameters
  • 5.7 The Model Existence Theorem
  • 5.8 Applications
  • 5.9 Logical Consequence
  • 5.10 Craig’s Interpolation Lemma
  • 5.11 Beth’s Definability Theorem
  • 6 First-Order Proof Procedures
  • 6.1 First-Order Semantic Tableaux
  • 6.2 First-Order Resolution
  • 6.3 Soundness
  • 6.4 Completeness
  • 6.5 Hilbert Systems
  • 6.6 Natural Deduction and Gentzen Sequents
  • 7 Implementing Tableaux and Resolution
  • 7.1 What Next
  • 7.2 Unification
  • 7.3 Unification Implemented
  • 7.4 Free Variable Semantic Tableaux
  • 7.5 A Tableau Implementation
  • 7.6 Free Variable Resolution
  • 7.7 Soundness
  • 7.8 Free Variable Tableau Completeness
  • 7.9 Free Variable Resolution Completeness
  • 7.10 The Replacement Theorem
  • 7.11 Skolemization
  • 7.12 PrenexForm
  • 8 Equality
  • 8.1 Introduction
  • 8.2 Syntax and Semantics
  • 8.3 The Equality Axioms
  • 8.4 Hintikka’s Lemma
  • 8.5 The Model Existence Theorem
  • 8.6 Consequences
  • 8.7 Tableau and Resolution Systems
  • 8.8 Alternate Tableaux and Resolution Systems
  • 8.9 A Free Variable Tableau System With Equality
  • 8.10 A Tableaux Implementation With Equality
  • 8.11 Paramodulation
  • References.

Similar Items