Proof theory and automated deduction
type: Item
instance of: scholarly article
title: Proof theory and automated deduction
zbMATH Open document ID: 0896.03014
author: Jean Goubault-Larrecq
author: Ian Mackie
published in: Applied Logic Series
publication date: 1998-02-25T00:00:00Z
review text: For several years, mathematical logic and logic methodologies have been in wide use in computer science. Vast knowledge and expertise have been collected by computer scientists. It covers problem solving using logic tools, logic programming languages and programming systems built on a base of automated proofs. This comprehensive monograph collects the considerable work in mathematical logic and logic methodologies into a systematic encyclopedia of theory and practice. This monograph elaborates a wide range of logical systems, algorithms and automated deduction methods. The authors successfully offer an excellent introduction to logic for specialists in computer science. The book describes several logical systems, such as classical propositional logic, intuitionistic and linear logic, modal and temporal logic, combinatory logic, and classical first order logic, used in computer science. The authors represent various approaches to describe logic systems such as Hilbert-style systems, natural deduction systems, sequential systems, resolutions, and tableaux. The fundamentals of classical logical problems such as cut-elimination, Herbrand theorem, and prenex and Skolem normal forms are discussed in the monograph. The authors pay particular attention to resolution techniques, most closely related to computer science. Various strategies and refinements of the resolution method are described. The authors demonstrate how to incorporate specific knowledge into a logic system using paramodulation, \(E\)-unification, and rewriting. In conclusion, the authors give an overview of the logic programming languages PROLOG and CONSTRAINTS. The monograph is an excellent textbook for experts and novices, students at all levels, researchers and specialists in Computer Science.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03-02
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 03-01
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 68N17
zbMATH DE Number: 1120791
zbMATH Keywords: proof theory
zbMATH Keywords: logic programming
zbMATH Keywords: mathematical logic
zbMATH Keywords: logic methodologies
zbMATH Keywords: logical systems
zbMATH Keywords: algorithms
zbMATH Keywords: automated deduction
zbMATH Keywords: resolution
reviewed by: Nail Zamov
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 1120791