DUŽÍ, Marie, Marek MENŠÍK, Miroslav PAJR and Vojtěch PATSCHKA. Natural deduction system in the TIL-script language. Online. In Endrjukaite, T., Jaakkola, H., Dudko, A., Kiyoki, Y., Thalheim, B., Yoshida, N. Frontiers in Artificial Intelligence and Applications. 312th ed. Amsterdam: IOS Press, 2019, p. 237-255. ISBN 978-1-61499-933-1. Available from: https://dx.doi.org/10.3233/978-1-61499-933-1-237.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Natural deduction system in the TIL-script language
Authors DUŽÍ, Marie (guarantor), Marek MENŠÍK (203 Czech Republic), Miroslav PAJR (203 Czech Republic, belonging to the institution) and Vojtěch PATSCHKA.
Edition 312. vyd. Amsterdam, Frontiers in Artificial Intelligence and Applications, p. 237-255, 19 pp. 2019.
Publisher IOS Press
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW URL
RIV identification code RIV/47813059:19240/19:A0000458
Organization unit Faculty of Philosophy and Science in Opava
ISBN 978-1-61499-933-1
ISSN 0922-6389
Doi http://dx.doi.org/10.3233/978-1-61499-933-1-237
Keywords in English Beta-conversion; Funcional application; Hyperintesionality; Natural deduction; Three kinds of context; TIL; TIL-Script
Tags ÚI
Tags International impact, Reviewed
Changed by Changed by: Mgr. Kamil Matula, Ph.D., učo 7389. Changed: 2/3/2020 09:20.
Abstract
In this paper we deal with the extension of the functionalities of the TIL-Script language, namely the proof system based on natural deduction. The system processes a subset of the set of TIL-Script constructions that are typed to v-construct a truth-value. Since TIL-Script is a functional programming language based on a hyperintensional lambda calculus with procedural semantics, we also describe the way how to validly apply beta conversion and how to operate in a hyperintensional context where the very procedure is an object of predication.
PrintDisplayed: 2/5/2024 23:21