Applied Logic

By: I. Mackie, Jean Goubault-Larrecq

Write A Review

Paperback | 30 November 2001

At a Glance

Paperback
444 Pages

Dimensions(cm)
23.5 x 15.5 x 2.54

Paperback

$84.99

or 4 interest-free payments of $21.25 with

Ships in 5 to 7 business days

The last twenty years have witnessed an accelerated development of pure and ap plied logic, particularly in response to the urgent needs of computer science. Many traditional logicians have developed interest in applications and in parallel a new generation of researchers in logic has arisen from the computer science community. A new attitude to applied logic has evolved, where researchers tailor a logic for their own use in the same way they define a computer language, and where auto mated deduction for the logic and its fragments is as important as the logic itself. In such a climate there is a need to emphasise algorithmic logic methodologies alongside any individual logics. Thus the tableaux method or the resolution method are as central to todays discipline of logic as classical logic or intuitionistic logic are. From this point of view, J. Goubault and I. Mackie's book on Proof Theory and Automated Deduction is most welcome. It covers major algorithmic methodolo gies as well as a variety of logical systems. It gives a wide overview for the ap plied consumer of logic while at the same time remains relatively elementary for the beginning student. A decade ago I put forward my view that a logical system should be presented as a point in a grid. One coordinate is its philosphy, motivation, its accepted theorems and its required non-theorems. The other coordinate is the algorithmic methodol ogy and execution chosen for its effective presentation. Together these two aspects constitute a 'logic'.

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $89.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

You Can Find This Book In

Non-Fiction Mathematics Mathematical Foundation Mathematical Logic Computing & I.T.Computer Science Artificial Intelligence Philosophy Philosophy & Logic Calculus & Mathematical Analysis Numerical Analysis Computer Programming & Software Development

Algorithms & Data Structures

List of Figures	p. xi
Preface	p. xiii
Acknowledgements	p. xv
Introduction	p. 1
Overview	p. 6
Classical Propositional Logic	p. 11
Syntax	p. 11
Semantics	p. 15
Deduction Systems	p. 19
Hilbert-style Systems	p. 20
Natural Deduction	p. 24
Gentzen Sequents	p. 36
Automated Proof Methods	p. 40
Tableaux	p. 40
Prepositional Resolution	p. 47
The Davis-Putnam Method	p. 53
Binary Decision Diagrams	p. 56
Digressions	p. 66
Expressiveness of Prepositional Classical Logic	p. 66
Boolean Algebras	p. 68
Quantified Prepositional Logic	p. 71
Other Propositional Logics	p. 73
Introduction	p. 73
Constructivity	p. 73
Resources	p. 75
Semantic Paradigms	p. 76
Notation	p. 77
Intuitionistic Logic	p. 79
Intuitionistic Natural Deduction (NJ₀)	p. 80
Intuitionistic Sequent Calculus (LJ₀)	p. 83
Relating Sequent Calculus and Natural Deduction	p. 85
Hilbert-style Presentation	p. 89
Normalisation and Cut Elimination	p. 95
Normalisation	p. 96
Cut Elimination	p. 98
Semantics of Intuitionistic Logic	p. 102
Kripke Semantics	p. 102
Intuitionistic Tableaux	p. 106
Functional Interpretation	p. 110
Relating Intuitionistic and Classical Logic	p. 111
Additive and Multiplicative Connectives	p. 117
Linear Logic	p. 119
Syntax of Linear Logic	p. 120
Classical Linear Sequent Calculus	p. 121
Coding Intuitionistic Logic	p. 126
The Curry-Howard Correspondence	p. 131
Introduction	p. 131
Functions	p. 133
Typed -Calculus and Natural Deduction	p. 134
Typed -calculus	p. 134
Term Assignment for Natural Deduction	p. 139
Properties	p. 143
Combinatory Logic and Hilbert-Style Axioms	p. 147
Combinatory Logic	p. 147
The Correspondence with Hilbert Axioms	p. 150
Applications of the Curry-Howard Correspondence	p. 152
System F	p. 153
Modal and Temporal Logics	p. 157
Introduction and Motivation	p. 157
S4 and Non-Monotonic Logics	p. 158
Syntax	p. 158
Philosophical Logic and Non-Monotonic Logics	p. 159
Kripke Semantics	p. 161
Decidability	p. 165
Sequent Systems and Tableaux	p. 168
Other Modal Logics Of Interest In Computer Science	p. 170
Hennessy-Milner Logic	p. 170
CTL	p. 172
Propositional Dynamic Logic	p. 173
Model-Checking	p. 176
Sequential Machines and Symbolic Model-Checking	p. 177
Binary Decision Diagrams	p. 181
Developments	p. 182
First-Order Classical Logic	p. 185
Definitions	p. 185
Syntax	p. 185
Semantics	p. 188
Deduction Systems	p. 190
Expressive Power	p. 191
Meta-Mathematical Properties	p. 197
Prenex and Skolem Forms	p. 197
Semantic Herbrand Theory	p. 201
Cut-Elimination and Syntactic Herbrand Theory	p. 210
Digressions	p. 220
Non-classical logics	p. 221
Arithmetic	p. 221
Higher-order logics	p. 224
Resolution	p. 233
Fundamental Ideas	p. 233
Unification	p. 235
Resolution	p. 241
Optimisations	p. 244
Clause Selection Strategies	p. 244
Deletion Strategies	p. 245
Ordering Strategies	p. 250
Semantic Resolution and Set-of-Support Strategies	p. 254
The Linear Strategy	p. 260
Other Refinements of Resolution	p. 263
Resolution as Cut-Only Proofs	p. 264
Tableaux, Connections and Matings	p. 269
First-Order Tableaux	p. 269
Using Herbrand's Theorem	p. 270
Extension Steps	p. 273
Free Variable Tableaux	p. 274
Presentation	p. 274
Herbrandizing On-the-fly	p. 276
Discussion	p. 279
Connections, Matings And Model Elimination	p. 281
Connections and Matings	p. 281
Relation with Resolution	p. 282
Chang's V-Resolution	p. 285
Model Elimination	p. 287
Incorporating Knowledge	p. 293
Motivations	p. 293
Equality and Rewriting	p. 295
Rewriting	p. 295
Paramodulation, or Integrating Rewriting with Resolution	p. 306
Equality and Tableaux	p. 310
Rigid E-Unification	p. 312
Equational Theories	p. 317
Herbrand Theory Modulo an Equational Theory	p. 318
E-Unification	p. 319
Particular Theories	p. 323
Further Reading	p. 325
Other Theories	p. 325
Sorts	p. 325
Theory Resolution	p. 331
Gröbner Bases	p. 333
Logic Programming Languages	p. 341
Introduction	p. 341
Prolog	p. 343
Constraints	p. 350
Parallelism	p. 354
OR-parallelism	p. 354
AND-parallelism	p. 356
Answers to Exercises	p. 357
Basics of Topology	p. 403
Bibliography	p. 407
Index	p. 415
Table of Contents provided by Publisher. All Rights Reserved.

