Fundamenta Informaticae - Volume 21, issue 4

Article Type: Other

DOI: 10.3233/FI-1994-2148

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 255-256, 1994

Authors: Moser, L.E. | Melliar-Smith, P.M. | Kutty, G. | Ramakrishna, Y.S.

Article Type: Research Article

Abstract: We present axiomatizations for Until Temporal Logic (UTL) and for Since/Until Temporal Logic (SUTL). These logics are intended for use in specifying and reasoning about concurrent systems. They employ neither a next nor a previous operator, which obstruct the use of hierarchical abstraction and refinement, and make reasoning about concurrency difficult. We also provide a procedure for translating SUTL formulas into UTL formulas, and demonstrate that the axiomatizations are sound and complete with respect to the class of ω-sequences. We show, however, that the axiomatization of UTL admits models that the axiomatization of SUTL does not, thereby demonstrating that the …logics are not equivalent. Show more

DOI: 10.3233/FI-1994-2141

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 257-305, 1994

Authors: Baral, Chitta

Article Type: Research Article

Abstract: In this paper we study the relationship between preferential model semantics of Shoham [19] and Kraus et al. [12] with the flat version of conditional logic denned by Bell [3] and its variations. We present a new selection function without constraining or changing the relation between the possible worlds. Using our selection function we construct a conditional logic equivalent to Shoham's preferential model semantics [18].

DOI: 10.3233/FI-1994-2142

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 307-319, 1994

Authors: Düntsch, Ivo

Article Type: Research Article

Abstract: Rough relation algebras were introduced by S. Comer as a generalisation of algebras of Pawlak's rough sets and Tarski's relation algebras. In this paper, some algebraic and arithmetical properties of rough relation algebras are studied and the representable rough relation algebras are characterised.

DOI: 10.3233/FI-1994-2143

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 321-331, 1994

Authors: Cholak, Peter | Blair, Howard A.

Article Type: Research Article

Abstract: The class of locally stratified logic programs is shown to be Pi-1-1 complete by the construction of a reducibility of the class of infinitely branching nondeterministic finite register machines.

DOI: 10.3233/FI-1994-2144

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 333-344, 1994

Authors: Hungar, Hardi

Article Type: Research Article

Abstract: The notion of an expressive interpretation was originally introduced by Cook in order to formulate completeness results for Hoare-style proof systems. An interpretation is called expressive for a programming language if the input/output relation of every program can be expressed by a first-order formula. Various necessary or sufficient conditions for an interpretation to be expressive are known. In this paper a characterization is given which improves on these results. It holds for a wide spectrum of programming languages. An interpretation is expressive iff it is either 1. uniformly locally finite or 2. weakly arithmetic and it has evaluation predicates (which …return the truth value of a boolean expression, given its gödel number and the values of its free variables). Besides this characterization, it is investigated which first-order signatures allow nontrivial (i.e. non uniformly locally finite) expressive interpretations. Signatures which have (besides constants) only one unary function symbol and only unary relation symbols, have only trivial expressive interpretations. All other signatures allow nontrivial expressive interpretations as well. Show more

DOI: 10.3233/FI-1994-2145

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 345-365, 1994

Authors: Bozapalidis, Symeon

Article Type: Research Article

Abstract: We investigate tree series coming from the representations of the free monoid PΣ of trees of the form σ(t1 ,..., ti−1 , x, ti+1 ,..., tn ), into the matrices with coefficients in a semiring K. Tree length, branch enumeration, terminal tree enumeration, branch length, etc, are representable tree series. Tree modules, a new algebraic structure, are introduced and the next fundamental result is proved: A tree series S : TΣ → K is representable iff it is computed by a pointed tree module K- finitely generated iff the syntactic tree module FS associted with S, is …contained into a K- finitely generated subtreemodule of K « TΣ ». An Eilenberg-type theorem is also established, stating that the lattice of all subtreemodules of ReprK (Σ) is isomorphic to the lattice of all V- ideals of the ordered by inclusion set of subtremodules of K « TΣ ». The following inverse image theorem holds: for any subset E of a finite semiring K and for any representable tree series S : TΣ → K, the forest S−l (E) = {t ∈ TΣ /(S.t) ∈ E} is recognizable: As a consequence we get that matrix representable tree transductions ref 1 ect (in the sense of relations) recognizable forests. Several applications are given. Show more

DOI: 10.3233/FI-1994-2146

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 367-389, 1994

Authors: Moshkov, Mikhail

Article Type: Research Article

Abstract: We consider decision trees with questions from an infinite set and time complexity measures. We investigate decidability conditions for two optimization problems for decision trees.

DOI: 10.3233/FI-1994-2147

Citation: Fundamenta Informaticae, vol. 21, no. 4, pp. 391-401, 1994