Pablo Donato on Nostr: This is a bit of a late announcement, but I successfully defended my PhD thesis! It ...
This is a bit of a late announcement, but I successfully defended my PhD thesis!
It is about the exploration of a new paradigm for building formal proofs interactively that I call "Proof-by-Action", where the textual tactics of state-of-the-art proof assistants are replaced by direct manipulation actions on the proof state in a GUI. This is founded on a recent branch of structural proof theory called "deep inference".
The manuscript is now officially available on HAL: https://theses.hal.science/tel-04698985.
It is about the exploration of a new paradigm for building formal proofs interactively that I call "Proof-by-Action", where the textual tactics of state-of-the-art proof assistants are replaced by direct manipulation actions on the proof state in a GUI. This is founded on a recent branch of structural proof theory called "deep inference".
The manuscript is now officially available on HAL: https://theses.hal.science/tel-04698985.