{"id":"arxiv/2607.29193","url":"https://arxiv.org/abs/2607.29193","tags":["math.LO"],"score":0,"title":"Proof theory for sequent-style tableaux: G0- and G3-style sequent calculi and full normalization","domain":"math.LO","source":"arxiv","authors":["Simone Cuconato"],"reviews":0,"subject":"math.LO","summary":"Sequent-style tableaux are a one-sided refutation calculus for classical propositional logic, in which each node of the refutation tree carries a finite block of formulae and the structural rules are absorbed into the data structure and the closure criterion. Building on the correspondence between this block calculus and the cut-free sequent calculus, and following the programme of Kamide and Negri, we recast the calculus as a structural-rule-free G3-style sequent calculus $\\mathbf{G}_t$ with shared contexts, and we introduce a G0-style sequent calculus $\\mathbf{G}_0$ with independent…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-31","reactions":{}}