DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2025.39

A Strictly Linear Subatomic Proof System

Authors: Victoria Barrett, Alessio Guglielmi, and Benjamin Ralph

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

We present a subatomic deep-inference proof system for a conservative extension of propositional classical logic with decision trees that is strictly linear. In a strictly linear subatomic system, a single linear rule shape subsumes not only the structural rules, such as contraction and weakening, but also the unit equality rules. An interpretation map from subatomic logic to propositional classical logic recovers the usual semantics and proof theoretic properties. By using explicit substitutions that indicate the substitution of one derivation into another, we are able to show that the unit-equality inference steps can be eliminated from a subatomic system for propositional classical logic with only a polynomial complexity cost in the size of the derivation, from which it follows that the system p-simulates Frege systems, and we show cut elimination for the resulting strictly linear system.

Cite as

Victoria Barrett, Alessio Guglielmi, and Benjamin Ralph. A Strictly Linear Subatomic Proof System. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 39:1-39:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{barrett_et_al:LIPIcs.CSL.2025.39,
  author =	{Barrett, Victoria and Guglielmi, Alessio and Ralph, Benjamin},
  title =	{{A Strictly Linear Subatomic Proof System}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{39:1--39:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.39},
  URN =		{urn:nbn:de:0030-drops-227967},
  doi =		{10.4230/LIPIcs.CSL.2025.39},
  annote =	{Keywords: Deep inference, Open deduction, Subatomic logic, Decision trees, Explicit substitutions, Cut elimination, Proof theory}
}

Search Results

Documents authored by Barrett, Victoria

A Strictly Linear Subatomic Proof System

Abstract

Cite as

Thanks for your feedback!

Could not send message