The goal of this paper is to implement the Transparent Intensional Logic framework in the Haskell programming language, based on the procedural, i.e., constructive nature of this logical system. The main benefits of this implementation include type checking of constructions for free and the possibility of using predefined functions of Haskell, which allows focusing solely on the essence of this work, namely, the transformation of various constructions of Transparent Intensional Logic into Haskell terms.

The main goal of this paper is to propose a formalism for type checking constructions of Transparent Intensional Logic capable of detecting the widest possible range of type-theoretical incoherence. To achieve this goal, however, a slight modification to the type system of Transparent Intensional Logic is necessary, specifically in the specification of higher-order types. This adjustment brings its type system closer to the type systems of standard programming languages within the functional paradigm, thereby increasing the practical implementation potential of Transparent Intensional Logic, which has so far been primarily utilized as a syntactic standard.

Though there is a huge amount of the so-called epistemic logics that deal with propositional attitudes, i.e., sentences of the form “a knows that P”, their ‘wh-cousins’ of the form “a knows who is a P”, “a knows what the P is”, “a knows which Ps are Qs”, etc., have been, to the best of my knowledge, almost neglected. A similar disproportion can be observed between the analysis of Yes-No questions, which has been under scrutiny of many erotetic logics, and Wh-questions which have been dealt with just by a few authors. To fill this gap, we have analysed Wh-questions in Transparent Intensional Logic (TIL) and adjusted Gentzen’s system of natural deduction to TIL natural language processing; thus, our TIL question-answering system can answer not only Yes-No questions but also derive answers to Wh-questions. In this paper, I am going to apply these results to the analysis of sentences containing a ‘knowing-wh’ constituent. In addition, I will analyse the relation between ‘knowing-that’ and ‘knowing-wh’. For instance, if a knows that the Mayor of Ostrava is Mr Macura, can we logically derive that a knows who is the Mayor of Ostrava? Or, vice versa, if a knows who is the Mayor of Ostrava and the Mayor of Ostrava is Mr Macura, do these assumptions logically entail that a knows that the Mayor of Ostrava is Mr Macura? Though in case of rational human agents the answers seem to be a no-doubt YES, perhaps a rather surprising answer is in general negative. We have to specify rules for deriving the relation between knowing-that and knowing-wh, and if a software agent is rational but resource bounded, it does not have to have in its ontology the rules necessary to derive the answer. The goal of the paper is the specification of these rules. Hence, when applying these results into the design of a multi-agent system composed of software resource-bounded agents, we have to compute their inferable knowledge, which accounts not only for their explicit knowledge but also for their inferential abilities.

In this paper, we deal with the support in the search for appropriate textual sources. Users ask for an atomic concept that is explicated using machine learning methods applied to different textual sources. Next, we deal with the so-obtained explications to provide even more useful information. To this end, we apply the method of computing association rules. The method is one of the data-mining methods used for information retrieval. Our background theory is the system of Transparent Intensional Logic (TIL); all the concepts are formalised as TIL constructions.

Humankind faces a most crucial mission; we must endeavour, on a global scale, to restore and improve our natural and social environments. This is a big challenge for global information systems development and for their modelling. In this paper, we discuss on different aspects of conceptual modelling in global environmental context. The paper is the summary of the panel session “The Future of Conceptual Modelling” in the 29th International Conference on Information Modelling and Knowledge Bases.

In this paper we deal with machine learning methods and algorithms applied to the area of geographic data. First, we briefly introduce learning with a supervisor that is applied in our case. Then we describe the algorithm 'Framework' together with heuristic methods used in it. Definitions of particular geographic objects, i.e. their concepts, are formulated in our background theory Transparent Intensional Logic (TIL) as TIL constructions. These concepts serve as general hypotheses. Basic principles of supervised machine learning are generalization and specialization. Given a positive example, the learner generalizes, while after a near-miss example specialization is applied. Heuristic methods deal with the way generalization and specialization are applied.

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.

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.

