Search: onr:"swepub:oai:gup.ub.gu.se/310231" >
On model-theoretic ...
On model-theoretic strong normalization for truth-table natural deduction
-
- Abel, Andreas, 1974 (author)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap (GU),Department of Computer Science and Engineering, Computing Science (GU)
-
(creator_code:org_t)
- Schloss Dagstuhl : Leibniz Zentrum für Informatik, 2021
- 2021
- English.
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - Schloss Dagstuhl : Leibniz Zentrum für Informatik. - 1868-8969.
- Related links:
-
https://gup.ub.gu.se...
-
show more...
-
https://doi.org/10.4...
-
show less...
Abstract
Subject headings
Close
- Intuitionistic truth table natural deduction (ITTND) by Geuvers and Hurkens (2017), which is inherently non-confluent, has been shown strongly normalizing (SN) using continuation-passing-style translations to parallel lambda calculus by Geuvers, van der Giessen, and Hurkens (2019). We investigate the applicability of standard model-theoretic proof techniques and show (1) SN of detour reduction (β) using Girard's reducibility candidates, and (2) SN of detour and permutation reduction (βπ) using biorthogonals. In the appendix, we adapt Tait's method of saturated sets to β, clarifying the original proof of 2017, and extend it to βπ.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Natural deduction
- Permutative conversion
- Reducibility
- Strong normalization
- Truth table
Publication and Content Type
- ref (subject category)
- kon (subject category)
Find in a library
To the university's database