CERES in higher-order logic (Q716500): Difference between revisions

Cut-elimination by resolution (CERES) for first-order logic [\textit{M. Baaz} et al., Lect. Notes Comput. Sci. 3452, 481--495 (2005; Zbl 1108.03305)] transforms the set of cut-formulas in a given proof \(\pi\) into a refutable formula \(R\). Given a resolution refutation of \(R\), cuts are sufficiently easily eliminated from \(\pi\). The extension \({\mathrm {CERES}}^\omega\) to higher-order logic described in the present paper is much more complicated. In particular, Skolemization involved in the first-order CERES is replaced here by a complicated mechanism of labels for quantifier rules in higher-order derivation, and a resolution calculus \(\mathcal{R}_{\mathrm{al}}\) used here is different from ordinary resolution \(\mathcal{R}\) for type theory [\textit{P. B. Andrews}, Stud. Log., Lond. 17, 63--81 (2008; Zbl 1226.03011)]. Completeness of \(\mathcal{R}_{\mathrm{al}}\) is conjectured, but not proved.