3 papers
math.LO2026
Sequent-style tableaux for intuitionistic propositional logic
Simone Cuconato
Sequent-style tableaux are a refutation calculus in which each node of the refutation tree carries a finite block of formulae and the structural rules are absorbed into the data st…
math.LO2026
Proof theory for sequent-style tableaux: G0- and G3-style sequent calculi and full normalization
Simone Cuconato
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 s…
math.LO2026
Sequent-style tableaux for first-order logic: structural analysis, cut admissibility, and the correspondence with LK
Simone Cuconato
We give a self-contained development of the first-order block calculus in unsigned sequent-style notation: each node of the refutation tree carries a finite block $Π= Γ\cup \neg[Δ]…