Fundamenta Informaticae - Volume 32, issue 3-4

Authors: Alessi, Fabio | Dezani-Ciancaglini, Mariangiola | Liguoro, Ugo de'

Article Type: Research Article

Abstract: To model at the same time parallel and nondeterministic functional calculi we define a powerdomain functor Ρ such that it is an endofunctor over the category of algebraic lattices. Ρ is locally continuous and we study the initial solution D∞ of the domain equation D = Ρ([D → D]⊥ ). We derive from the algebras of Ρ the logic of D∞ , that is the axiomatic description of its compact elements. We then define a λ-calculus and a type assignment system using the logic of D∞ as the related type theory. We prove that the filter model of …this calculus, which is isomorphic to D∞ , is fully abstract with respect to the observational Preorder of the λ-calculus. Show more

Keywords: λ-calculus, Nondeterminism, Full Abstraction, Powerdomain Construction, Intersection Type Disciplines

DOI: 10.3233/FI-1997-323401

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 193-250, 1997

Authors: Bucciarelli, Antonio

Article Type: Research Article

Abstract: We introduce a technique based on logical relations, which, given two models M and N of a simply typed lambda-calculus L, allows us to construct a model M/N whose L-theory is a superset of both Th(M) and Th(N). By means of some examples, we show that classic bi-domain constructions lack this property, in general.

Keywords: simply typed λ-calculi, logical relations, PCF, Scott-continuous model, stable model

DOI: 10.3233/FI-1997-323402

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 251-266, 1997

Authors: Bujosa, Andrés | Criado, Regino | Hernandez-Medina, Miguel A.

Article Type: Research Article

Abstract: We use the ring of p-tangles to submerge symbolic expressions in a module structure. Using this structure, the problem of unifying expressions is shown to be equivalent to certain linear systems of equations with coefficients in the ring, whose solution gives the result of unification, if this exists.

DOI: 10.3233/FI-1997-323403

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 267-280, 1997

Authors: Castilho, Marcos A. | del Cerro, Luis Fariñas | Gasquet, Olivier | Herzig, Andreas

Article Type: Research Article

Abstract: In this paper we generalize the existing tableau methods for modal logics. First of all, while usual modal tableaux are based on trees, our basic structures are rooted directed acyclic graphs (RDAG). This allows natural tableau rules for some modal logics that are difficult to capture in the usual way (such as those having an accessibility relation that is dense or confluent). Second, tableau rules rewrite patterns, which are (schemas of) parts of a RDAG. A particular case of these rules are the single-step rules recently proposed by Massacci. This allows in particular tableau rule presentations for K5, KD5, K45, …KD45, and S5 that respect the subformula property. Third, we divide modal tableau rules into propagation rules and structural rules. Structural rules construct new edges and nodes (without adding formulas to nodes), while propagation rules add formulas to nodes. This distinction allows to prove completeness in a modular way. Show more

Keywords: Tableaux, Modal logic, Structural Rules, Propagation Rules

DOI: 10.3233/FI-1997-323404

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 281-297, 1997

Authors: Chakraborty, Mihir K. | Basu, Sanjukta

Article Type: Research Article

Abstract: The notion of graded consequence and some other metalogical notions like consistency, inconsistency, tautologihood and theoremhood to which grades have been introduced earlier by us are reviewed in the context of generalized operators. Some preliminary results regarding the relation between the notion of graded consequence and the notion of graded inconsistency are proved. The method of axiomatization is reconsidered in this general situation.

Keywords: Fuzzy set, fuzzy logic, graded consequence, residuated lattice

DOI: 10.3233/FI-1997-323405

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 299-311, 1997

Authors: Chlebus, Bogdan S. | Diks, Krzysztof | Pelc, Andrzej

Article Type: Research Article

Abstract: There is given a graph, that models a communication network of a multiprocessor system, and there are tokens (jobs) allocated to nodes of the graph. The task is to distribute the tokens evenly, subject to the constraint that they may be moved only along the edges of the graph. The cost of a distribution strategy is measured as the total number of operations of moving a token along an edge. An algorithm for general graphs is developed, by reduction to a maximum-flow minimum-cost problem, that finds a cost-optimal distribution strategy, given a graph and an initial token allocation. The main …result is an algorithm for graphs that are lines of nodes; it finds the distribution strategy in time O(n), for a line of n nodes. Show more

Keywords: graph, token, optimal distribution, line of nodes

DOI: 10.3233/FI-1997-323406

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 313-328, 1997

Authors: Fokkink, Wan

Article Type: Research Article

Abstract: Klusener introduced a timed variant of branching bisimulation. In this paper it is shown that Klusener's axioms for finite process terms, together with two standard axioms for recursion, make a complete axiomatization for regular processes modulo timed branching bisimulation.

Keywords: timed process algebra, regular processes, branching bisimulation

DOI: 10.3233/FI-1997-323407

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 329-340, 1997

Authors: Honkala, Juha

Article Type: Research Article

Abstract: We study a power series generalization of DTOL systems with main interest on decidability questions.

Keywords: DTOL system, formal power series, decidability

DOI: 10.3233/FI-1997-323408

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 341-348, 1997

Authors: Khamsi, Mohamed A. | Misane, Driss

Article Type: Research Article

Abstract: In this work, we define signed disjunctive programs and investigate the existence of answer sets for this class of programs. Our main argument is based on an analogue of Tarski's fixed point theorem which we prove for multivalued mappings. This is an original approach compared to known techniques used to prove the existence of answer sets for disjunctive programs.

DOI: 10.3233/FI-1997-323409

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 349-357, 1997

Authors: Skarbek, Władysław

Article Type: Research Article

Abstract: Based on two image compression schemes (MIT and RNS), it is shown that it is possible to associate similar object images using their intermediate representation. Thus both methods can be applied to large image database for both goals: high quality image compression and reliable search for queries by image content. MIT scheme of Moghaddam and Pentland is specialized to face images. It moves image comparison task from high dimensional image space to low dimensional principal subspace spanned on eigenfaces. The closest point in the subspace is used for image association. RNS scheme of the author represents images (not limited to …a certain scene type) by recurrent neural subnetworks which together with a competition layer create an associative memory. The single recurrent subnetwork Ni is designed for the i-th image and it implements a stochastic nonlinear operator Fi . It can be shown that under realistic assumptions Fi has a unique attractor which is located in the vicinity of the original image. When at the input a noisy, incomplete or distorted image is presented, the associative recall is implemented in two stages. Firstly, a competition layer finds the most invariant subnetwork. Next, the selected recurrent subnetwork reconstructs in few iterations the original image. Show more

DOI: 10.3233/FI-1997-323410

Citation: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 359-371, 1997