Type-Theoretical Approaches to Problems and Solutions

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F15%3A00083750" target="_blank" >RIV/00216224:14210/15:00083750 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Type-Theoretical Approaches to Problems and Solutions

Popis výsledku v původním jazyce

We examine two possible approaches to the formal treatment of the notion of problem in the type-theoretical paradigm. More specifically, we will explore an approach put forward by Martin-Löf's Constructive Type Theory (abbr. CTT, based on BHK interpretation of intuitionistic logic and Curry-Howard-de Bruijn correspondence), which can be seen as a direct continuation of Kolmogorov's original calculus of problems, and an approach put forward by Materna utilizing Tichý's Transparent Intensional Logic (abbr. TIL, based on partial lambda calculus and ramified classical type theory), which can be viewed as a realist attempt of interpreting Kolmogorov's logic of problems. Thus both of these theories can be seen as building upon Kolmogorov's first key insightthat (constructive) logic is better understood as dealing with problems rather than with propositions. We conclude that neither of these theories can be considered at their current state as providing satisfactory account of the notion of

Název v anglickém jazyce

Type-Theoretical Approaches to Problems and Solutions

Popis výsledku anglicky

We examine two possible approaches to the formal treatment of the notion of problem in the type-theoretical paradigm. More specifically, we will explore an approach put forward by Martin-Löf's Constructive Type Theory (abbr. CTT, based on BHK interpretation of intuitionistic logic and Curry-Howard-de Bruijn correspondence), which can be seen as a direct continuation of Kolmogorov's original calculus of problems, and an approach put forward by Materna utilizing Tichý's Transparent Intensional Logic (abbr. TIL, based on partial lambda calculus and ramified classical type theory), which can be viewed as a realist attempt of interpreting Kolmogorov's logic of problems. Thus both of these theories can be seen as building upon Kolmogorov's first key insightthat (constructive) logic is better understood as dealing with problems rather than with propositions. We conclude that neither of these theories can be considered at their current state as providing satisfactory account of the notion of

Druh

O - Ostatní výsledky

CEP obor

AA - Filosofie a náboženství

OECD FORD obor

—

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů