Fundamenta Informaticae - Volume 100, issue 1-4

Article Type: Other

DOI: 10.3233/FI-2010-259

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. vii-ix, 2010

Authors: Bárány, Vince | Kaiser, Łukasz | Rabinovich, Alex

Article Type: Research Article

Abstract: We study an extension of monadic second-order logic of order with the uncountability quantifier "there exist uncountably many sets". We prove that, over the class of finitely branching trees, this extension is equally expressive to plain monadic second-order logic of order. Additionally we find that the continuum hypothesis holds for classes of sets definable in monadic second-order logic over finitely branching trees, which is notable for not all of these classes are analytic. …Our approach is based on Shelah's composition method and uses basic results from descriptive set theory. The elimination result is constructive, yielding a decision procedure for the extended logic. Show more

Keywords: infinite trees, monadic second-order logic, cardinality quantifiers, Cantor topology

DOI: 10.3233/FI-2010-260

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 1-17, 2010

Authors: van Benthem, Johan | Gheerbrant, Amélie

Article Type: Research Article

Abstract: Current methods for solving games embody a form of "procedural rationality" that invites logical analysis in its own right. This paper is a brief case study of Backward Induction for extensive games, replacing earlier static logical definitions by stepwise dynamic ones. We consider a number of analysis from recent years that look different conceptually, and find that they are all mathematically equivalent. This shows how an abstract logical perspective can bring out basic invariant …structure in games. We then generalize this to an exploration of fixed-point logics on finite trees that best fit game-theoretic equilibria. We end with some open questions that suggest a broader program for merging current computational logics with notions and results from game theory. This paper is largely a program for opening up an area: an extended version of the technical results will be found in the forthcoming dissertation [26]. Show more

Keywords: Backward Induction, ExtensiveGames, Dynamic-Epistemic Logic, Fixed-Point Logic

DOI: 10.3233/FI-2010-261

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 19-41, 2010

Authors: Coquand, Thierry | Jaber, Guilhem

Article Type: Research Article

Abstract: The goal of this note is to show the uniform continuity of definable functional in intuitionistic type theory as an application of forcing with dependent type theory.

Keywords: Type theory, dependent types, forcing

DOI: 10.3233/FI-2010-262

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 43-52, 2010

Authors: Dunin-K�plicz, Barbara | Nguyen, Linh Anh | Szałas, Andrzej

Article Type: Research Article

Abstract: In natural language we often use graded concepts, reflecting different intensity degrees of certain features. Whenever such concepts appear in a given real-life context, they need to be appropriately expressed in its models. In this paper, we provide a framework which allows for extending the BGI model of agency by grading beliefs, goals and intentions. We concentrate on TEAMLOG [6, 7, 8, 9, 12] and provide a complexity-optimal decision method for its graded version TEAMLOG^K …by translating it into CPDL_{reg} (propositional dynamic logic with converse and "inclusion axioms" characterized by regular languages). We also develop a tableau calculus which leads to the first EXPTIME (optimal) tableau decision procedure for CPDL_{reg} . As CPDL_{reg} is suitable for expressing complex properties of graded operators, the procedure can also be used as a decision tool for other multiagent formalisms. Show more

DOI: 10.3233/FI-2010-263

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 53-76, 2010

Authors: Düntsch., Ivo | Orłowska, Ewa | Rewitzky, Ingrid

Article Type: Research Article

Abstract: In this paper we show that the problem of discrete duality can be extended beyond the clasical setting of duality between a class of algebras and a class of relational structures. Namely, for some classes of algebras, the relevant dual structures are the structures with multirelations. Several applications of multirelations will be described.

Keywords: Apartness space, dependency, discrete duality, game of choice, multirelation, nearness space, neighbourhood system, point-set relation, skill relation

DOI: 10.3233/FI-2010-264

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 77-98, 2010

Authors: Grzymala-Busse, Jerzy W. | Rzasa, Wojciech

Article Type: Research Article

Abstract: In this paper, we present the newest version of the MLEM2 algorithm for rule induction, a basic component of the LERS data mining system. This version of the MLEM2 algorithm is based on local lower and upper approximations, and in its current formis presented in this paper for the first time. Additionally, we present results of experiments comparing the local version of the MLEM2 algorithm for rule induction with an older version of MLEM2, which was …based on global lower and upper approximations. Our experiments show that the local version of MLEM2 is significantly better than the global version of MLEM2 (2% significance level, two-tailed Wilcoxon test). Show more

