For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Pablo Donato (LIX), invited by the PARTOUT team.

Abstract: In this talk, I will present the work I have been doing for my thesis in the past year and a half, which is an exploration in how to build formal proofs interactively through graphical, deep inference proof systems.

I will start with a demonstration of Actema, a prototype of graphical user interface for theorem proving in intuitionistic FOL based on direct manipulation of the proof state. A notable feature is the ability to reason by drag-and-dropping formulas within a sequent, which is a direct application of the subformula linking paradigm of K. Chaudhuri. The specificity of our approach lies in how we handle quantifiers through unification, as well as equalities. This enables both an elegant characterization, and a wide generalization of the behavior of standard rewrite tactics.

In the second part, I will present the “Bubble Calculus”, a new kind of nested sequent system which comes equipped with a nice graphical syntax. Inspired by the membranes of the Chemical Abstract Machine of Boudol and Berry, we add a so-called “bubble” construct for localizing interactions between propositions, which can be understood as internalizing the notion of premiss/subgoal inside judgments. By allowing bubbles to be polarized, one can then recover intuitionistic, dual-intuitionistic, bi-intuitionistic and classical logic as fragments which differ only in the allowed switch/membrane traversal rules.

In the third and last part, I will introduce an intuitionistic variant of the existential graphs of C. S. Peirce, arguably the first graphical proof system in the western logic tradition. To make the notation more readable, I will use a botanical metaphor where the graphs are represented as (nested) flowers. Contrarily to bubbles, flowers have a linear translation to and from traditional formulas, which allows to get completely rid of the latter in the proof system.

Join Zoom Meeting

• https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVpUVkxSZz09
• Meeting ID: 891 5561 2228
• Passcode: ZLEY8Z

The list of next seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics