Title: CERES in higher-order logic
Authors: Hetzl, Stefan 
Leitsch, Alexander 
Weller, Daniel 
Category: Original Research Article
Issue Date: 2011
Journal: Annals of Pure and Applied Logic 
ISSN: 0168-0072
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 (unsatisfiable) set of sequents (the characteristic sequent set) from a proof of a sequent . A refutation of in a higher-order resolution calculus can be used to transform cut-free parts of (the proof projections) into a cut-free proof of . An example illustrates the method and shows that can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.
Keywords: cut-elimination; resolution; higher-order logic
DOI: 10.1016/j.apal.2011.06.005
Organisation: E104 - Institut für Diskrete Mathematik und Geometrie 
License: CC BY-NC-ND 4.0 CC BY-NC-ND 4.0
Publication Type: Article
Appears in Collections:Article

Files in this item:

File Description SizeFormat
Hetzl - 2011 - CERES in higher-order logic.pdf476.16 kBAdobe PDFThumbnail
Show full item record

Page view(s)

checked on Jun 17, 2021


checked on Jun 17, 2021

Google ScholarTM


This item is licensed under a Creative Commons License Creative Commons