All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

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ý&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.

  • 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