Automated theorem proving

The book covers a comprehensive exploration of natural and formal logic, beginning with an abstraction from natural reasoning and establishing logical rules. It delves into the connection method in propositional logic, detailing its language, semantics, syntactic validity, connection calculus, and algorithmic aspects, complemented by exercises and historical remarks. The discussion extends to first-order logic, addressing its language, semantics, transformation to normal form, unification, and connection calculus, along with algorithmic considerations and exercises. Variants and improvements are examined, including resolution techniques, performance evaluation, connection graph resolution, and logical calculi of natural deduction. The text also presents alternative approaches such as linear unification and splitting by need, concluding with a summary and prospectus. Applications and extensions of the connection method are highlighted, focusing on knowledge structuring, programming, and problem-solving. It also addresses the connection method with equality, rewrite rules, induction, and higher-order logic, while discussing actual implementations and notable omissions. The book includes references and a list of symbols for further clarity and understanding.