Fundamenta Informaticae - Volume 28, issue 1-2

Authors: Marek, Wiktor | Polkowski, Lech | Skowron, Andrzej

Article Type: Other

DOI: 10.3233/FI-1996-281214

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. i-i, 1996

Authors: Alferes, José Júlio | Pereira, Luís Moniz | Przymusinski, Teodor C.

Article Type: Research Article

Abstract: In order to be able to explicitly reason about beliefs, we've introduced a non-monotonic formalism, called the Autoepistemic Logic of Beliefs, AEB, obtained by augmenting classical propositional logic with a belief operator, β. For this language we've defined the static autoepistemic expansions semantics. The resulting nonmonotonic knowledge representation framework turned out to be rather simple and yet quite powerful. Moreover, it has some very natural properties which sharply contrast with those of Moore's AEL. While static expansions seem to provide a natural and intuitive semantics for many belief theories, and, in particular, for all affirmative belief theories (which include the …class of all normal and disjunctive logic programs), they often can lead to inconsistent expansions for theories in which (subjective) beliefs clash with the known (objective) information or with some other beliefs. In particular, this applies to belief theories (and to logic programs) with strong or explicit negation. In this paper we generalize AEB to avoid the acceptance of inconsistency provoking beliefs. We show how such AEB theories can be revised to prevent belief originated inconsistencies, and also to introduce declarative language level control over the revision level of beliefs, and apply it to the domains of diagnosis and declarative debugging. The generality of our AEB framework can capture and justify the methods that have been deployed to solve similar revision problems within the logic programming paradigm. Show more

Keywords: Belief Revision, Logics of Knowledge and Beliefs, Non-Monotonic Reasoning, Logic Programming

DOI: 10.3233/FI-1996-281201

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 1-22, 1996

Authors: Apt, Krzysztof R. | Ben-Eliyahu, Rachel

Article Type: Research Article

Abstract: We show here that meta-variables of Prolog admit a simple declarative interpretation. This allows us to extend the usual theory of SLD-resolution to the case of logic programs with meta-variables, and to establish soundness and strong completeness of the corresponding extension of the SLD-resolution. The key idea is the use of ambivalent syntax which allows us to use the same symbols as function and relation symbols. We also study the problem of absence of run-time errors in presence of meta-variables. We prove that this problem is undecidable. However, we also provide some sufficient and polynomial-time-decidable conditions which imply absence of …run-time errors. Show more

Keywords: meta-variables, ambivalent syntax, Prolog programs, soundness and completeness, absence of errors

DOI: 10.3233/FI-1996-281202

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 23-36, 1996

Authors: Blair, Howard A.

Article Type: Research Article

Abstract: Given a binary recursively enumerable relation R, one or more logic programs over a language L can be constructed and interconnected to produce a dependency relation D on selected predicates within the Herbrand base BL of L isomorphic to R. D can be, optionally, a positive, negative or mixed dependency relation. The construction is applied to representing any effective game of the type introduced by Gurevich and Harrington, which they used to prove Rabin's decision method for S2S, as the dependency relation of a logic program. We allow games over an infinite alphabet of possible moves. We use this …representation to reveal a common underlying reason, having to do with the shape of a program's dependency relation, for the complexity of several logic program properties. Show more

Keywords: logic program, dependency relation, game, complexity

DOI: 10.3233/FI-1996-281203

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 37-54, 1996

Authors: Blikle, Andrzej

Article Type: Research Article

Abstract: This is an essay where the author expresses his views on applied denotational semantics. In the author's opinion, whether a software system has or does not have a sufficiently abstract denotational semantics should be regarded as a pragmatic attribute of the system rather than merely as a mathematical attribute of its description. In a software system with denotational semantics structured programming is feasible and for such systems there is a routine method of developing program-correctness logic. All that may not be the case if denotationality is not ensured. On the other hand, a non-denotational semantics can be always artificially made …denotational on the expense of lowering its level of abstraction. This leads to an important pragmatic question: to what extent and in which situations can we sacrifice denotationality and/or abstraction of a semantics? All discussions are carried on an algebraic ground but the paper is not very technical and contains a short introduction to the algebraic theory of denotational semantics. Show more

DOI: 10.3233/FI-1996-281204

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 55-85, 1996

Authors: Dix, Jürgen | Gottlob, Georg | Marek, Wiktor

Article Type: Research Article

Abstract: It is wellknown that Minker's semantics GCWA for positive disjunctive programs P, i.e. to decide if a literal is true in all minimal models of P is ΠP2 -complete. This is in contrast to the same entailment problem for semantics of non-disjunctive programs such as STABLE and SUPPORTED (both are co-NP-complete) as well as MsuppP and WFS (that are even polynomial). Recently, the idea of reducing disjunctive to non-disjunctive programs by using so called shift-operations was introduced independently by Bonatti, Dix/Gottlob/Marek, and Schaerf. In fact, Schaerf associated to each semantics SEM for normal programs a corresponding semantics …Weak-SEM for disjunctive programs and asked for the properties of these weak semantics, in particular for the complexity of their entailment relations. While Schaerf concentrated on Weak-STABLE and Weak-SUPPORTED, we investigate the weak versions of Apt/Blair/Walker's stratified semantics MsuppP and of Van Gelder/Ross/Schlipf's well-founded semantics WFS. We show that credulous entailment for both semantics is NP-complete (consequently, sceptical entailment is co-NP-complete). Thus, unlike GCWA, the complexity of these semantics belongs to the first level of the polynomial hierarchy. Note that, unlike Weak-WFS, the semantics Weak-MsuppP is not always defined: testing consistency of Weak-MsuppP is also NP–complete. We also show that Weak-WFS and Weak-MsuppP are cumulative and rational and that., in addition, Weak-WFS satisfies some of the well-behaved principles introduced by Dix. Show more

