Type Checking Algorithm for the TIL-Script Language

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F19%3A10241521" target="_blank" >RIV/61989100:27240/19:10241521 - isvavai.cz</a>

Výsledek na webu

<a href="http://ebooks.iospress.nl/volumearticle/50914" target="_blank" >http://ebooks.iospress.nl/volumearticle/50914</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.3233/978-1-61499-933-1-219" target="_blank" >10.3233/978-1-61499-933-1-219</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Type Checking Algorithm for the TIL-Script Language

Popis výsledku v původním jazyce

The success of automated reasoning techniques over large natural-language texts heavily relies on a fine-grained analysis of natural language assumptions. While there is a common agreement that the analysis should be hyperintensional, most of the automatic reasoning systems are still based on an intensional logic, at the best. In this paper we introduce the TIL-Script language, which is a computational variant of Pavel Tichý&apos;s Transparent Intensional Logic (TIL). TIL is a hyperintensional, typed lambda calculus of partial functions. Hyperintensional, because the TIL terms are interpreted as denoting procedures rather than their products, which are partial functions-in-extension. Thus, in our stratified ontology we have got procedures, their products, i.e. functions-in-extensions, or even procedures of a lower order, as well as functional values. These procedures are rigorously defined as TIL constructions. With constructions of constructions, constructions of functions, functions, and functional values in our stratified ontology, we need to keep track of the traffic between multiple logical strata. The ramified type hierarchy does just that. The type of first order objects includes all objects that are not constructions. The type of second-order objects includes constructions of first-order objects. The type of third-order objects includes constructions of first- or second-order objects. And so on, ad infinitum. The goal of this paper is to introduce the algorithm of type control over the results of logical analysis of natural-language expressions, i.e., checking whether the analysis results in a type-theoretically coherent procedure assigned to the expression as its meaning.

Název v anglickém jazyce

Type Checking Algorithm for the TIL-Script Language

Popis výsledku anglicky

The success of automated reasoning techniques over large natural-language texts heavily relies on a fine-grained analysis of natural language assumptions. While there is a common agreement that the analysis should be hyperintensional, most of the automatic reasoning systems are still based on an intensional logic, at the best. In this paper we introduce the TIL-Script language, which is a computational variant of Pavel Tichý&apos;s Transparent Intensional Logic (TIL). TIL is a hyperintensional, typed lambda calculus of partial functions. Hyperintensional, because the TIL terms are interpreted as denoting procedures rather than their products, which are partial functions-in-extension. Thus, in our stratified ontology we have got procedures, their products, i.e. functions-in-extensions, or even procedures of a lower order, as well as functional values. These procedures are rigorously defined as TIL constructions. With constructions of constructions, constructions of functions, functions, and functional values in our stratified ontology, we need to keep track of the traffic between multiple logical strata. The ramified type hierarchy does just that. The type of first order objects includes all objects that are not constructions. The type of second-order objects includes constructions of first-order objects. The type of third-order objects includes constructions of first- or second-order objects. And so on, ad infinitum. The goal of this paper is to introduce the algorithm of type control over the results of logical analysis of natural-language expressions, i.e., checking whether the analysis results in a type-theoretically coherent procedure assigned to the expression as its meaning.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA18-23891S" target="_blank" >GA18-23891S: Hyperintensionální usuzování nad texty přirozeného jazyka</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2019

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ů

Název statě ve sborníku

Frontiers in Artificial Intelligence and Applications. Volume 312

ISBN

978-1-61499-932-4

ISSN

0922-6389

e-ISSN

1535-6698

Počet stran výsledku

18

Strana od-do

219-236

Název nakladatele

IOS Press

Místo vydání

Amsterdam

Místo konání akce

Riga

Datum konání akce

4. 6. 2018

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—