DOI: 10.3233/FI-2010-265

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 99-116, 2010

Authors: Mazurkiewicz, Antoni

Article Type: Research Article

Abstract: The paper deals with the class of finite triangular graphs. It turns out that this class enjoys regular properties similar to those of trees and complete graphs. The main objective of the paper is to lift algorithms for some typical local computations, known for other classes of graphs, to the class of triangular graphs. Local algorithms on graphs, according to [8, 9], are defined as local rules for relabeling graph nodes. Rules are local, if they are defined …only for a class of subgraphs of processed graph (as neighborhoods of nodes or edges) and neither their results nor their applicability do not depend upon the knowledge of the whole graph labeling. While designing local algorithm for triangular graphs one needs to use some intrinsic properties of such graphs; it puts some additional light on their inherent structure. To illustrate essential features of local computations on triangular graphs, local algorithms for three typical issues of local computations are discussed: leader election, spanning tree construction, and nodes ordering. Correctness of these algorithms, as deadlock freeness, proper termination, and impartiality, are proved. Show more

Keywords: Local algorithms, triangular graphs, leader elections, spanning trees, nodes orderings

DOI: 10.3233/FI-2010-266

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 117-140, 2010

Authors: Skowron, Andrzej | Stepaniuk, Jarosław | Swiniarski, Roman

Article Type: Research Article

Abstract: We discuss some generalizations of the approximation space definition introduced in 1994 [24, 25]. These generalizations are motivated by real-life applications. Rough set based strategies for extension of such generalized approximation spaces from samples of objects onto their extensions are discussed. This enables us to present the uniform foundations for inducing approximations of different kinds of granules such as concepts, classifications, or functions. In particular, we emphasize the fundamental role of approximation …spaces for inducing diverse kinds of classifiers used in machine learning or data mining. Show more

Keywords: rough sets, granular computing, approximation space, extension of approximation space, concept approximation, function approximation

DOI: 10.3233/FI-2010-267

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 141-157, 2010

Authors: Vakarelov, Dimiter

Article Type: Research Article

Abstract: In this paper we present a point-free theory of Whiteheadean style of space and time. Its algebraic formulation, called dynamic contact algebra (DCA), is a Boolean algebra whose elements symbolized dynamic regions changing in time, with two spatio-temporal mereotopological relations between them: stable and unstable contact. We prove several representation theorems for DCAs, representing them in structures arising from products of contact algebras or from products of topological spaces. We also present a decidable …quantifier-free constraint logic for reasoning about stable and unstable mereotopological relations between dynamic regions. We consider the paper as a first step in point-free dynamic mereotopology. Show more

Keywords: Dynamicmereotopology, point-free theory of space and time, topological representation theorem, spatio-temporal logic

DOI: 10.3233/FI-2010-268

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 159-180, 2010

Authors: Veltink, Gerrit Jan

Article Type: Research Article

Abstract: Modern day computer architectures offer ever-increasing support for parallel processing, still it turns out to be quite difficult for programmers and therefore programs to tap into these parallel resources. To benefit from real general-purpose parallel computing we claim that it is likely that a paradigm shift is needed in the way we think about programming. This change of thought in turn will need to be reflected in future programming languages as well. We think that the …field of process algebra provides thorough insight in how to reason about the construction of software for concurrent systems and will be one of the enabling technologies supporting this transition. The wish to connect process algebra, a mathematical theory, to the world of computer-readable and executable specifications led to the development of PSF (Process Specification Formalism). PSF is an implementation of the process algebra ACP (Algebra of Communicating Processes) integrating ASF (Algebraic Specification Formalism) to specify algebraic data types. One of the first publications on PSF appeared in Fundamenta Informaticae in 1990. Here we stated as the first sentence of the abstract: "Traditional methods for programming sequential machines are inadequate for specifying parallel systems". Unfortunately, though some advancements have been made since 1990, we can still uphold this statement 20 years later. This current report documents the developments that lead to the construction of PSF and the 1990 publication and moreover it also documents how PSF and its tools have evolved since 1990 taking the conclusion and the outlook for future work from the original article as a reference point. Using the knowledge gained both in constructing tools for PSF and in using PSF to specify concurrent systems, we will judge, discuss and criticise the design decisions taken and show paths for future developments. Show more

Keywords: process algebra, algebraic data types, concurrency, parallel systems, formal specification, ACP, ASF, PSF

DOI: 10.3233/FI-2010-269

Citation: Fundamenta Informaticae, vol. 100, no. 1-4, pp. 181-227, 2010