Automatic Reasoning

Formal logical proof systems aim at providing support for solving complex reasoning tasks such as mathematical proofs or the verification of software system, an area where humans tend to make mistakes and get easily overwhelmed by details.

This book gives a comprehensive and extensively motivated presentation of the theoretical foundations of automatic reasoning systems, enabling beginners to gain an overview of this complex field. It is suitable as a basis for a corresponding course but also useful for specialists who wish to familiarize themselves with this subject.

It is suitable as a basis for a corresponding course but also useful for specialists who wish to familiarize themselves with this subject.

Contents

• Syntax, semantics, and inference systems for logical reasoning.
• Fundamental forms of reasoning: propositional and predicate logic.
• Reasoning about computation: the -calculus.
• Reasoning about program properties: simple type theory.
• A uniform calculus: constructive type theory.
• Automating formal reasoning: interactive proof assistants.

This book is a translation of the original German edition. The translation was done with the help of an artificial intelligence machine translation tool. A subsequent human revision was done primarily in terms of content, so that the book may read stylistically differently from a conventional translation.