Reducing redundancy in cut-elimination by resolution
Bruno Woltzenlogel Paleo · Journal of Logic and Computation · 2014
Abstract. CERes is a method of cut-elimination that uses resolution proof search to avoid some kinds of redundancies that affect reductive cut-elimination methods. This paper shows that, unfortunately, there are also cases where CERes can produce proofs that are more redundant and even exponentially larger than the proofs produced by reductive cut-elimination methods. The paper then describes a few novel variants of CERes that are much less susceptible to these redundancies.