Flavio Previale

Contraction Elimination in Sequent Based Ground Equational Calculus

2015 · arXiv (Cornell University)

In "Cut Elimination for Gentzen's Sequent Calculus with Equality and Logic of Partial Terms" LNCS 7750,161-172(2013), we have shown that the cut rule is eliminable in two ground equational sequent calculi, to be denoted by …

Absorbing the structural rules in the sequent calculus with additional atomic rules

2019 · Institutional Research Information System (University of Udine)

We show that if the structural rules are admissible over a set $$\mathcal{R}$$ of atomic rules, then they are admissible in the sequent calculus obtained by adding the rules in $$\mathcal{R}$$ to the multisuccedent minimal …