Fundamenta Informaticae - Volume 1, issue 1

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