Title: Formalising Haag-Kastler Nets In Higher-Order Logic
Speaker: Richard Schmoetten
Despite the enormous experimental success of quantum field theory (QFT) and its standard model of particle physics, its logical grounding remains ambiguous. Differing tools and methods are introduced more or less rigorously, and consequently the theory as a whole has no formal axiomatic basis. Algebraic QFT (AQFT) is an attempt to redress this deficiency, and my PhD is about enriching it with interactive and automated reasoning, in the guise of Isabelle/HOL.