We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: A Subatomic Proof System for Decision Trees

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 shape 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 propositional variables as superpositions of their truth values, which are connected by self-dual, non-commutative connectives. A proof can then be projected via each propositional variable into two proofs, one for each truth value, without a need for cuts. Those projections are semantically natural and are at the heart of all the constructions in this paper. To accommodate self-dual non-commutativity, we compose proofs by deep inference.
Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)
Cite as: arXiv:2105.01382 [cs.LO]
  (or arXiv:2105.01382v1 [cs.LO] for this version)

Submission history

From: Chris Barrett [view email]
[v1] Tue, 4 May 2021 09:23:07 GMT (44kb)

Link back to: arXiv, form interface, contact.