Fundamenta Informaticae - Volume 165, issue 3-4

Authors: Penczek, Wojciech | Schlingloff, Holger | Wasilewski, Piotr

Article Type: Other

DOI: 10.3233/FI-2019-1781

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. i-iii, 2019

Authors: Fitting, Melvin

Article Type: Research Article

Abstract: Justification logic began with Sergei Artemov’s work providing an arithmetic semantics for intuitionistic logic. As part of that work, a small number of explicit modal logics were introduced—logics in which there was a structure of terms that kept track of not just what was a necessary truth, but why it was necessary. These explicit modal logics were connected with standard modal logics such as S4, T, K, and others using Realization Theorems, essentially saying that modal operators concealed an underlying informational structure. Since Artemov’s work, the phenomenon of justification logic has turned out to be very broad. For instance, I …have shown that infinitely many modal logics have justification counterparts. In this paper I will sketch the basics and try to give some of the ideas behind formal justification proofs, justification semantics, and realization theorems. Show more

Keywords: justification logic, modal logic, BHK semantics, intuitionistic logic, logic of proofs, realization

DOI: 10.3233/FI-2019-1782

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 193-203, 2019

Authors: De Angelis, Emanuele | Fioravanti, Fabio | Meo, Maria Chiara | Pettorossi, Alberto | Proietti, Maurizio

Article Type: Research Article

Abstract: We present an operational semantics for time-aware business processes, that is, processes modeling the execution of business activities, whose durations are subject to linear constraints over the integers. We assume that some of the durations are controllable, that is, they can be determined by the organization that executes the process, while others are uncontrollable, that is, they are determined by the external world. Then, we consider controllability properties, which guarantee the completion of the execution of the process, satisfying the given duration constraints, independently of the values of the uncontrollable durations. Controllability properties are encoded by quantified reachability formulas, …where the reachability predicate is recursively defined by means of constrained Horn clauses (CHCs). These clauses are automatically derived from the operational semantics of the process. Finally, we present two algorithms for solving the so called weak and strong controllability problems. Our algorithms reduce these problems to the verification of a set of quantified integer constraints, which are simpler than the original quantified reachability formulas, and can effectively be handled by state-of-the-art CHC solvers. Show more

DOI: 10.3233/FI-2019-1783

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 205-244, 2019

Authors: Aldilaijan, Abdulla | Azad, Mohammad | Moshkov, Mikhail

Article Type: Research Article

Abstract: In this paper, we present results of experimental studies related to the existence of totally optimal decision trees (which are optimal relative to two or more cost functions simultaneously) for nine decision tables from the UCI Machine Learning Repository. Such trees can be useful when we consider decision trees as algorithms for problem solving or as a way for knowledge representation. For cost functions, we use depth, average depth, and number of nodes. We study not only exact but also approximate decision trees based on five uncertainty measures: entropy, Gini index, misclassification error, relative misclassification error, and number of unordered …pairs of rows with different decisions. To investigate the existence of totally optimal trees, we use an extension of dynamic programming that allows us to make multi-stage optimization of decision trees relative to a sequence of cost functions. Experimental results show that totally optimal decision trees exist in many cases. The behavior of graphs that describe how the number of decision tables with totally optimal decision trees depends on their accuracy is mainly irregular. However, one can observe some trends, in particular, an upward trend when accuracy is decreasing. Show more

Keywords: decision tree, uncertainty measure, cost function, totally optimal decision tree, multi-stage optimization

DOI: 10.3233/FI-2019-1784

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 245-261, 2019

Authors: Bazan, Jan G. | Szczur, Adam | Skowron, Andrzej | Rzepko, Marian | Król, Paweł | Bajorek, Wojciech | Czarny, Wojciech

Article Type: Research Article

Abstract: A new method of decision tree construction from temporal data is proposed in the paper. This method uses the so-called temporal cuts for binary partition of data in tree nodes. The novelty of the proposed approach is that the quality of cuts is calculated not on the basis of the discernibility of objects (related to time points), but on the basis of the discernibility of time windows labeled with different decision classes. The paper includes results of experiments performed on our data sets and collections from machine learning repositories. In order to evaluate the presented method, we compared its performance …with the classification results of a local discretization decision tree, and other methods well known from literature. Our new method outperforms these known methods. Show more

Keywords: rough sets, discretization, classifiers, temporal cuts, temporal data

DOI: 10.3233/FI-2019-1785

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 263-281, 2019

Authors: Dutta, Soma | Jankowski, Andrzej | Rozenberg, Grzegorz | Skowron, Andrzej

Article Type: Research Article

