Fundamenta Informaticae - Volume 14, issue 4

Article Type: Other

DOI: 10.3233/FI-1991-14401

Citation: Fundamenta Informaticae, vol. 14, no. 4, pp. i-viii, 1991

Authors: Blikle, Andrzej

Article Type: Research Article

Abstract: Partial functions, hence also partial predicates, cannot be avoided in algorithms. However, in spite of the fact that partial functions have been formally introduced into the theory of software very early, partial predicates are still not quite commonly recognized. In many programming- and software-specification languages partial Boolean expressions are treated in a rather simplistic way: the evaluation of a Boolean sub-expression to an error leads to the evaluation of the hosting Boolean expression to an error and, in the consequence, to the abortion of the whole program. This technique is known as an eager evaluation of expressions. A …more practical approach to the evaluation of expressions – gaining more interest today among both theoreticians and programming-language designers – is lazy evaluation . Lazily evaluated Boolean expressions correspond to (non-strict) three-valued predicates where the third value represents both an error and an undefinedness . On the semantic ground this leads to a three-valued propositional calculus, three-valued quantifiers and an appropriate logic. This paper is a survey-essay devoted to the discussion and the comparison of a few three-valued propositional and predicate calculi and to the discussion of the author’s claim that a two-valued logic, rather than a three-valued logic, is suitable for the treatment of programs with three-valued Boolean expressions. The paper is written in a formal but not in a formalized style. All discussion is carried on a semantic ground. We talk about predicates (functions) and a semantic consequence relation rather than about expressions and inference rules. However, the paper is followed by more formalized works which carry our discussion further on a formalized ground, and where corresponding formal logics are constructed and discussed. Show more

DOI: 10.3233/FI-1991-14402

Citation: Fundamenta Informaticae, vol. 14, no. 4, pp. 387-410, 1991

Authors: Konikowska, Beata | Tarlecki, Andrzej | Blikle, Andrzej

Article Type: Research Article

Abstract: Different calculi of partial or three-valued predicates have been used and studied by several authors in the context of software specification, development and validation. This paper offers a critical survey on the development of three-valued logics based on such calculi. In the first part of the paper we review two three-valued predicate calculi, based on, respectively, McCarthy’s and Kleene’s propositional connectives and quantifiers, and point out that in a three-valued logic one should distinguish between two notions of validity: strong validity (always true) and weak validity (never false). We define in model-theoretic terms a number of consequence …relations for three-valued logics. Each of them is determined by the choice of the underlying predicate calculus and of the weak or strong validity of axioms and of theorems. We discuss mutual relationships between consequence relations defined in such a way and study some of their basic properties. The second part of the paper is devoted to the development of a formal deductive system of inference rules for a three-valued logic. We use the method of semantic tableaux (slightly modified to deal with three-valued formulas) to develop a Gentzen-style system of inference rules for deriving valid sequents, from which we then derive a sound and complete system of natural deduction rules. We have chosen to study the consequence relation determined by the predicate calculus with McCarthy’s propositional connectives and Kleene’s quantifiers and by the strong interpretation of both axioms and theorems. Although we find this choice appropriate for applications in the area of software specification, verification and development, we regard this logic merely as an example and use it to present some general techniques of developing a sequent calculus and a natural deduction system for a three-valued logic. We also discuss the extension of this logic by a non-monotone is-true predicate. Show more

DOI: 10.3233/FI-1991-14403

Citation: Fundamenta Informaticae, vol. 14, no. 4, pp. 411-453, 1991

Authors: Novotný, Miroslav | Pawlak, Zdzizław

Article Type: Research Article

Abstract: The semilattice of all subsets of a finite nonempty set provided with the operation of union and a congruence of this semilattice enable to define independent elements of the semilattice. Reducts, subreducts, and superreducts of an arbitrary element in the semilattice are introduced and investigated. A particular type of congruence, the so called rough top equality, is studied. These algebraic notions and methods are applied to black boxes, to information systems, and to contexts in Wille’s sense. The algebraic results are used to solve the problem whether two sets of inputs give the same output in a black box, …whether two sets of attributes define the same classification of objects in an information system, and, finally, whether two sets of features generate the same concept in a context. Partial dependence between two sets of attributes of an information system is introduced and a distance between these sets is defined. Show more

Keywords: dependence space, independence, reduct, subreduct, superreduct, rough top equality, black box, information system, context, partial dependence

DOI: 10.3233/FI-1991-14404

Citation: Fundamenta Informaticae, vol. 14, no. 4, pp. 454-476, 1991

Authors: Korczynski, Waldemar

Article Type: Research Article

Abstract: In this paper an algebraic characterization of a class of Petri nets is given. The nets are characterized by a kind of algebras, which can be considered as a generalization of the concept of the case graph of a (marked) Petri net.

DOI: 10.3233/FI-1991-14405

Citation: Fundamenta Informaticae, vol. 14, no. 4, pp. 477-491, 1991

Authors: Comer, Stephen D.

Article Type: Research Article

Abstract: This paper is based on the notion of an information system <U ,Ω,V ,f > in the sense of Pawlak. Every set of knowledge P ⊆ Ω determines a closure operator on U . The class of Boolean algebras with added operations determined by all sets of know ledge are axiomatixed. As a consequence of the representation theorem information systems can be constructed that have a prescribed lattice of functional dependencies.

DOI: 10.3233/FI-1991-14406

Citation: Fundamenta Informaticae, vol. 14, no. 4, pp. 492-502, 1991