Contraction Elimination in Sequent Based Ground Equational Calculus
Logic
2016-01-01 v1
Abstract
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 EQ_M and EQ'. In this note we prove that the contraction rule is not eliminable in EQ_M but it is eliminable in EQ'.
Cite
@article{arxiv.1512.09171,
title = {Contraction Elimination in Sequent Based Ground Equational Calculus},
author = {F. Parlamento and F. Previale},
journal= {arXiv preprint arXiv:1512.09171},
year = {2016}
}
Comments
7 pages