Projects per year
Abstract
We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunctiondisjunctionnegation and binary decision trees. We give two reasons to do so. The first is prooftheoretical 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 cutfree proofs in the sequent calculus, have polynomial cutfree 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 selfdual, noncommutative 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 selfdual noncommutativity, we compose proofs in deep inference.
That design is made possible by considering atoms as superpositions of their truth values, which are connected by selfdual, noncommutative 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 selfdual noncommutativity, we compose proofs in deep inference.
Original language  English 

Article number  26 
Pages (fromto)  125 
Journal  ACM Transactions on Computational Logic 
Volume  23 
Issue number  4 
Early online date  28 Jun 2022 
DOIs  
Publication status  Published  31 Oct 2022 
Fingerprint
Dive into the research topics of 'A Subatomic Proof System for Decision Trees'. Together they form a unique fingerprint.Projects
 1 Finished

Efficient and Natural Proof Systems
Guglielmi, A., Bruscoli, P. & McCusker, G.
Engineering and Physical Sciences Research Council
1/02/13 → 12/05/16
Project: Research council