Expansion trees with cut. (September 2019)
- Record Type:
- Journal Article
- Title:
- Expansion trees with cut. (September 2019)
- Main Title:
- Expansion trees with cut
- Authors:
- Aschieri, Federico
Hetzl, Stefan
Weller, Daniel - Abstract:
- Abstract: Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logics by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller's expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas. In this paper, we present a new syntactic approach that directly extends Miller's expansion trees by cuts and also covers non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and shows that it is weakly normalizing.
- Is Part Of:
- Mathematical structures in computer science. Volume 29:Number 8(2019)
- Journal:
- Mathematical structures in computer science
- Issue:
- Volume 29:Number 8(2019)
- Issue Display:
- Volume 29, Issue 8 (2019)
- Year:
- 2019
- Volume:
- 29
- Issue:
- 8
- Issue Sort Value:
- 2019-0029-0008-0000
- Page Start:
- 1009
- Page End:
- 1029
- Publication Date:
- 2019-09
- Subjects:
- Proof theory, -- cut-elimination, -- Herbrand's theorem, -- expansion trees
Computer science -- Mathematics -- Periodicals
004.015105 - Journal URLs:
- http://journals.cambridge.org/action/displayJournal?jid=MSC ↗
- DOI:
- 10.1017/S0960129519000069 ↗
- Languages:
- English
- ISSNs:
- 0960-1295
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library HMNTS - ELD Digital store
- Ingest File:
- 11845.xml