Natural Deduction System in the TIL-Script Language
D Marie, Men scaron iacute k Marek, Pajr Miroslav, Patschka Vojt ecaron ch · Frontiers in artificial intelligence and applications · 2019
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.