Fundamenta Informaticae - Volume 81, issue 1-3

Authors: Krajewski, Stanisław

Article Type: Research Article

Abstract: The so called Lucas argument, and more recently that put forward by Penrose, attempt to use Gödel's incompleteness theorems to demonstrate the non-mechanical nature of the mind, or in other words, that mind is not computational. Generalizing and strengthening the criticism of those arguments that have been made by mathematical logicians, it is proved that all possible variants of the argument must lead to a vicious circle or to inconsistency or to unsoundness (acceptance of a …false statement). This defeats Lucas, who assumes his consistency and Penrose, who assumes his soundness. As Gödel has remarked, the existence of a robot, whom we will call Luke, equivalent to the humanmind as far as mathematical capacities go, is not excluded by his incompleteness theorem. Show more

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 173-181, 2007

Authors: Krynicki, Michał | Mostowski, Marcin | Zdanowski, Konrad

Article Type: Research Article

Abstract: The paper presents the current state of knowledge in the field of logical investigations of finite arithmetics. This is an attempt to summarize the ideas and results in this area. Some new results are presented – these are mainly generalizations of the earlier results related to properties of sl-theories and some nontrivial cases of FM-representability theorem.

Keywords: finite models, arithmetic, finite arithmetic, interpretations, complete sets, FM-representability, truth definitions

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 183-202, 2007

Authors: Maksimova, Larisa

Article Type: Research Article

Abstract: In 1964-68 Andrzej Grzegorczyk investigated relational and topological semantics for the intuitionistic logic [15]–[18] . In this connection, following to McKinsey and Tarski, he also considered a semantics for modal logics. It is well known that there is a translation of the intuitionistic logic into the modal S4 logic. This translation was suggested by Gödel in order to find an interpretation of the intuitionistic logic via provability operator. A. Grzegorczyk found a modal formula G …valid in all partially ordered frames with descending chain condition but not in all topological spaces. It follows that this formula is not valid in S4 but one can translate the intuitionistic logic into the calculus arising from S4 by adding Grzegorczyk's formula as a new axiom schema. The resulting logic was called the Grzegorczyk logic in later papers and books on modal logic. There are a lot of investigations devoted to the Grzegorczyk logic. In this paper we give a short overview of results on the Grzegorczyk logic and its extensions. Show more

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 203-210, 2007

Authors: Marek, Victor W. | Remmel, Jeffrey B.

Article Type: Research Article

Abstract: Logic programming with stable logic semantics (SLP) is a logical formalism that assigns to programs, i.e. sets of clauses where we allow both atoms and their negations in the body of clause, a special class of models of the program, called stable models. We show that stable logic semantics does not satisfy the natural analogue of the compactness theorem. However, we show that there are a variety of conditions which will ensure that a program satisfies …the analogue of the compactness theorem. Show more

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 211-239, 2007

Authors: Mostowski, Marcin

Article Type: Research Article

Abstract: In this paper we consider a "mathematical" proof of the Church Thesis. The proof is based on very weak assumptions about intuitive computability and the FM-representability theorem from [11]. It develops and improves the argument mentioned in [12]. Our argument essentially depends on the mathematical model of the world we are in.

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 241-248, 2007

Authors: Murawski, Roman

Article Type: Research Article

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 249-256, 2007

Authors: Romanowska, Anna B. | Smith, Jonathan D.H. | Orłowska, Ewa

Article Type: Research Article

Abstract: This paper presents a new approach to the study of (real) barycentric algebras, in particular convex subsets of real affine spaces. Barycentric algebras are cast in the setting of two-sorted algebras. The real unit interval indexing the set of basic operations of a barycentric algebra is replaced by an LΠ-algebra, the algebra of Łukasiewicz Product Logic. This allows one to define barycentric algebras abstractly, independently of the choice of the unit real interval. It reveals an …unexpected connection between barycentric algebras and (fuzzy) logic. The new class of abstract barycentric algebras incorporates barycentric algebras over any linearly ordered field, the B-sets of G. M. Bergman, and E. G. Manes' if-then-else algebras over Boolean algebras. Show more

Keywords: affine space, barycentric algebra, mode, cancellative mode, LΠ-algebra, Łukasiewicz Product Logic, heterogeneous algebra, B-set, if-then-else algebra, rectangular algebra

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 257-273, 2007

Authors: Orłowska, Ewa | Rewitzky, Ingrid

Article Type: Research Article

Abstract: Discrete dualities are presented for Heyting algebras with various modal operators, for Heyting algebras with an external negation, for symmetric Heyting algebras, and for Heyting-Brouwer algebras.

Keywords: Discrete duality, Heyting algebra, modal operator, negation, symmetric Heyting algebra, Heyting-Brouwer algebra

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 275-295, 2007

Authors: Rybakov, Vladimir V.

Article Type: Research Article

Abstract: This paper aims to prove that the linear temporal logic LTL^{u,s}_{n,n-1} (N), which is an extension of the standard linear temporal logic LTL by operations Since and Previous (LTL itself, as standard, uses only Until and Next) and is based on the frame of all natural numbers N, as generating Kripke/Hintikka structure, is decidable w.r.t. admissible consecutions (inference rules). We find an algorithm recognizing consecutions admissible in LTL^{u,s}_{n,n-1} (N). As a …consequence this algorithm solves satisfiability problem and shows that LTL^{u,s}_{n,n-1} (N) itself is decidable, despite LTL^{u,s}_{n,n-1} (N) does not have the finite model property. Show more

Keywords: decidability, algorithms, inference rules, temporal logic, linear temporal logic, admissible inference rules

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 297-313, 2007

Authors: Salwicki, Andrzej

Article Type: Research Article

Abstract: The paper of Andrzej Grzegorczyk [19] on hierachy of the primitive recursive classes dates for 1953. This is the most frequently cited article of Polish author in computer science literature, having some hundreds citations. Moreover, many citations are in the papers of eminent computer scientists e.g. [10,24,33,34,31], sometimes the laureates of prestigious awards. In this paper we make an attempt to present Andrzej Grzegorczyk as a computer scientist.

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 315-323, 2007

Authors: Srebrny, Marian | St�pień, Lidia

Article Type: Research Article

Abstract: In this paper we present an application of the propositional SATisfiability environment to computing bases of some vector spaces. As a motivation we refer to certain computational tasks in the area of the algebraic theory of quadratic forms; more precisely, in the theory of Witt rings of quadratic forms. As known in algebra, the problem of finding all automorphisms of an elementary Witt ring can be reduced to searching for some special kind of bases of …certain vector space over the two-element Galois field. We show how one can code a search for some kind of bases as a propositional formula in such a way that its satisfying valuations code the desired bases. Some encouraging experimental results are reported for the proposed propositional search procedure using the currently best SAT solvers. Show more

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 325-345, 2007

Authors: Švejdar, Vítězslav

Article Type: Research Article

Abstract: Q^- is a weaker variant of Robinson arithmetic Q in which addition and multiplication are partial functions, i.e. ternary relations that are graphs of possibly non-total functions. We show that Q is interpretable in Q^- . This gives an alternative answer to a question of A. Grzegorczyk whether Q^- is essentially undecidable.

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 347-354, 2007

Authors: Woleński, Jan

Article Type: Research Article

Citation: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 355-365, 2007