Subatomic Proof Systems: Splittable Systems

Andrea Aler Tubella, Alessio Guglielmi

Research output: Contribution to journalArticle

1 Citation (Scopus)
23 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
DOIs
Publication statusPublished - 1 Feb 2018

Fingerprint

Blueprints
Cut-elimination
Proof System
Linear Logic
Atoms
Normalization
Logic
Inference Rules
Admissibility
Theorem
Multiplicative
Corollary
Classify
Series
Class

Keywords

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

ASJC Scopus subject areas

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

Cite this

Subatomic Proof Systems: Splittable Systems. / Aler Tubella, Andrea; Guglielmi, Alessio.

In: ACM Transactions on Computational Logic, Vol. 19, No. 1, 5, 01.02.2018, p. 1-33.

Research output: Contribution to journalArticle

@article{6afb2664a6aa4022911d48bfc317ecd4,
title = "Subatomic Proof Systems: Splittable Systems",
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.",
keywords = "Cut-elimination, Deep inference, Normalisation, Subatomic proof systems",
author = "{Aler Tubella}, Andrea and Alessio Guglielmi",
year = "2018",
month = "2",
day = "1",
doi = "10.1145/3173544",
language = "English",
volume = "19",
pages = "1--33",
journal = "ACM Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery",
number = "1",

}

TY - JOUR

T1 - Subatomic Proof Systems: Splittable Systems

AU - Aler Tubella, Andrea

AU - Guglielmi, Alessio

PY - 2018/2/1

Y1 - 2018/2/1

N2 - 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.

AB - 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.

KW - Cut-elimination

KW - Deep inference

KW - Normalisation

KW - Subatomic proof systems

UR - http://www.scopus.com/inward/record.url?scp=85042515848&partnerID=8YFLogxK

U2 - 10.1145/3173544

DO - 10.1145/3173544

M3 - Article

VL - 19

SP - 1

EP - 33

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 1

M1 - 5

ER -