D 2017

Existential generalization in TIL

MENŠÍK, Marek, Jakub KERMASCHEK a Luděk CIENCIALA

Základní údaje

Originální název

Existential generalization in TIL

Autoři

MENŠÍK, Marek (203 Česká republika, garant, domácí), Jakub KERMASCHEK (203 Česká republika) a Luděk CIENCIALA (203 Česká republika, domácí)

Vydání

Volume 17. Sofia, International Multidisciplinary Scientific GeoConference Surveying Geology and Mining Ecology Management, SGEM, od s. 311-318, 8 s. 2017

Nakladatel

International Multidisciplinary Scientific Geoconference

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Bulharsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Kód RIV

RIV/47813059:19240/17:A0000111

Organizační jednotka

Filozoficko-přírodovědecká fakulta v Opavě

ISBN

978-619-7408-01-0

ISSN

DOI

http://dx.doi.org/10.5593/sgem2017/21/S07.040

Klíčová slova anglicky

Deduction; Existential Generalization; Extension; Hyperintension; Intension; Logic; TIL

Štítky

ÚI

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 28. 3. 2018 14:15, Mgr. Kamil Matula, Ph.D.

Anotace

V originále

The paper deals with the fundamental rule of extensional logics, namely the rule of Existential Generalization. This rule can be applied in the situation when a function f is applied on its argument a to obtain the value of f at a. If the application does not fail, i.e., if the function f is defined at a, then we can existentially quantify, and derive that there is the value f(a). Our system is based on Transparent Intensional Logic (TIL). Since TIL is a hyperintensional, partial, typed lambda calculus, we examine the validity of the rule in TIL, or rather in its computational variant the TIL-Script language. The rule is context sensitive in the sense that depending on a context we should recognize the type of entity to be abstracted over. This is not to say that the rule can be invalid dependently on context; the rule is valid universally. Only that the type of the argument over which we quantity depends on the context. There are three kinds of contexts to be distinguished, namely extensional, intensional and hyperintensonal. We introduce the definition of these three kinds of context and an algorithm that recognizes in which context a particular construction occurs so that the Existential Generalization can be validly applied. The tool navigates users through the correct application of the deduction rules.
Zobrazeno: 27. 12. 2024 14:44