Automated Reasoning in Practice

This lecture covers the practical aspects of automated reasoning, focusing on systems like TPTP, TSTP, and CASC. It delves into the history and applications of automated reasoning, successful systems like Isabelle and Coq, and the infrastructure of the TPTP project. The lecture also discusses tools for parsing, type checking, and running automated reasoning systems, emphasizing the importance of a consistent TPTP language and ontology. Additionally, it explores future developments in the field, such as proof combination and access to provenance information.