Formalisation and Automation of Foundational Theories - A LogiKEy Perspective

Explore a 42-minute conference talk by Christoph Benzmüller at the Hausdorff Center for Mathematics, focusing on the formalisation and automation of foundational theories from the LogiKEy perspective. Delve into four key statements, including the timeless nature of mathematical formalisation, the importance of formalising legal and ethical theories for AI control, and the shift towards clever cut introduction in proof automation. Examine the near-complete automation of Boolos' Curious Inference within Isabelle/HOL, demonstrating how intelligent cut-introduction can enable exponentially shorter proofs. Gain insights into the speaker's views on free logic and counter-model finding, supported by references to relevant research in artificial intelligence, legal reasoning, and logical frameworks.

Christoph Benzmüller: Comments on the formalisation and automation of foundational theories ...