Proof complexity of substructural logics
type: Item
instance of: scholarly article
title: Proof complexity of substructural logics
zbMATH Open document ID: 1491.03078
author: Raheleh Jalali
published in: Annals of Pure and Applied Logic
publication date: 2021-06-14T00:00:00Z
full work available at URL: https://arxiv.org/abs/2006.09705
review text: The article is well written and organized, no typos where found. Three results are proved; the first one, is an exponential lower bound on the length of the proof of a sequence of hard \textbf{P}-tautologies \((\mathrm{Clique}_{n,k}\), and \(\mathrm{Color}_{n,m})\), namely a sequence of \textbf{P}-provable formulas \(\{A_n\}^\infty_{n=1}\), that is, the length of the shortest \textbf{P}-proof for \(A_n\) is exponential in \(|A_n|\), where \textbf{P} is a proof system as strong as full Lambek calculus (\textbf{FL}), and it is polynomially simulated by \textbf{eF} (extended Frege) for some superintuitionistic logic of \(\infty\)-branching, denoted by L-\textbf{EF}. The second result is a similar proof of the previous one but for a proof system and logic extending Visser's basic propositional calculus (\textbf{BPC}). And the third result is in the classical setting, again, an exponential lower bound on the number of proof line of any proof system polynomially simulated by \textbf{CLF}\(^{-}_{ew}\).
reviewed by: Ariel Germán Fernández
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B47
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F52
zbMATH DE Number: 7358539
zbMATH Keywords: proof complexity
zbMATH Keywords: substructural logics
zbMATH Keywords: subintuitionistic logics
MaRDI profile type: MaRDI publication profile
OpenAlex ID: W3138992896
arXiv ID: 2006.09705
cites work: The monotone circuit complexity of Boolean functions
cites work: A translation of intuitionistic predicate logic into basic predicate logic
cites work: An Introduction to Basic Arithmetic
cites work: Basic Propositional Calculus I
cites work: Proof Complexity of Non-classical Logics
cites work: The relative efficiency of propositional proof systems
cites work: Residuated lattices. An algebraic glimpse at substructural logics
cites work: Linear logic
cites work: The intractability of resolution
cites work: Disjunction property and complexity of substructural logics
cites work: A lower bound for intuitionistic logic
cites work: On lengths of proofs in non-classical logics
cites work: Substitution Frege and extended Frege proof systems in non-classical logics
cites work: Substructural logics with mingle
cites work: Proof Complexity
cites work: The Mathematics of Sentence Structure
cites work: Decision problems for propositional linear logic
cites work: Q4694214
cites work: Lower bounds for resolution and cutting plane proofs and monotone computations
cites work: Basic predicate calculus
cites work: Q3509064
cites work: A propositional logic with explicit fixed points
DOI: 10.1016/J.APAL.2021.102972
description: scientific article