CERES in higher-order logic

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

Abstract

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.

Links

PhilArchive



    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

Analytics

Added to PP
2013-10-27

Downloads
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