Keywords: Disjunctive Logic Programming, Semantics, Complexity, Abstract Properties

DOI: 10.3233/FI-1996-281205

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 87-100, 1996

Authors: Fitting, Melvin

Article Type: Research Article

Abstract: We state and prove a modal Herbrand theorem that is, we believe, a more natural analog of the classical version than has appeared before. The statement itself requires the enlargement of the usual machinery of first-order modal logic—we use the device of predicate abstraction, something that has been considered elsewhere as well. This expands the expressive power of modal logic in a natural way. Our proof of the modal version of Herbrand's theorem uses a tableau system that takes predicate abstraction into account. It is somewhat simpler than other systems for the same purpose that have previously appeared.

DOI: 10.3233/FI-1996-281206

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 101-122, 1996

Authors: Gottlob, Georg | Truszczyński, Mirosław

Article Type: Research Article

Abstract: In this paper we investigate the complexity of problems concerned with approximating the stable model semantics. We show that under rather weak assumptions it is NP-hard to decide whether the size of a polynomially computable approximation is within a constant factor from the size of the intersection (union) of stable models of a program. We also show that unless P=NP, no approximation exists that uniformly bounds the intersection (union) of stable models.

Keywords: Logic programming, stable models, well-founded semantics, computational complexity

DOI: 10.3233/FI-1996-281207

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 123-128, 1996

Authors: Hsiang, Jieh | Wasilewska, Anita

Article Type: Research Article

Abstract: We present here an effective proof theory that allows one to reason within algebras of algebraic logic in a purely syntactic, algebraic fashion. We demonstrate the effectiveness of the method by discussing our automated proofs of problems and theorems taken from Professor Helena Rasiowa's book An Algebraic Approach to Non-Classical Logics, Studies in Logic and Fundation of Mathematics, Volume 78, North Holland Publishing Company, Amsterdam, London - PWN, Warsaw (1974). We include a detailed proof of a problem presented to us by Professor Helena Rasiowa in June 1993. Most of these proofs are the first direct proofs ever discovered, and …they are produced by the computer without human assistance. Show more

DOI: 10.3233/FI-1996-281208

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 129-140, 1996

Authors: Mirkowska, Grazyna | Salwicki, Andrzej

Article Type: Research Article

Abstract: It is commonly believed that a programmable model satisfying the axioms of a given algebraic specification guarantees good properties and is a correct implementation of the specification. This convinction might be related to the Tennenbaum's property[Ten] of the arithmetic: every computable model of the Peano arithmetic of natural numbers is isomorphic to the standard model. Here, on the example of stacks, we show a model satisfying all axioms of the algebraic specification of stacks which can not be accepted as a good model in spite of the fact that it is defined by a program. For it enables to ”pop” …a stack infinitely many times. Show more

DOI: 10.3233/FI-1996-281209

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 141-152, 1996

Authors: Plaza, Jan A.

Article Type: Research Article

Abstract: We present an approach to foundations of logic programming in which the connection with algebraic semantics becomes apparent. The approach is based on omega-Herbrand models instead of conventional Herbrand models. We give a proof of Clark's theorem on completeness of SLD-resolution by methods of the algebraic semantics. We prove the existence property for definite programs.

Keywords: Rasiowa-Sikorski lemma, algebraic semantics, logic programming, completeness of SLD-resolution

DOI: 10.3233/FI-1996-281210

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 153-164, 1996

Authors: Pratt, Vaughan | Tiuryn, Jerzy

Article Type: Research Article

Abstract: We consider tractable and intractable cases of the satisfiability problem for conjunctions of inequalities between variables and constants in a fixed finite poset. We show that crowns are intractable. We study members and closure properties of the class of tractable posets. We define a feasible poset to be one whose potential obstacles to satisfiability are representable by a certain formula of the first-order extended by the least fixed operator. For bipartite posets we give a complete classification of hard posets and feasible ones.

DOI: 10.3233/FI-1996-281211

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 165-182, 1996

Authors: Trakhtenbrot, B.A.

Article Type: Research Article

DOI: 10.3233/FI-1996-281212

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 183-195, 1996

Authors: Urzyczyn, Paweł

Article Type: Research Article

Abstract: We consider several different definitions of type assignment with positive recursive types, from the point of view of their typing ability. We discuss the relationships between these systems. In particular, we show that the class of typable pure lambda terms remains the same for different type disciplines involving positive type fixpoints, and that type reconstruction is decidable.

Keywords: Lambda calculus, positive recursive types, type constraints

DOI: 10.3233/FI-1996-281213

Citation: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 197-209, 1996