A method for computing the complete meaning of sentences with anaphoric reference is presented, that is, the method for implementing the substitution of an appropriate antecedent to accompany the anaphoric reference. Our method is similar to the one applied in general by Hans Kamp's Discourse Representation Theory (DRT). ‘DRT’ is an umbrella term for a collection of logical and computational linguistic methods developed for a dynamic interpretation of natural language, where each sentence is interpreted within a certain discourse, which is a sequence of sentences uttered by a group of speakers. Interpretation conditions are given via instructions for updating the discourse representation. Yet these methods are mostly based on first-order logics. Thus, only expressions denoting individuals (indefinite or definite noun phrases) can introduce so-called discourse referents, which are free variables that are updated when interpreting the discourse. Our background theory is Pavel Tichý's Transparent Intensional Logic with its procedural rather than set-theoretic model semantics. Since our semantics is procedural, hence hyperintensional and higher-order, not only individuals, but entities of any type, like properties of individuals, propositions and hyperpropositions, relations-in-intension, and even constructions (i.e., meanings of antecedent expressions), can be linked to anaphoric variables. Moreover, the thoroughgoing typing of the universe of TIL makes it possible to determine the respective type-theoretically appropriate antecedent, which is one of the novel contributions of this paper. The second novelty is the specification of the algorithm for dynamic discourse representation within TIL.

The paper deals with the fundamental computational rule of functional programming languages, namely the rule of beta conversion. This rule specifies the way in which a function f is applied to its argument a. There are two possible ways of executing the conversion, to wit ‘by name’ and ‘by value’. It has been proved that these two ways are not operationally equivalent, and, which is worse, the execution by name is not a denotationally equivalent transformation in the logic of partial functions. Since Transparent Intensional Logic (TIL) is a partial, typed lambda calculus, we examine the validity of the rule in TIL, or rather in its computational variant the TIL-Script language. We show that there are contexts in which the rule by name can be validly applied. The main result is the specification of such contexts, and comparison with the reduction by value. To this end, we present a tool that recognizes a context in which a formal parameter of a given calling procedure occurs and interactively navigates the user to a correct way of reduction. In case of an invalid way the program informs the user about the problem and warns against undesirable side effects. As a result, the program proposes to execute the rule by value.

Intensional epistemic logics are not apt for handling properly the specification of communication and reasoning of resource-bounded agents in a multi-agent system. They oscillate between two unrealistic extremes: either the explicit knowledge of an ‘idiot’ agent, deprived of any inferential capabilities, or the implicit knowledge of an agent who is a logical/mathematical genius. The goal of this paper is to introduce the notion of inferable knowledge of a rational yet resource-bounded agent. The stock of inferable knowledge of such an agent a is the closure of a chain-of-knowledge sequence validly derivable from a's existing stock of explicit knowledge via one or more rules of inference that a masters. We are using Pavel Tichý's Transparent Intensional Logic as our framework. This logic models knowing as a relation-in-intension between an agent and a construction (a hyperintensional mode of presentation of a possible-world proposition) rather than a set of possible worlds or a piece of syntax. We motivate the restriction of the epistemic closure principle to inferable knowledge, present the theoretical framework, define the concept of inferable knowledge, and explain the technicalities of the so restricted closure principle.

In this paper we introduce the Learning Management System (LMS) eLogika that has been developed in our department for teaching mathematical logic. There were many reasons that led us to the decision to develop such a system, including inter alia a great amount of students enrolled for the courses on logic. Yet the most important reason was a specific character of logic education. As a result, the eLogika system is a web application that provides didactic material for courses on mathematical logic. Its main goal is an automatic test generation and computer-aided test evaluation based on a large database of logic tasks. The system makes it possible to adjust the level of particular tests according to students' knowledge level. To this end we developed a feedback module that makes use of statistics and data mining methods. The system can generate a large number of training as well as exam test variants for each common thematic topic. At the same time it provides effective semi-automatic methods of test rating and evaluation. In the paper we describe particular modules of eLogika with the focus on the modules of data mining and statistics.

In the last decades we got used to software applications (or computers, if you like) being everywhere and working for us. Yet sometimes they fail to work as desired. The current situation is often characterized as the second software crisis. There are many alleged causes of this state. They include, inter alia, web net overload, loss of data, inconsistency of data, intrusions by hackers, etc. etc. Yet in our opinion, the main problem is an old one. It consists in an insufficient specification of the procedures to be executed. We have been dealing with this problem since the beginning of computer era. Though there are many specification methods and languages, the problem remains very much a live issue and so far no satisfactory solution has been found. Our stance is that a declarative logical specification is needed. A serious candidate for such a high-quality declarative specification is a higher-order logic equipped with a procedural semantics. The goal of our contribution is to describe a specification method using Transparent Intensional Logic (TIL). TIL is a hyperintensional, typed, partial lambda-calculus. Hyperintensional, because the meaning of TIL-terms are not the functions/mappings themselves; rather, they are procedures producing functions as their products. Proper typing makes it possible to define inputs and outputs of a procedure. Finally, we must take into account partiality and the possibility of a failure to produce a product. A procedure may fail to produce a correct product for one of two reasons. Either the mapping the procedure produces is undefined at the argument(s) serving as point(s) of evaluation, or the procedure is ill- or under-specified, in which case the empirical execution process has undesirable results. This paper investigates, in a logically rigorous manner, how a detailed specification can prevent these problems.

