Abstracts of Fundamenta Informaticae Volume 32.  

Number 1 

 M. F. FRIAS , G. A. BAUM and A. M.HAEBERER
Fork Algebras in Algebra, Logic and Computer Science
pages 1--25

Since the main themes at the Helena Rasiowa memorial were algebra, logic and computer science, we will present a survey of results on fork algebras from
these points of view. IIn this paper we study fork algebras from the points ofview of their algebraic and logical properties and applications. These results
will prove to be essential, in a future work, for the definition of a wide-spectrum calculus for program construction. 
S. KASANGIAN and S. VIGNA
The Topos of Labelled Trees: A Categorical Semantics for SCCS
pages  27-45

In this paper a we give a semantics for SCCS using the constructions of the topos of labelled trees. The semantics accounts for all aspects of the original
formulation of  SCCS including unbounded non-determinism. Then, a partial solution to the problem of characterizing bisimulation in terms of a class of morphisms is proposed. We define a class of morphisms of the topos of trees, called  conflict preserving, such that two trees T and  U are bisimilar iff there is a pair of conflict preserving morphisms f from T  to  U and g from  U to T such that fgf=f and gfg=g. It is the first characterization which does not require the existence of a third quotient object. The results can be easily extended to more general transition systems. 
D. PIGOZZI and A. SALIBRA
Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus
pages 47-90

 Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are ntended as an alternative to combinatory algebras in this regard. Like combinatory algebras they can be defined by true identities and thus form a variety in the sense of universal algebra.
One feature of lambda abstraction algebras that sets them apart from combinatory algebras is the way variables in the lambda calculus are abtracted; this provides each lambda abstraction algebra with an implicit coordinate system.
Another peculiar feature is the algebraic reformulation of ($\beta$)-conversion as the definition of abstract substitution. Functional lambda abstraction algebras arise as the
 ``coordinatizations'' of environment models or lambda models, the natural combinatory models of the lambda calculus. As in the case of cylindric and polyadic algebras, questions of the functional representation of various subclasses of lambda abstraction algebras  are an important part of the theory.
The main result of the paper is a stronger version of the functional representation theorem for locally finite lambda abstraction algebras, the algebraic analogue of the completeness theorem of lambda calculus. This result is used to study the connection between the combinatory models of the lambda calculus and lambda abstraction algebras. Two significant results of this kind are the existence of a strong categorical equivalence between lambda algebras and locally finite lambda abstraction algebras, and between lambda models and rich, locally finite lambda abstraction algebras. 


J. TYSZKIEWICZ
Queries and Algorithms Computable by Polynomial Time Existential Reflective Machines
pages 91-105

We consider two kinds of reflective relational machines: the usual ones, which use first order queries, and existential reflective machines, which use only first order existential queries. We compare these two computation models. We build on already existing results for standard relational machines, obtained by Abiteboul, Papadimitriou and
Vianu~[2], so we prove only results for existential machines.
First we show that for both standard and existential reflective machines the set of polynomial time computable Boolean queries consists precisely of all  PSPACE omputable queries.
Then we go further and compare which classes of algorithms both kinds of machines represent. Unless  PSPACEPNP there are PSPACE queries which cannot be computed by polynomial time existential reflective machines which use only polynomial amount of relational memory, while it is possible for standard reflective machines. We conclude that existential reflective machines, being equivalent in computational power to unrestricted machines, implement substantially worse algorithms than the latter.
Concerning deciding P classes of structures, every fixpoint query can be evaluated by a polynomial time unrestricted reflective machine using constant number of variables, while existential reflective machines need $\lfloor n/2\rfloor$ variables to implement the graph connectivity query. So again the algorithms represented by existential reflective machines are worse.
Finally, for each $k$ we get a characterization of the $\Delta_{k+1}^p$ level in the polynomial time hierarchy in terms of reflective relational machines which use either $\Pi^0_k$ or $\Sigma^p_k$ queries. 

Number 2


M.K. CHAKRABORTY  and E. ORLOWSKA
Substitutivity Principles in Some Theories of Uncertainty
pages 107-120

A semantics of identity inspired by rough set modeling of uncertainty is proposed and the underlying substitutivity principles are presented. A survey of some theories of identity is given, in particular, an interpretation of identity in E-unification theory, some many-valued logics and some algebraic theories. 


T. GAASTERLAND and J. LOBO
Qualifying Answers According to User Needs and Preferences
pages 121-137

This paper presents a rigorous methodology for using annotated logic programming techniques to handle user preferences and needs in answering database queries. Two alternative transformations turn a database program into a new program that returns answers to queries according to qualitative labels. The two transformations
have different semantics and are each appropriate in different situations.  We have modified the standard definitions of annotated logic programs to handle user needs and preferences in databases.
In the formalism, the user provides a lattice of domain-independent values that define preferences and needs and a set of domain specific user constraints qualified with lattice values. After the original database and the user constraints have been transformed into a new annotated deductive database, query-answering procedures for deductive databases are used, with minor modifications, to obtain annotated answers to queries. Because preference declaration is separated from data representation and management, preferences can be easily altered without touching the database.  The resulting query language allows users to ask for answers at different preference levels. 


 V. MAREK, A. NERODE and J. B. REMMEL
 Complexity of Recursive Normal Default Logic
 pages 139-147

