Proof theory and automated deduction (Q1379289)

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.