Visual information such as pictorial symbols, icons and images capture our imagination. In our paper, we discuss icons and images in the context of cross-cultural communication. The authors present their own viewpoints to the subject. We discuss about communication in the multi-cultural world and analyze icons in cross-cultural context. Two professional application domains for icons will be presented. A Kansei-based cross-cultural multimedia computing system and a cross-cultural image communication system are described. Icons are a good means for communication within a certain application domain and in a certain context.

Software products in companies are a substantial part of their production and a necessary condition of their business success. However, there is still a problem of software proper specification and verification. We propose a formal specification method for software processes based on Transparent Intensional Logic, TIL. This method is logic-oriented, because logical specification within a rich formal framework makes it possible to explicitly define process resources as well as process logic. Moreover, our novel contribution consists in integrating a knowledge-based method with process dynamic modeling.

We view the content of ontology via a logic of intensions. This is due to the fact that particular intensions like properties, roles, attributes and propositions can stand in mutual necessary relations which should be registered in the ontology of a given domain, unlike some contingent facts. The latter are a subject of updates and are stored in a knowledge-base state. Thus we examine (higher-order) properties of intensions like being necessarily reflexive, irreflexive, symmetric, anti-symmetric, transitive, etc., mutual relations between intensions like being incompatible, being a requisite, being complementary, and so like. We also define two kinds of entailment relation between propositions, viz. mere entailment and presupposition. Finally, we show that higher-order properties of propositions trigger necessary integrity constraints that should also be included in the ontology. As the logic of intensions we vote for Transparent Intensional Logic (TIL), because TIL framework is smoothly applicable to all three kinds of context, viz. extensional context of individuals, numbers and functions-in-extension (mappings), intensional context of properties, roles, attributes and propositions, and finally hyper-intensional context of procedures producing intensional and extensional entities as their products.

In the paper we propose a Brain Architecture which allows developers of a Multi-Agent System (MAS) to integrate various supporting tools. For the purpose of agents' communication and reasoning we make use of Transparent Intesional logic (TIL), or more exactly of its software variant the TIL-Script language. The proposed architecture makes it possible to utilise also the Prolog language as a reasoning tool. Rules and facts are stored in agent's internal knowledge base is designed in a way appropriate both for Prolog and TIL-Script languages. The architecture is an open one so that other tools of reasoning can be easily incorporated.

Multi-agent system is a system of autonomous, intelligent but resource-bounded agents. Particular agents have to be able to make decisions on their own, based on the activities of the other agents and events within the system as well as its environment. Thus the agents have to communicate and collaborate with each other as well as with their environment. They communicate by exchanging messages encoded in a near-to-natural language. Traditional first-order languages are not expressive enough to meet the demands of MAS communication. Therefore we make use of the powerful system of Transparent Intensional Logic (TIL). The paper introduces the software variant of TIL, namely the TIL-Script functional programming language. We describe its syntax and semantic, as well as the way the TIL-Script facilities are integrated into the whole multi-agent system.

This paper contains five contributions of the participants of the panel discussion on “Multi-agent Knowledge Modelling” in the EJC 2008 conference. We addressed four main topics: (a) Semantic Web technologies, (b) reality vs. agents, (c) cross-cultural knowledge and (d) communication of agents. Each of the discussants presented his/her view of the addressed problem. Some views were rather pessimistic, other optimistic or realistic, but all of them posed questions and raised open problems as well as solution proposals. Thus this paper is a contribution to the topic of multi-agent knowledge modelling from different points of view.

We introduce a new theory of concepts conceived as structured abstract entities. The theory is based on the key notion of Transparent Intensional Logic (TIL), known as TIL construction. The rich procedural semantics of TIL makes it possible to explicitly analyze all the semantically salient features of natural language expressions. We illustrate how to make use of TIL theory of concepts in distinguishing analytical and empirical concepts, and particular kinds of necessities. We also deal with a rigorous specification of requisite relations between intensions such as properties. Finally, ontology is characterised as a relatively stable part of the system that should play an integrating role. We show how to make use of TIL rich theory in specification of the content of ontologies in a multi-agent system.