# Logic for Computer Science

Foundations of Automatic Theorem Proving, Second Edition

Dover Publications (Verlag)
• 1. Auflage
• |
• erschienen am 18. Mai 2015
• |
• 528 Seiten

 E-Book | ePUB mit Adobe DRM | Systemvoraussetzungen
978-0-486-80508-5 (ISBN)

This advanced text for undergraduate and graduate students introduces mathematical logic with an emphasis on proof theory and procedures for algorithmic construction of formal proofs. The self-contained treatment is also useful for computer scientists and mathematically inclined readers interested in the formalization of proofs and basics of automatic theorem proving. 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.
 Reihe: Auflage: First Edition, First Sprache: Englisch Verlagsort: New York | USA Maße: Höhe: 234 mm | Breite: 156 mm Dateigröße: 67,45 MB Gewicht: 671 gr Schlagworte: ISBN-13: 978-0-486-80508-5 (9780486805085) ISBN-10: 0486805085 (0486805085)
weitere Ausgaben werden ermittelt
Jean H. Gallier
• Cover
• Title page
• Preface (Dover Edition)
• Preface (1985 Edition)
• How to use this Book as A Text
• Chapter 1: Introduction
• Chapter 2: Mathematical Preliminaries
• 2.1 Relations, Functions, Partial Orders, Induction
• 2.1.1 Relations
• 2.1.2 Partial Functions, Total Functions
• 2.1.3 Composition of Relations and Functions
• 2.1.4 Injections, Surjections, Bijections
• 2.1.5 Direct Image, Inverse Image
• 2.1.6 Sequences
• 2.1.7 Natural Numbers and Countability
• 2.1.8 Equivalence Relations
• 2.1.9 Partial and Total Orders
• 2.1.10 Well-Founded Sets and Complete Induction
• 2.1.11 Restrictions and Extensions
• 2.1.12 Strings
• 2.2 Tree Domains and Trees
• 2.2.1 Tree Domains
• 2.2.2 Trees
• 2.2.3 Paths
• 2.2.4 Subtrees
• 2.2.5 Tree Replacement
• 2.2.6 Ranked Alphabets and S-Trees
• 2.3 Inductive Definitions
• 2.3.1 Inductive Closures
• Inductive Sets
• 2.3.2 Freely Generated Sets
• 2.3.3 Functions Defined Recursively over Freely Generated
• Problems
• Chapter 3: Propositional Logic
• 3.1 Introduction
• 3.2 Syntax of Propositional Logic
• 3.2.1 The Language of Propositional Logic
• 3.2.2 Free Generation of PROP
• Problems
• 3.3 Semantics of Propositional Logic
• 3.3.1 The Semantics of Propositions
• 3.3.2 Satisfiability, Unsatisfiability, Tautologies
• 3.3.3 Truth Functions and Functionally Complete Sets of Connectives
• 3.3.4 Logical Equivalence and Boolean Algebras
• * 3.3.5 NP-Complete Problems
• Problems
• 3.4 Proof Theory of Propositional Logic: The Gentzen System G´
• 3.4.1 Basic Idea: Searching for a Counter Example
• 3.4.2 Sequents and the Gentzen System G'
• 3.4.3 Falsifiable and Valid Sequents
• 3.4.4 Axioms, Deduction Trees, Proof Trees, Counter Example Trees
• 3.4.5 Soundness of the Gentzen System G´,
• 3.4.6 The Search Procedure
• 3.4.7 Completeness of the Gentzen System G´
• 3.4.8 Conjunctive and Disjunctive Normal Form
• 3.4.9 Negation Normal Form
• Problems
• 3.5 Proof Theory for Infinite Sequents: Extended Completeness of G´,
• 3.5.1 Infinite Sequents
• 3.5.2 The Search Procedure for Infinite Sequents
• 3.5.3 König's Lemma
• 3.5.4 Signed Formulae
• 3.5.5 Hintikka Sets
• 3.5.6 Extended Completeness of the Gentzen System G´
• 3.5.7 Compactness, Model Existence, Consistency
• 3.5.8 Maximal Consistent Sets
• Problems
• 3.6 More on Gentzen Systems: The Cut Rule
• 3.6.1 Using Auxiliary Lemmas in Proofs
• 3.6.2 The Gentzen System LK´
• 3.6.3 Logical Equivalence of G´, LK´, and LK´ - {cut}
• 3.6.4 Gentzen's Hauptsatz for LK´ (Cut elimination theorem for LK')
• 3.6.5 Characterization of Consistency in LK´
• Problems
• Notes and Suggestions for Further Reading
• Chapter 4: Resolution in Propositional Logic
• 4.1 Introduction
• 4.2 A Special Gentzen System
• 4.2.1 Definition of the System GCNF´
• 4.2.2 Soundness of the System GCNF´
• 4.2.3 Completeness of the System GCNF´
• Problems
• 4.3 The Resolution Method for Propositional Logic
• 4.3.1 Resolution DAGs
• 4.3.2 Definition of the Resolution Method for Propositional Logic
• 4.3.3 Soundness of the Resolution Method
• 4.3.4 Converting GCNF´-proofs into Resolution Refutations and Completeness
• 4.3.5 From Resolution Refutations to GCNF´-proofs
• Problems
• Notes and Suggestions for Further Reading
• Chapter 5: First-Order Logic
• 5.1 Introduction
• 5.2 First-Order Languages
• 5.2.1 Syntax
• 5.2.2 Free Generation of the Set of Terms
• 5.2.3 Free Generation of the Set of Formulae
• 5.2.4 Free and Bound Variables
• 5.2.5 Substitutions
• Problems
• 5.3 Semantics of First-Order Languages
• 5.3.1 First-Order Structures
• 5.3.2 Semantics of Formulae
• 5.3.3 Satisfaction, Validity, and Model
• 5.3.4 A More Convenient Semantics
• 5.3.5 Free Variables and Semantics of Formulae
• 5.3.6 Subformulae and Rectified Formulae
• 5.3.7 Valid Formulae Obtained by Substitution in Tautologies
• 5.3.8 Complete Sets of Connectives
• 5.3.9 Logical Equivalence and Boolean Algebras
• Problems
• 5.4 Proof Theory of First-Order Languages
• 5.4.1 The Gentzen System G for Languages Without Equality
• 5.4.2 Deduction Trees for the System G
• 5.4.3 Soundness of the System G
• 5.4.4 Signed Formulae and Term Algebras (no Equality Symbol)
• 5.4.5 Reducts, Expansions
• 5.4.6 Hintikka Sets (Languages Without Equality)
• 5.4.7 Completeness: Special Case of Languages Without Function Symbols and Without Equality
• Problems
• 5.5 Completeness for Languages with Function Symbols and no Equality
• 5.5.1 Organizing the Terms for Languages with Function Symbols and no Equality
• 5.5.2 The Search Procedure for Languages with Function Symbols and no Equality
• 5.5.3 Completeness of the System G (Languages Without Equality)
• 5.5.4 Löwenheim-Skolem, Compactness, and Model Existence Theorems for Languages Without Equality
• 5.5.5 Maximal Consistent Sets
• Problems
• 5.6 A Gentzen System for First-Order Languages With Equality
• 5.6.1 Hintikka Sets for Languages With Equality
• 5.6.2 The Gentzen System G= (Languages With Equality)
• 5.6.3 Soundness of the System G=
• 5.6.4 Search Procedure for Languages With Equality
• 5.6.5 Completeness of the System G=
• 5.6.6 Löwenheim-Skolem, Compactness, and Model Existence Theorems for Languages With Equality
• 5.6.7 Maximal Consistent Sets
• 5.6.8 Application of the Compactness and Löwenheim-Skolem Theorems: Nonstandard Models of Arithmetic
• Problems
• Notes and Suggestions for Further Reading
• Chapter 6: Gentzen'S Cut Elimination Theorem and Applications
• 6.1 Introduction
• 6.2 Gentzen System LK for Languages Without Equality
• 6.2.1 Syntax of LK
• 6.2.2 The Logical Equivalence of the Systems G, LK, and LK - {cut}
• Problems
• 6.3 The Gentzen System LKe With Equality
• 6.3.1 Syntax of LKe
• 6.3.2 A Permutation Lemma for the System G=
• 6.3.3 Logical equivalence of G=, LKe, and LKe Without Essentia Cuts: Gentzen's Hauptsatz for LKe Without Essential Cuts
• Problems
• 6.4 Gentzen's Hauptsatz for Sequents in NNF
• 6.4.1 Negation Normal Form
• 6.4.2 The Gentzen System G1nnf
• 6.4.3 Completeness of G1nnf
• 6.4.4 The Cut Elimination Theorem for G1nnf
• 6.4.5 The System G1nnf
• 6.4.6 The Cut Elimination Theorem for G1nnf
• Problems
• 6.5 Craig's Interpolation Theorem
• 6.5.1 Interpolants
• 6.5.2 Craig's Interpolation Theorem Without Equality
• 6.5.3 Craig's Interpolation Theorem With Equality
• Problems
• 6.6 Beth's Definability Theorem
• 6.6.1 Implicit and Explicit Definability
• 6.6.2 Explicit Definability Implies Implicit Definability
• 6.6.3 Beth's Definability Theorem, Without Equality
• 6.6.4 Beth's Definability Theorem, With Equality
• Problems
• 6.7 Robinson's Joint Consistency Theorem
• Problems
• Notes and Suggestions for Further Reading
• Chapter 7: Gentzen'S Sharpened Hauptsatz
• Herbrand'S Theorem
• 7.1 Introduction
• 7.2 Prenex Normal Form
• Problems
• 7.3 Gentzen's Sharpened Hauptsatz for Prenex Formulae
• 7.3.1 Pure Variable Proofs
• 7.3.2 The Permutability Lemma
• 7.3.3 Gentzen's Sharpened Hauptsatz
• Problems
• 7.4 The Sharpened Hauptsatz for Sequents in NNF
• 7.4.1 The System G2nnf
• 7.4.2 Soundness of the System G2nnf
• 7.4.3 A Gentzen-like Sharpened Hauptsatz for G2nnf
• 7.4.4 The Gentzen System G1nnf
• 7.4.5 A Gentzen-like Sharpened Hauptsatz for G1nnf
• Problems
• 7.5 Herbrand's Theorem for Prenex Formulae
• 7.5.1 Preliminaries
• 7.5.2 Skolem Function and Constant Symbols
• 7.5.3 Substitutions
• 7.5.4 Herbrand's Theorem for Prenex Formulae
• Problems
• 7.6 Skolem-Herbrand-Gödel's Theorem for Formulae in NNF
• 7.6.1 Skolem-Herbrand-Gödel's Theorem in Unsatisfiability Form
• 7.6.2 Skolem Normal Form
• 7.6.3 Compound Instances
• 7.6.4 Half of a Herbrand-like Theorem for Sentences in NNF
• 7.6.5 Skolem-Herbrand-Gödel's Theorem (Sentences in NNF)
• 7.6.6 Comparison of Herbrand and Skolem-Herbrand-Gödel Theorems
• Problems
• * 7.7 The Primitive Recursive Functions
• 7.7.1 The Concept of Computability
• 7.7.2 Definition of the Primitive Recursive Functions
• 7.7.3 The Partial Recursive Functions
• 7.7.4 Some Primitive Recursive Functions
• Problems
• Notes and Suggestions for Further Reading
• Chapter 8: Resolution in First-Order Logic
• 8.1 Introduction
• 8.2 Formulae in Clause Form
• 8.3 Ground Resolution
• 8.4 Unification and the Unification Algorithm
• 8.4.1 Unifiers and Most General Unifiers
• 8.4.2 The Unification Algorithm
• Problems
• 8.5 The Resolution Method for First-Order Logic
• 8.5.1 Definition of the Method
• 8.5.2 Soundness of the Resolution Method
• 8.5.3 Completeness of the Resolution Method
• Problems
• 8.6 A Glimpse at Paramodulation
• Notes and Suggestions for Further Reading
• Chapter 9: Sld-Resolution and Logic Programming (PROLOG)
• 9.1 Introduction
• 9.2 GCjtyF´-Proofs in SLD-Form
• 9.2.1 The Case of Definite Clauses
• 9.2.2 GGVF´-Proofs in SLD-Form
• 9.2.3 Completeness of Proofs in SLD-Form
• Problems
• 9.3 SLD-Resolution in Propositional Logic
• 9.3.1 SLD-Derivations and SLD-Refutations
• 9.3.2 Completeness of SLD-Resolution for Horn Clauses
• Problems
• 9.4 SLD-Resolution in First-Order Logic
• 9.4.1 Definition of SLD-Refutations
• 9.4.2 Completeness of SLD-Resolution for Horn Clauses
• Problems
• 9.5 SLD-Resolution, Logic Programming (PROLOG)
• 9.5.1 Refutations as Computations
• 9.5.2 Model-Theoretic Semantics of Logic Programs
• 9.5.3 Correctness of SLD-Resolution as a Computation Procedure
• 9.5.4 Completeness of SLD-Resolution as a Computational Procedure
• 9.5.5 Limitations of PROLOG
• Problems
• Notes and Suggestions for Further Reading
• Chapter 10: Many-Sorted First-Order Logic
• 10.1 Introduction
• 10.2 Syntax
• 10.2.1 Many-Sorted First-Order Languages
• 10.2.2 Free Generation of Terms and Formulae
• 10.2.3 Free and Bound Variables, Substitutions
• Problems
• 10.3 Semantics of Many-Sorted First-Order Languages
• 10.3.1 Many-Sorted First-Order Structures
• 10.3.2 Semantics of Formulae
• 10.3.3 An Alternate Semantics
• 10.3.4 Semantics and Free Variables
• 10.3.5 Subformulae and Rectified Formulae
• Problems
• 10.4 Proof Theory of Many-Sorted Languages
• 10.4.1 Gentzen System G for Many-Sorted Languages Without Equality
• 10.4.2 Deduction Trees for the System G
• 10.4.3 Soundness of the System G
• 10.4.4 Completeness of G
• 10.5 Many-Sorted First-Order Logic With Equality
• 10.5.1 Gentzen System G= for Languages With Equality
• 10.5.2 Soundness of the System G=
• 10.5.3 Completeness of the System G=
• 10.5.4 Reduction of Many-Sorted Logic to One-Sorted Logic
• Problems
• 10.6 Decision Procedures Based on Congruence Closure
• 10.6.1 Decision Procedure for Quantifier-free Formulae Without Predicate Symbols
• 10.6.2 Congruence Closure on a Graph
• 10.6.3 The Graph Associated With a Conjunction
• 10.6.4 Existence of the Congruence Closure
• 10.6.5 Decision Procedure for Quantifier-free Formulae
• 10.6.6 Computing the Congruence Closure
• Problems
• Notes and Suggestions for Further Reading
• Appendix
• 2.4 Algebras
• 2.4.1 Definition of an Algebra
• 2.4.2 Homomorphisms
• 2.4.3 Subalgebras
• 2.4.4 Least Subalgebra Generated by a Subset
• 2.4.5 Subalgebras Freely Generated by a Set X
• 2.4.6 Congruences
• 2.4.7 Quotient Algebras
• 2.5 Many-Sorted Algebras
• 2.5.1 S-Ranked Alphabets
• 2.5.2 Definition of a Many-Sorted Algebra
• 2.5.3 Homomorphisms
• 2.5.4 Subalgebras
• 2.5.5 Least Subalgebras
• 2.5.6 Freely Generated Subalgebras
• 2.5.7 Congruences
• 2.5.8 Quotient Algebras
• 2.5.9 Many-Sorted Trees
• Problems
• References
• Index of Symbols
• Index of Definitions
• Subject Index
Schweitzer Klassifikation
DNB DDC Sachgruppen
Dewey Decimal Classfication (DDC)
BISAC Classifikation

Dateiformat: EPUB

Systemvoraussetzungen:

Computer (Windows; MacOS X; Linux): Installieren Sie bereits vor dem Download die kostenlose Software Adobe Digital Editions (siehe E-Book Hilfe).

Tablet/Smartphone (Android; iOS): Installieren Sie bereits vor dem Download die kostenlose App Adobe Digital Editions (siehe E-Book Hilfe).

E-Book-Reader: Bookeen, Kobo, Pocketbook, Sony, Tolino u.v.a.m. (nicht Kindle)

Das Dateiformat EPUB ist sehr gut für Romane und Sachbücher geeignet - also für "fließenden" Text ohne komplexes Layout. Bei E-Readern oder Smartphones passt sich der Zeilen- und Seitenumbruch automatisch den kleinen Displays an. Mit Adobe-DRM wird hier ein "harter" Kopierschutz verwendet. Wenn die notwendigen Voraussetzungen nicht vorliegen, können Sie das E-Book leider nicht öffnen. Daher müssen Sie bereits vor dem Download Ihre Lese-Hardware vorbereiten.

Weitere Informationen finden Sie in unserer E-Book Hilfe.

 33,49 € inkl. 19% MwSt.