Normal default logic, the fragment of default logic obtained by restricting defaults to rules of the form $\frac{\alpha: M\beta}{\beta}$, is the most important and widely studied part of default logic.  In [20], we proved  a basis theorem for extensions of recursive propositional logic normal default theories and hence for finite
predicate logic normal default theories.  That is, we proved that every recursive propositional normal default theory possesses an extension which is r.e. in $0'$. Here we
show that this bound is tight. Specifically, we show that for every r.e. set $A$ and every set $B$ r.e. in $A$ there is a recursive normal default theory $\langle D,W\rangle$ with a unique extension  which is Turing-equivalent to $A\bigoplus B$. A similar result holds for finite predicate logic normal default theories. 


G. PAUN, L. POLKOWSKI and A. SKOWRON
Rough Set Approximations of Languages
pages 149-162
We investigate here the possibility of approximating a language starting from a partial knowledge of its strings. This is understood as the possibility to read only a bounded part of a string: a prefix or a subword. In this way, indiscernibility relations among strings (they are equivalence or tolerance relations) are introduced, which lead to lower and upper approximations of languages. By varying the length of the perceived substring, we get sequences of approximations converging to the language. In many cases, the pproximations of context-free languages are proved to be regular languages. 
C. RUIZ and J. MINKER
Combining Closed World Assumptions with Stable Negation
pages 163-181

We study the semantics of disjunctive logic programs that simultaneously contain multiple kinds of default negations. We introduce operators $\mbox{not}_G$, \mbox{not}_W$, and $not_{STB}$ in the  language of logic programs to represent the {\em Generalized Closed World Assumption\/}, the {\em Weak Generalized Closed World Assumption\/}, and the stable negation, respectively. The notion of stratification involving different kinds of negations is defined and the meaning of stratified programs with multiple negations is described. The class of stratified programs is extended to the class of quasi-stratified programs and the semantics of the latest class is studied. 


K. SEGERBERG
Proposal for a Theory of Belief Revision Along the Lines of Lindstroem and Rabinowicz
pages 182-191

A particular modelling for belief revision is proposed that differs in important respects from $AGM$, the standard modelling that has dominated current discussion for more than a decade:  its Grove models are not linear and it can handle iterated change.


Number 3-4


 F.ALESSI , M. DEZANI-CIANCAGLINI and U. de'LIGUORO
A Convex Powerdomain over Lattices: its Logic and $\lambda$-Calculus
pages 193-250

To model at the same time parallel and nondeterministic functional calculi we define a powerdomain functor $\cal P$ such that it is an endofunctor over
the category of algebraic lattices.  $\cal P$ is locally continuous and we study the initial solution $\sdom$ of the domain equation  $D={\cal P}([D\rightarrow D]_\bot)$.
We derive from the algebras of $\cal P$ the logic of $\sdom$, that is the axiomatic description of its compact elements. We then define a $\lambda$-calculus and a type
assignment system using the logic of $\sdom$ as the related type theory. We prove that the filter model of this calculus, which is isomorphic to $\sdom$, is fully abstract with respect to the observational Preorder of the $\lambda$-calculus. 


A. BUCCIARELLI
Bi-models: Relational Versus  Domain-theoretic Approaches
pages  251-266

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. 


A. BUJOSA, R. CRIADO and M. A. HERNANDEZ-MEDINA
 Unification: Nothing but the Solution of a System of Linear Equations
 pages 267-280

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. 


 M. A. CASTILHO, L. FARINAS del CERRO, O. GASQUET and A. HERZIG
Modal Tableaux with Propagation Rules and Structural Rules
pages 281-297

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. 



 
M. K. CHKRABORTY and S. BASU
Graded Consequence and Some Metalogical Notions Generalized
pages 299-311

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. 



 
B. CHLEBUS, K.DIKS and  A. PELC
Transition-optimal Token Distribution
pages 313-328

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 ost-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. 


W. FOKKINK
 An Axiomatization for Regular Processes in Timed Branching  Bisimulation
pages 329-340

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. 


J. HONKALA
 Decision Problems Concerning a Power Series Generalization of DT0L Systems
pages 341-348

We study a power series generalization of DT0L systems with main interest on decidability questions. 


M. A. KHAMSI and D. MISANE
Disjunctive Signed Logic Programs
pages 349-357

 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. 


W. SKARBEK
On Relation of Image Compression and Image  Association
pages 359-371

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 ${\cal N}_i$ is designed for the $i$-th image and it implements a stochastic nonlinear operator ${\cal F}_i.$ It can be shown that under realistic assumptions ${\cal F}_i$ 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. 


F. L. TIPLEA
Jumping Petri Nets. Specific Properties}
pages 373-392

A  Jumping Petri Net ([18], [12]), $JPTN$ for short, is defined as a classical net which can spontaneously jump from a marking to another one. In [18] it has been shown that the reachability problem for $JPTN$'s is undecidable, but it is decidable for finite $JPTN$'s ($FJPTN$).
In this paper we establish some specific properties and investigate the computational power of such nets, via the interleaving semantics. Thus, we show that the non-labelled $JPTN$'s have the same computational power as the labelled or $\lambda$-labelled $JPTN$'s. When final markings are considered, the power of $JPTN$'s equals the power
of Turing machines. The family of regular languages and the family of languages generated by $JPTN$'s with finite state space are shown to be equal. Languages generated by $FJPTN$'s can be represented in terms of regular languages and substitutions with  classical Petri net languages. This characterization result leads to many important consequences, e.g. the recursiveness (context-sensitiveness, resp.) of languages generated by arbitrarily labelled (labelled, resp.) $FJPTN$'s.
A pumping lemma for nonterminal jumping net languages is also established. Finally, some  comparisons  between  families  of languages are given, and a connection between $FJPTN$'s and a subclass of inhibitor nets is presented.