Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Purchase individual online access for 1 year to this journal.
Price: EUR 410.00Impact Factor 2023: 0.8
Fundamenta Informaticae is an international journal publishing original research results in all areas of theoretical computer science. Papers are encouraged contributing:
- solutions by mathematical methods of problems emerging in computer science
- solutions of mathematical problems inspired by computer science.
Topics of interest include (but are not restricted to): theory of computing, complexity theory, algorithms and data structures, computational aspects of combinatorics and graph theory, programming language theory, theoretical aspects of programming languages, computer-aided verification, computer science logic, database theory, logic programming, automated deduction, formal languages and automata theory, concurrency and distributed computing, cryptography and security, theoretical issues in artificial intelligence, machine learning, pattern recognition, algorithmic game theory, bioinformatics and computational biology, quantum computing, probabilistic methods, & algebraic and categorical methods.
Article Type: Other
DOI: 10.3233/FI-1977-1101
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. i-vii, 1977
Article Type: Correction
DOI: 10.3233/FI-1977-1117
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. I-I, 1977
Authors: Mirkowska, Grażyna
Article Type: Research Article
Abstract: The paper presents tools for formalizing and proving properties of programs. The language of algorithmic logic constitutes an extension of a programming language by formulas that describe algorithmic properties. The paper contains two axiomatizations of algorithmic logic, which are complete. It can be proved that every valid algorithmic property possesses a formal proof. An analogue of Herbrand theorem and a theorem on the normal form of a program are proved. Results of meta-mathematical character are applied to theory of programs, e.g. Paterson’s theorem is an immediate corollary to Herbrand’s theorem.
DOI: 10.3233/FI-1977-1102
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 1-17, 1977
Authors: Kreczmar, Antoni
Article Type: Research Article
Abstract: In the paper we solve some effectivity problems of program schemas. Such properties of programs as, for example, the strong and the weak equivalence, the correctness and the partial correctness of a program, the halting problem are classified in Kleene-Mostowski hierarchy. A basic tool used in the paper is algorithmic logic.
DOI: 10.3233/FI-1977-1103
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 19-32, 1977
Authors: Winkowski, Jozef
Article Type: Research Article
Abstract: In this paper an approach to proving properties of programs is presented, which slightly differs from the methods developed up to now. In contrast to other approaches it needs no formal program notion but only a formalization of some basic program properties. The key idea in this approach is to associate with any program under consideration a formal theory in such a way that all the processes, which may be thougth as possible executions of the program considered, become models of the associated theory. Such a theory can be constructed by formulating axioms about the program executions, and about …quantities which explicitly or implicitly occur in the program and change their values while the program is being executed. Appropriate axioms and the properties which are to be proved can easily be described by formulas of the predicate logic. This enables one to consider various properties of the program as theorems of the resulting theory and to prove them by usual means of the predicate logic. Show more
DOI: 10.3233/FI-1977-1104
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 33-49, 1977
Authors: Lipski Jr., Witold
Article Type: Research Article
Abstract: The following combinatorial problem arising in file organization is considered: Given three sets M1 , M2 , M3 ⊆ X, find an arrangement of X such that each Mi is a segment of consecutive elements of X. Also some theorems extending the results of Ghosh concerning the two-dimensional consecutive retrieval property are proved. In particular, necessary and sufficient condition for a family of three sets to admit a two-dimensional organization is given.
DOI: 10.3233/FI-1977-1105
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 51-60, 1977
Authors: Dembiński, Piotr
Article Type: Research Article
Abstract: A simple (finite automata) model for parallel computation is considered. The parallelism is replaced by nondeterminism. The class of all parallel realizations of given processes is algebraically characterized, and a natural “less parallel” gelation between realizations is introduced. A sufficient and necessary condition is riven for the existence of the maximally parallel realization in the set of correct lealizations (distinguished by means of computational invariants).
DOI: 10.3233/FI-1977-1106
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 61-69, 1977
Authors: Tiuryn, Jerzy
Article Type: Research Article
Abstract: An M-groupoid is a simplified model of computer. The classes of M-groupoids, address machines, stored program computers and iterative systems are presented as categories – by a suitable choice of homomorphisms. It is shown that the first three categories are equivalent, whereas the fourth is weaker (it is not equivalent to the previous ones and it can easily be embedded in the category of M-groupoids). This fact proves that M-groupoids form an essentially better and reasonably simple approximation of more complicated models of computers than iterative systems.
DOI: 10.3233/FI-1977-1107
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 71-91, 1977
Authors: Banachowski, Lech
Article Type: Research Article
Abstract: The present paper contains investigations concerning the semantic correctness of programs. Presented methods of analysis of programs are appropriate for every domain of computation. Algorithmic logic extended by classical quantifiers is a fundamental mathematical tool used in the paper. Interrelations between properties of programs and properties of descriptions of programs are studied (a description of a program is a mathematical model of the notion of a documentation of a program).
DOI: 10.3233/FI-1977-1108
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 93-119, 1977
Authors: Marek, Wiktor | Traczyk, Tadeusz
Article Type: Research Article
Abstract: In the paper the notion of a stochastic informational retrieval system is introduced and discussed. This is a generalization of the notion of an i.s.r. system in the case of data which are measured with some precision. The method of numerical Boolean algebras is applied. Theorems connected with the decomposition of such systems are proved.
DOI: 10.3233/FI-1977-1109
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 121-130, 1977
Authors: Janicki, Ryszard
Article Type: Research Article
Abstract: A mathematical model for recursive coroutines in introduced. Relationships between Mazurkiewicz algorithms and this model are considered. Some linguistic and computational properties of coroutines are proved. The set of all functions computed by programs with recursive coroutines is proved to contain the set of all functions computed by commonly used recursive programs.
DOI: 10.3233/FI-1977-1110
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 131-145, 1977
Authors: Mirkowska, Grażyna
Article Type: Research Article
DOI: 10.3233/FI-1977-1111
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 147-165, 1977
Authors: Banachowski, Lech
Article Type: Research Article
DOI: 10.3233/FI-1977-1112
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 167-193, 1977
Authors: Kreczmar, Antoni
Article Type: Research Article
Abstract: In the present paper we investigate algorithmic properties of fields. We prove that axioms of formally real fields for the field R of reals and axioms of fields of characteristic zero for the field C of complex numbers, give the complete characterization of algorithmic properties. By Kfoury’s theorem programs which define total functions over R or C are effectively equivalent to loop-free programs. Examples of programmable and nonprogrammable functions and relations over R and C are given. In the case of ordered reals the axioms of Archimedean ordered …fields completely characterize algorithmic properties. We show how to use the equivalent version of Archimed’s axiom (the exhaustion rule) in order to prove formally the correctness of some iterative numerical algorithms. Show more
Keywords: programs and programmability, algorithmic properties, programmability in fields, axioms for algorithmic properties of reals, ordered reals and complex numbers
DOI: 10.3233/FI-1977-1113
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 195-230, 1977
Authors: Janicki, Sławomir | Szynal, Dominik
Article Type: Research Article
Abstract: There are a great many research works concerning the well-known stochastic automata of Moore, Mealy, Rabin, Turing and others. Recently an automaton of Markov’s chain type has been introduced by Bartoszyński. This automaton is obtained by a generalization of Pawlak’s deterministic machine. The aim of this note is to give a concept of a stochastic automaton of Markov’s generalized chain type. The introduced automaton called a stochastic k -automaton (s.k -a.) is a common generalization of Bartoszyński’s automaton and Grodzki’s deterministic k -machine. By a stochastic k -automaton we mean an ordered triple M k …= ⟨ U , a , π ⟩ , k ⩾ 1 , where U denotes a finite non-empty set, a is a function from U k to [0, 1] with ∑ v ∈ U k a ( v ) = 1 , and π is a function from U k+1 to [0,1] with ∑ u ∈ U π ( v , u ) = 1 for every v ∈ U k . For all N ⩾ k we can define a probability measure P N on U N = U × U × … × U as follows: P N ( u 1 , u 2 , … , u N ) = a ( u 1 , u 2 , … , u k ) π ( u 1 , u 2 , … , u k + 1 ) π ( u 2 , u 3 , … , u k + 2 ) … π ( u N − k , u N − k + 1 , … , u N ) . We deal with the problems of the shrinkage and the extension of a system of s.k-a .’s M k ( i ) = ⟨ U , a ( i ) , π ( i ) ⟩ , i = 1 , 2 , … , m , m ⩾ 2 . In this note there are given conditions under which an s.k -a. M k = ⟨ U , a , π ⟩ exists and the language of this automaton defined as L M = { ( u 1 , u 2 , u 3 , … ) : ∧ N ⩾ 1 P N ( u l , u 2 , … u N ) > 0 } either contains the languages of all the automata M k ( i ) , i = 1 , 2 , … , m , or this language equals the intersection of all those languages. Show more
Keywords: stochastic k-automaton, extension, shrinkage, N-word, set of N-words, words, language, probability measure, carrier, concordance, truly concordance, pairwise concordance
DOI: 10.3233/FI-1977-1114
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 231-241, 1977
Authors: Karásek, Jiří
Article Type: Research Article
Abstract: The paper deals with nondeterministic and deterministic k -machines which represent, in a certain sense, generalizations of some well-known notions. Connections between the sets of sequences constructed by nondeterministic and deterministic k -machines, and some other related problems are investigated.
Keywords: deterministic machines, nondetcrministic machines, finite automata
DOI: 10.3233/FI-1977-1115
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 243-250, 1977
Authors: Aiello, Luigia | Aiello, Mario | Attardi, Giuseppe | Prini, Gianfranco
Article Type: Research Article
Abstract: An interactive proof checker is a system which is able of building a formal proof (in some deductive calculus) by executing commands provided by the user. Proof checkers are useful both for making experiments in proof construction within various formal systems and for proving theorems in those fields of mathematics (such as mathematical theory of computation) where proofs are necessarily very large and unfeasible by hand. Two levels may be distinguished in a proof checker. The lower one implements the proof management routines, and is independent of any particular logic. The higher one implements the inference rules of a particular …logical calculus. Powerful higher level rules are also needed to make the use of the checker practical. Almost all routine steps may be then generated automatically, and the user has just to give some “hints” to the checker, which transforms an “informal argument” into a formal proof. Show more
Keywords: automatic theorem proving, denotational semantics of programming languages, mathematical theory of computation, proof of formal properties of programs
DOI: 10.3233/FI-1977-1116
Citation: Fundamenta Informaticae, vol. 1, no. 1, pp. 251-275, 1977
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
[email protected]
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office [email protected]
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
如果您在出版方面需要帮助或有任何建, 件至: [email protected]