Abstract: Reaction system is a model of interactive computations which was motivated by the functioning of the living cell. It is an idealized mathematical model, also because it abstracts from the complex nature of the physical systems where only partial, incomplete information is available (e.g ., about their states). The framework of rough sets was developed to deal with such incomplete information. In this paper we establish a connection between reaction systems and rough sets. This is done in a somewhat broader perspective of the relationship between “pure” mathematical models and “realistic models” that take into account the limitation of perceiving …physical reality. Show more

Keywords: rough set, reaction system, interactions of biochemical reactions, interactive computing, interactive granular computing, modeling of complex states, transition between complex states

DOI: 10.3233/FI-2019-1786

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 283-302, 2019

Authors: Gori, Roberta | Gruska, Damas | Milazzo, Paolo

Article Type: Research Article

Abstract: Reaction systems are a qualitative formalism for modeling systems of biochemical reactions. They describe the evolution of sets of objects representing biochemical molecules. One of the main characteristics of Reaction systems is the non-permanency of the objects, namely objects disappear if not produced by any enabled reaction. Reaction systems execute in an environment that provides new objects at each step. Causality properties of reaction systems can be studied by using notions of formula based predictor. In this context, we define a notion of opacity that can be used to study information flow properties for reaction systems. Objects will …be partitioned into high level (invisible) and low level (visible) ones. Opacity ensures that the presence (or absence) of high level objects cannot be guessed observing the low level objects only. Such a property is shown to be decidable and computable by exploiting the algorithms for minimal formula based predictors. Show more

DOI: 10.3233/FI-2019-1787

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 303-319, 2019

Authors: Niewiadomski, Artur | Switalski, Piotr | Sidoruk, Teofil | Penczek, Wojciech

Article Type: Research Article

Abstract: We present nine SAT-solvers and compare their efficiency for several decision and combinatorial problems: three classical NP-complete problems of the graph theory, bounded Post correspondence problem (BPCP), extended string correction problem (ESCP), two popular chess problems, PSPACE-complete verification of UML systems, and the Towers of Hanoi (ToH) of exponential solutions. In addition to several known reductions to SAT for the problems of graph k -colouring, vertex k -cover, Hamiltonian path, and verification of UML systems, we also define new original reductions for the N-queens problem, the knight’s tour problem, and ToH, SCP, and BPCP. Our extensive experimental results allow for …drawing quite interesting conclusions on efficiency and applicability of SAT-solvers to different problems: they behave quite efficiently for NP-complete and harder problems but they are by far inferior to tailored algorithms for specific problems of lower complexity. Show more

DOI: 10.3233/FI-2019-1788

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 321-344, 2019

Authors: Sawicka, Anna | Kacprzak, Magdalena | Zbrzezny, Andrzej

Article Type: Research Article

Abstract: We can understand a protocol as a set of rules used by the communicating entities i.e. people or computers. These rules specify allowed interactions between them. Every day people use protocols unconsciously during their conversations since they help to achieve the goal of the conversation (e.g. a compromise, a persuasion). In the paper, we focus on argumentative dialogues in which players can perform actions representing speech acts like claim , question , scold etc. Since we consider dialogues which have an emotional undertow we want to design a system for semantic verification of properties of dialogue games with emotional …reasoning. This framework is based on interpreted systems designed for a dialogue protocol in which participants have emotional skills. The GERDL language is used for a dialogue game specification. We present the idea of encoding rules describing the dialogue game given in this language. We want to verify some properties of dialogue games and we focus on the reachability property that can take into account emotions and commitments of players. Show more

Keywords: dialogue game, description language, dialogue protocol, emotions

DOI: 10.3233/FI-2019-1789

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 345-361, 2019

Authors: Wolski, Marcin | Gomolińska, Anna

Article Type: Research Article

Abstract: Pattern structures were introduced by Ganter and Kuznetsov in the framework of formal concept analysis (FCA) as a mean to direct analysis of objects having complex descriptions, e.g., descriptions presented in the form of graphs instead of a set of properties. Pattern structures actually generalise/replace the original FCA representation of the initial information about objects, that is, formal contexts (which form a special type of data tables); as a consequence, pattern structures are regarded in FCA as given (in some sense a priori to the analysis) rather than built (a posteriori ) from data. The main goal of this …paper is twofold: firstly, we would like to export the idea of pattern structures to and consistently with the framework/methodology of rough set theory (RST); secondly, we want to derive pattern structures from simple data tables rather than to regard them as the initial information about objects. To this end we present and discuss two methods of generating non-trivial pattern structures from simple information systems/tables. Both methods are inspired by near set theory, which is a methodology theoretically close to rough set theory, but developed in the topological settings of (descriptive) nearness of sets. Interestingly, these methods bear formal connections to other ideas from RST such as generalised decisions or symbolic value grouping. Show more

Keywords: rough set theory, formal concept analysis, near set theory, pattern structures

DOI: 10.3233/FI-2019-1790

Citation: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 363-380, 2019