Sökning: onr:"swepub:oai:gup.ub.gu.se/310231" >
On model-theoretic ...
On model-theoretic strong normalization for truth-table natural deduction
-
- Abel, Andreas, 1974 (författare)
- 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
- Engelska.
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - Schloss Dagstuhl : Leibniz Zentrum für Informatik. - 1868-8969.
- Relaterad länk:
-
https://gup.ub.gu.se...
-
visa fler...
-
https://doi.org/10.4...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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 βπ.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Natural deduction
- Permutative conversion
- Reducibility
- Strong normalization
- Truth table
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas