Proof theory and automated deduction

Authors Jean Goubault-Larrecq, Ian Mackie

Publication date 25 February 1998

Published in Applied Logic Series (Search for Journal in Brave)

algorithms automated deduction logic methodologies logic programming logical systems mathematical logic proof theory resolution

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Logic programming (68N17)

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.

Recommendations

Cited in

(23)

This page was built for publication: Proof theory and automated deduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1379289)