-
Proof Compression via Subatomic Logic and Guarded Substitutions
Authors:
Victoria Barrett,
Alessio Guglielmi,
Benjamin Ralph,
Lutz Straßburger
Abstract:
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. As a consequence, we can give a subatomic proof system for propositional classical logic such that all derivations are strictly linear: no inference step deletes or adds information, even units.
In this paper, we intr…
▽ More
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. As a consequence, we can give a subatomic proof system for propositional classical logic such that all derivations are strictly linear: no inference step deletes or adds information, even units.
In this paper, we introduce a powerful new proof compression mechanism that we call guarded substitutions, a variant of explicit substitutions, which substitute only guarded occurrences of a free variable, instead of all free occurrences. This allows us to construct ''superpositions'' of derivations, which simultaneously represent multiple subderivations. We show that a subatomic proof system with guarded substitution can p-simulate a Frege system with substitution, and moreover, the cut-rule is not required to do so.
△ Less
Submitted 26 May, 2025;
originally announced May 2025.
-
Fast Iterative Configuration of Reconfigurable Intelligent Surfaces in mmWave Systems
Authors:
Anna V. Guglielmi,
Stefano Tomasin
Abstract:
Reconfigurable intelligent surfaces (RISs) are a promising solution to improve the coverage of cellular networks, thanks to their ability to steer impinging signals in desired directions. However, they introduce an overhead in the communication process since the optimal configuration of a RIS depends on the channels to and from the RIS, which must be estimated. In this paper, we propose a novel fa…
▽ More
Reconfigurable intelligent surfaces (RISs) are a promising solution to improve the coverage of cellular networks, thanks to their ability to steer impinging signals in desired directions. However, they introduce an overhead in the communication process since the optimal configuration of a RIS depends on the channels to and from the RIS, which must be estimated. In this paper, we propose a novel fast iterative configuration (FIC) protocol to determine the optimal RIS configuration that exploits the small number of paths of millimetre-wave (mmWave) channels and an adaptive choice of the explored RIS configurations. In particular, we split the elements of the RIS into a number of subsets equal to the number of channel taps. For each subset, then an iterative procedure finds at each iteration the optimal RIS configuration in a codebook exploring a two-dimensional grid of possible angles of arrival and departure of the path at the RIS. Over the iterations, the grid is made finer around the point identified in previous iterations. Numerical results obtained using an urban channel model confirm that the proposed solution is fast and provides a configuration close to the optimal in a shorter time than other existing approaches.
△ Less
Submitted 5 March, 2024;
originally announced March 2024.
-
Information Theoretic Key Agreement Protocol based on ECG signals
Authors:
Anna V. Guglielmi,
Alberto Muraro,
Giulia Cisotto,
Nicola Laurenti
Abstract:
Wireless body area networks (WBANs) are becoming increasingly popular as they allow individuals to continuously monitor their vitals and physiological parameters remotely from the hospital. With the spread of the SARS-CoV-2 pandemic, the availability of portable pulse-oximeters and wearable heart rate detectors has boomed in the market. At the same time, in 2020 we assisted to an unprecedented inc…
▽ More
Wireless body area networks (WBANs) are becoming increasingly popular as they allow individuals to continuously monitor their vitals and physiological parameters remotely from the hospital. With the spread of the SARS-CoV-2 pandemic, the availability of portable pulse-oximeters and wearable heart rate detectors has boomed in the market. At the same time, in 2020 we assisted to an unprecedented increase of healthcare breaches, revealing the extreme vulnerability of the current generation of WBANs. Therefore, the development of new security protocols to ensure data protection, authentication, integrity and privacy within WBANs are highly needed. Here, we targeted a WBAN collecting ECG signals from different sensor nodes on the individual's body, we extracted the inter-pulse interval (i.e., R-R interval) sequence from each of them, and we developed a new information theoretic key agreement protocol that exploits the inherent randomness of ECG to ensure authentication between sensor pairs within the WBAN. After proper pre-processing, we provide an analytical solution that ensures robust authentication; we provide a unique information reconciliation matrix, which gives good performance for all ECG sensor pairs; and we can show that a relationship between information reconciliation and privacy amplification matrices can be found. Finally, we show the trade-off between the level of security, in terms of key generation rate, and the complexity of the error correction scheme implemented in the system.
△ Less
Submitted 14 May, 2021;
originally announced May 2021.
-
A Subatomic Proof System for Decision Trees
Authors:
Chris Barrett,
Alessio Guglielmi
Abstract:
We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is proof-theoretical naturalness: the system consists of all and only the inference rules generated by the single, simple, linear scheme of the recently introduced subatomic logic…
▽ More
We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is proof-theoretical naturalness: the system consists of all and only the inference rules generated by the single, simple, linear scheme of the recently introduced subatomic logic. Thanks to this regularity, cuts are eliminated via a natural construction. The second reason is that the system generates efficient proofs. Indeed, we show that a certain class of tautologies due to Statman, which cannot have better than exponential cut-free proofs in the sequent calculus, have polynomial cut-free proofs in our system. We achieve this by using the same construction that we use for cut elimination. In summary, by expanding the language of propositional logic, we make its proof theory more regular and generate more proofs, some of which are very efficient.
That design is made possible by considering atoms as superpositions of their truth values, which are connected by self-dual, non-commutative connectives. A proof can then be projected via each atom into two proofs, one for each truth value, without a need for cuts. Those projections are semantically natural and are at the heart of the constructions in this paper. To accommodate self-dual non-commutativity, we compose proofs in deep inference.
△ Less
Submitted 30 June, 2022; v1 submitted 4 May, 2021;
originally announced May 2021.
-
Feature selection for gesture recognition in Internet-of-Things for healthcare
Authors:
Giulia Cisotto,
Martina Capuzzo,
Anna V. Guglielmi,
Andrea Zanella
Abstract:
Internet of Things is rapidly spreading across several fields, including healthcare, posing relevant questions related to communication capabilities, energy efficiency and sensors unobtrusiveness. Particularly, in the context of recognition of gestures, e.g., grasping of different objects, brain and muscular activity could be simultaneously recorded via EEG and EMG, respectively, and analyzed to i…
▽ More
Internet of Things is rapidly spreading across several fields, including healthcare, posing relevant questions related to communication capabilities, energy efficiency and sensors unobtrusiveness. Particularly, in the context of recognition of gestures, e.g., grasping of different objects, brain and muscular activity could be simultaneously recorded via EEG and EMG, respectively, and analyzed to identify the gesture that is being accomplished, and the quality of its performance. This paper proposes a new algorithm that aims (i) to robustly extract the most relevant features to classify different grasping tasks, and (ii) to retain the natural meaning of the selected features. This, in turn, gives the opportunity to simplify the recording setup to minimize the data traffic over the communication network, including Internet, and provide physiologically significant features for medical interpretation. The algorithm robustness is ensured both by consensus clustering as a feature selection strategy, and by nested cross-validation scheme to evaluate its classification performance.
△ Less
Submitted 22 May, 2020;
originally announced May 2020.
-
Subatomic Proof Systems: Splittable Systems
Authors:
Andrea Aler Tubella,
Alessio Guglielmi
Abstract:
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 elimination. By considering atoms as self-dual non-commutative 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 v…
▽ More
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 elimination. By considering atoms as self-dual non-commutative 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 normalisation and cut elimination by way of a general theorem. In this paper we define and consider splittable systems, which essentially comprise a large class of linear logics, including MLL and BV, and we prove for them a splitting theorem, guaranteeing cut elimination and other admissibility results as corollaries. In papers to follow, we will extend this result to non-linear 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.
△ Less
Submitted 4 December, 2017; v1 submitted 29 March, 2017;
originally announced March 2017.
-
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Authors:
Paola Bruscoli,
Alessio Guglielmi,
Tom Gundersen,
Michel Parigot
Abstract:
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 Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek's result: we give a quasipolynomial-ti…
▽ More
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 Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek's result: we give a quasipolynomial-time cut-elimination procedure for classical propositional logic in deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they only trace structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.
△ Less
Submitted 2 May, 2016; v1 submitted 31 March, 2009;
originally announced March 2009.
-
A System of Interaction and Structure IV: The Exponentials and Decomposition
Authors:
Lutz Strassburger,
Alessio Guglielmi
Abstract:
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 the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper…
▽ More
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 the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.
△ Less
Submitted 27 July, 2010; v1 submitted 30 March, 2009;
originally announced March 2009.
-
Normalisation Control in Deep Inference via Atomic Flows
Authors:
Alessio Guglielmi,
Tom Gundersen
Abstract:
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 flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in d…
▽ More
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 flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.
△ Less
Submitted 31 March, 2008; v1 submitted 8 September, 2007;
originally announced September 2007.
-
On the Proof Complexity of Deep Inference
Authors:
Paola Bruscoli,
Alessio Guglielmi
Abstract:
We obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; 2) there are analytic deep-inference proof systems that exhibit an exponential speed-up over analytic Gentzen proof systems that they polynomially simulate.
We obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; 2) there are analytic deep-inference proof systems that exhibit an exponential speed-up over analytic Gentzen proof systems that they polynomially simulate.
△ Less
Submitted 19 April, 2009; v1 submitted 8 September, 2007;
originally announced September 2007.
-
On Structuring Proof Search for First Order Linear Logic
Authors:
Paola Bruscoli,
Alessio Guglielmi
Abstract:
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 search as computation' paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for line…
▽ More
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 search as computation' paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.
△ Less
Submitted 1 December, 2003;
originally announced December 2003.
-
A System of Interaction and Structure
Authors:
Alessio Guglielmi
Abstract:
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 challenging for the sequent calculus, and so far it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulae…
▽ More
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 challenging for the sequent calculus, and so far it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulae submitted to certain equational laws typical of sequents. The calculus of structures is obtained by generalising the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allow the design of BV, yield a modular proof of cut elimination.
△ Less
Submitted 27 January, 2007; v1 submitted 28 October, 1999;
originally announced October 1999.
