Type Checking Algorithm for the TIL-Script Language
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Type Checking Algorithm for the TIL-Script Language
Original language description
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ý'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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA18-23891S" target="_blank" >GA18-23891S: Hyperintensional Reasoning over Natural Language Texts</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Frontiers in Artificial Intelligence and Applications. Volume 312
ISBN
978-1-61499-932-4
ISSN
0922-6389
e-ISSN
1535-6698
Number of pages
18
Pages from-to
219-236
Publisher name
IOS Press
Place of publication
Amsterdam
Event location
Riga
Event date
Jun 4, 2018
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—