Skip to content

Proof Theory and Automated Deduction

ISBN-10: 1402003684

ISBN-13: 9781402003684

Edition: 1997

Authors: Jean Goubault-Larrecq, Ian Mackie

List price: $139.00
Shipping box This item qualifies for FREE shipping.
Blue ribbon 30 day, 100% satisfaction guarantee!
what's this?
Rush Rewards U
Members Receive:
Carrot Coin icon
XP icon
You have reached 400 XP and carrot coins. That is the daily max!

Description:

Proof Theory and Automated Deduction is written for final-year undergraduate and first-year post-graduate students. It should also serve as a valuable reference for researchers in logic and computer science. It covers basic notions in logic, with a particular stress on proof theory, as opposed to, for example, model theory or set theory; and shows how they are applied in computer science, and especially the particular field of automated deduction, i.e. the automated search for proofs of mathematical propositions. We have chosen to give an in-depth analysis of the basic notions, instead of giving a mere sufficient analysis of basic and less basic notions. We often derive the same theorem by different methods, showing how different mathematical tools can be used to get at the very nature of the objects at hand, and how these tools relate to each other. Instead of presenting a linear collection of results, we have tried to show that all results and methods are tightly interwoven. We believe that understanding how to travel along this web of relations between concepts is more important than just learning the basic theorems and techniques by rote. Audience: The book is a valuable reference for researchers in logic and computer science.
Customers also bought

Book details

List price: $139.00
Copyright year: 1997
Publisher: Springer
Publication date: 11/30/2001
Binding: Paperback
Pages: 444
Size: 6.00" wide x 9.00" long x 1.00" tall
Weight: 1.386
Language: English

List of Figures
Preface
Acknowledgements
Introduction
Overview
Classical Propositional Logic
Syntax
Semantics
Deduction Systems
Hilbert-style Systems
Natural Deduction
Gentzen Sequents
Automated Proof Methods
Tableaux
Prepositional Resolution
The Davis-Putnam Method
Binary Decision Diagrams
Digressions
Expressiveness of Prepositional Classical Logic
Boolean Algebras
Quantified Prepositional Logic
Other Propositional Logics
Introduction
Constructivity
Resources
Semantic Paradigms
Notation
Intuitionistic Logic
Intuitionistic Natural Deduction (NJ<sub>0</sub>)
Intuitionistic Sequent Calculus (LJ<sub>0</sub>)
Relating Sequent Calculus and Natural Deduction
Hilbert-style Presentation
Normalisation and Cut Elimination
Normalisation
Cut Elimination
Semantics of Intuitionistic Logic
Kripke Semantics
Intuitionistic Tableaux
Functional Interpretation
Relating Intuitionistic and Classical Logic
Additive and Multiplicative Connectives
Linear Logic
Syntax of Linear Logic
Classical Linear Sequent Calculus
Coding Intuitionistic Logic
The Curry-Howard Correspondence
Introduction
Functions
Typed �-Calculus and Natural Deduction
Typed �-calculus
Term Assignment for Natural Deduction
Properties
Combinatory Logic and Hilbert-Style Axioms
Combinatory Logic
The Correspondence with Hilbert Axioms
Applications of the Curry-Howard Correspondence
System F
Modal and Temporal Logics
Introduction and Motivation
S4 and Non-Monotonic Logics
Syntax
Philosophical Logic and Non-Monotonic Logics
Kripke Semantics
Decidability
Sequent Systems and Tableaux
Other Modal Logics Of Interest In Computer Science
Hennessy-Milner Logic
CTL
Propositional Dynamic Logic
Model-Checking
Sequential Machines and Symbolic Model-Checking
Binary Decision Diagrams
Developments
First-Order Classical Logic
Definitions
Syntax
Semantics
Deduction Systems
Expressive Power
Meta-Mathematical Properties
Prenex and Skolem Forms
Semantic Herbrand Theory
Cut-Elimination and Syntactic Herbrand Theory
Digressions
Non-classical logics
Arithmetic
Higher-order logics
Resolution
Fundamental Ideas
Unification
Resolution
Optimisations
Clause Selection Strategies
Deletion Strategies
Ordering Strategies
Semantic Resolution and Set-of-Support Strategies
The Linear Strategy
Other Refinements of Resolution
Resolution as Cut-Only Proofs
Tableaux, Connections and Matings
First-Order Tableaux
Using Herbrand's Theorem
Extension Steps
Free Variable Tableaux
Presentation
Herbrandizing On-the-fly
Discussion
Connections, Matings And Model Elimination
Connections and Matings
Relation with Resolution
Chang's V-Resolution
Model Elimination
Incorporating Knowledge
Motivations
Equality and Rewriting
Rewriting
Paramodulation, or Integrating Rewriting with Resolution
Equality and Tableaux
Rigid E-Unification
Equational Theories
Herbrand Theory Modulo an Equational Theory
E-Unification
Particular Theories
Further Reading
Other Theories
Sorts
Theory Resolution
Gr�bner Bases
Logic Programming Languages
Introduction
Prolog
Constraints
Parallelism
OR-parallelism
AND-parallelism
Answers to Exercises
Basics of Topology
Bibliography
Index