CERES in higher-order logic

Annals of Pure and Applied Logic 162 (12):1001-1034 (2011)
  Copy   BIBTEX


We define a generalization of the first-order cut-elimination method CERES to higher-order logic. At the core of lies the computation of an set of sequents from a proof π of a sequent S. A refutation of in a higher-order resolution calculus can be used to transform cut-free parts of π into a cut-free proof of S. An example illustrates the method and shows that can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.



    Upload a copy of this work     Papers currently archived: 91,139

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

89 (#184,016)

6 months
11 (#187,035)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Ceres in intuitionistic logic.David Cerna, Alexander Leitsch, Giselle Reis & Simon Wolfsteiner - 2017 - Annals of Pure and Applied Logic 168 (10):1783-1836.

Add more citations

References found in this work

A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
Untersuchungen über das logische Schließen. I.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 35:176–210.
Untersuchungen über das logische Schließen. II.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 39:405–431.
Resolution in type theory.Peter B. Andrews - 1971 - Journal of Symbolic Logic 36 (3):414-432.
Intensional models for the theory of types.Reinhard Muskens - 2007 - Journal of Symbolic Logic 72 (1):98-118.

View all 8 references / Add more references