Applied Logic

At a Glance

Paperback

Shipping

How to return your order

Defective items

You Can Find This Book In

More in Numerical Analysis

Monte Carlo and Quasi-Monte Carlo 2024

MCQMC 2024, Waterloo, Canada, August 18â"23

Advances in Numerical Methods and Analysis

Introductory Numerical Analysis

Learning Data Science

Data Wrangling, Exploration, Visualization, and Modeling with Python

Introduction to Finite Element Analysis Using Matlab(r) and Abaqus

Impact Dynamics

A Numerical Approach

Data-Driven Modeling & Scientific Computation

Methods for Complex Systems & Big Data

Chapman & Hall/CRC Numerical Analysis and Scientific Computi

Chapman & Hall/CRC Numerical Analysis and Scientific Computing Series

Fuzzy Model-Based Sliding Mode Control of Complex Nonlinear Systems

Engineering Mathematics and Operations Research

Application of Numerical Methods in Engineering Problems using MATLAB®

Flight Mechanics Modeling and Analysis

Monte Carlo Integration with MATLAB and Simulink

Numerical Methods for Modeling Metasurface with GSTC

Infinite-Dimensional Spectral Computations

Foundations, Algorithms, and Modern Applications

New Trends in the Applications of Differential Equations in Sciences

NTADES 2025, Saints Constantine and Helena, Bulgaria, September 1â"4

Mathematics and Intelligent Systems in Industry

MISI'25 Conference, Safi, Morocco, July 9â"10, 2025

Computational and Experimental Simulations in Engineering

Proceedings of ICCES 2025, Volume 4

Mathematics for Industrial Applications

8th ICoMS, Athens, Greece, September 24â"26, 2025

PDE-constrained optimization within FreeFEM

SpringerBriefs on PDEs and Data Science

Heuristic Search Methods and Dynamics for Multi-Body Gravitational Systems

With Mission Applications for Cislunar Space, the Moon, and Mars

Python Essentials

Symbolic and Numeric Problem-Solving in Engineering

Quantum Chaos and Disorder

An Introduction with Sample Programs and Exercises

Modeling with Knowledge and Data

Concepts and Applications for Engineers

Introduction to Numerical Mathematics

Theory, Practice and Numerous Examples

This product is categorised by