207 citations · 309 across the 9 of their papers we have counts for
9 papers
Proof Compression via Subatomic Logic and Guarded Substitutions
Victoria Barrett, Alessio Guglielmi, Benjamin Ralph +1
Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives.…
A Subatomic Proof System for Decision Trees
Chris Barrett, Alessio Guglielmi
We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees.…
Subatomic Proof Systems: Splittable Systems
Andrea Aler Tubella, Alessio Guglielmi
This paper presents the first in a series of results that allow us to develop a theory providing finer control over the complexity of normalisation, and in particular of cut elimin…
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Paola Bruscoli, Alessio Guglielmi, Tom Gundersen +1
Jeřábek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Ats…
A System of Interaction and Structure IV: The Exponentials and Decomposition
Lutz Strassburger, Alessio Guglielmi
We study a system, called NEL, which is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials. Equivalently, NEL is MELL augmented with t…
Normalisation Control in Deep Inference via Atomic Flows
Alessio Guglielmi, Tom Gundersen
We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flo…
On Structuring Proof Search for First Order Linear Logic
Paola Bruscoli, Alessio Guglielmi
Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the 'proof…
Consistency Without Cut Elimination
Kai Bruennler, Alessio Guglielmi
In this note we will show how to get consistency for first order classical logic, in a purely syntactic way, without going through cut elimination. The procedure is very simple and…
A System of Interaction and Structure
Alessio Guglielmi
This paper introduces a logical system, called BV, which extends multiplicative linear logic by a non-commutative self-dual logical operator. This extension is particularly challen…