Deep Inference for Graphical Theorem Proving

Abstract: In this talk, I will summarize my four-year thesis journey focused on designing graphical user interfaces (GUIs) for interactive proof construction. Deep inference proof theory guided my approach, inspiring innovative representations and interactions with logical entities.

The first part of the talk will introduce the Proof-by-Action paradigm, enabling users to construct proofs through direct manipulation of the proof state. Actema, a GUI prototype for intuitionistic first-order logic, demonstrates this approach with its drag-and-drop proof tactic grounded in "subformula linking", a recent technique based on the calculus of structures.

In the subsequent discussion, I will present an open-ended line of research where I aim to get rid of traditional symbolic formulas, in favor of more structured and iconic representations of the proof state. This includes the development of so-called "bubble calculi", a family of systems that reframe and extend the theory of nested sequents as local rewriting systems. Bubble calculi enjoy a graphical and topological interpretation, enable efficient sharing of contexts among subgoals, and capture both intuitionistic, dual-intuitionistic, bi-intuitionistic and classical logic in a unified way.

Finally, I will introduce the flower calculus, an intuitionistic refinement of C.S. Peirce's theory of existential graphs, understood as a system for interactive proof building. It provides more iconic and economical means of reasoning than bubble calculi, by exposing a small number of expressive rules that apply to the goals themselves, removing completely the need for logical connectives. I will conclude with a demonstration of the Flower Prover, another prototype of GUI in the Proof-by-Action paradigm, whose actions map directly to the rules of the flower calculus.

game theorylogic in computer scienceprogramming languagescomputer science theorycategory theory

Audience: researchers in the topic

University of Birmingham theoretical computer science seminar

Series comments: Meeting ID: 818 7333 5084 ~ Password: 217