Subatomic Proof Systems: Splittable Systems

Andrea Aler Tubella, Alessio Guglielmi

Research output: Contribution to journalArticle

1 Citation (Scopus)
66 Downloads (Pure)

Abstract

This article presents the first in a series of results that allow us to develop a theory providing finer control over the complexity of normalization, and in particular of cut elimination. By considering atoms as self-dual noncommutative connectives, we are able to classify a vast class of inference rules in a uniform and very simple way. This allows us to define simple conditions that are easily verifiable and that ensure normalization and cut elimination by way of a general theorem. In this article, we define and consider splittable systems, which essentially make up a large class of linear logics, including Multiplicative Linear Logic and BV, and we prove for them a splitting theorem, guaranteeing cut elimination and other admissibility results as corollaries. In articles to follow, we will extend this result to nonlinear logics. The final outcome will be a comprehensive theory giving a uniform treatment for most existing logics and providing a blueprint for the design of future proof systems.

Original languageEnglish
Article number5
Pages (from-to)1-33
Number of pages33
JournalACM Transactions on Computational Logic
Volume19
Issue number1
Early online date31 Jan 2018
DOIs
Publication statusPublished - 28 Feb 2018

Keywords

  • Cut-elimination
  • Deep inference
  • Normalisation
  • Subatomic proof systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)
  • Logic
  • Computational Mathematics

Fingerprint Dive into the research topics of 'Subatomic Proof Systems: Splittable Systems'. Together they form a unique fingerprint.

  • Projects

  • Profiles

    Cite this