–
Room P3.10, Mathematics Building
João Rasga, Instituto Superior Técnico
Sufficient conditions for cut elimination in first order based calculi
Sufficient conditions for a sequent calculus to enjoy cut elimination are established for a wide class of first order based logics. The conditions result from the application of traditional cut elimination proof techniques to an arbitrary calculus composed by rules that must satisfy a number of reasonable conditions. Based on the cut elimination theorem, the subformula property and the consistency of these calculi are established.