FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Two Unifying Structural Principles

Author: Alessio Guglielmi

Paper Information

Title:Two Unifying Structural Principles
Authors:Alessio Guglielmi
Proceedings:TYDI-0 Abstracts
Editor: Lutz Stra├čburger
Keywords:proof theory, normalisation, proof semantics, proof complexity
Abstract:

ABSTRACT. It is possible to design proof systems for a vast range of logics, including all the common ones, by adopting two general proof constructors:

(1) the subatomic shape recently introduced by Andrea Aler Tubella, and

(2) a very general notion of formal substitution that is currently being explored by Benjamin Ralph and that subsumes standard quantification.

The two constructors could be considered two design principles, or, in other words, two ways of looking at proofs. In this talk, I will show how, by adopting them, we get a good starting point for designing proof systems that naturally yield canonical proofs of minimal size and that allow for a unified normalisation theory.

Pages:1
Talk:Jul 07 14:00 (Session 28N: Medial)
Paper: