Fundamenta Informaticae - Volume 79, issue 1-2

Authors: Bell, Paul

Article Type: Research Article

Abstract: We consider decidability questions for the emptiness problem of intersections of matrix semigroups. This problem was studied by A. Markov [7] and more recently by V. Halava and T. Harju [5]. We give slightly strengthened results of their theorems by using a different matrix encoding. In particular, we show that given two finitely generated semigroups of non-singular upper triangular 3 × 3 matrices over the natural numbers, checking the emptiness of their intersections is undecidable. We …also show that the problem is undecidable even for unimodular matrices over 3 × 3 rational matrices. Show more

Keywords: Matrix Semigroups, Semigroup Intersection, Undecidability

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 1-4, 2007

Authors: Cowen, Robert | Kolany, Adam

Article Type: Research Article

Abstract: Two set systems E, F on an underlying set V will be said to have Property S if there exists a subset σ of V , such that σ∩ e ≠Ø, for all e ∈ E and f ⊈σ, for all f ∈ F (see [8], [9]]). We give rules for deciding Property S, which generalizes the very successful Davis-Putnam rules for deciding satisfiability in propositional logic.

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 5-15, 2007

Authors: Chaitin, Gregory

Article Type: Research Article

Abstract: Using 1947 work of Post showing that the word problem for semigroups is unsolvable, we explicitly exhibit an algebraic characterization of the bits of the halting probability Ω. Our proof closely follows a 1978 formulation of Post's work by M. Davis. The proof is self-contained and not very complicated.

Keywords: Halting probability, word problem

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 17-23, 2007

Authors: Eiter, Thomas | Erdem, Esra | Faber, Wolfgang | Senko, Ján

Article Type: Research Article

Abstract: Consider an agent executing a plan with nondeterministic actions, in a dynamic environment, which might fail. Suppose that she is given a description of this action domain, including specifications of effects of actions, and a set of trajectories for the execution of this plan, where each trajectory specifies a possible execution of the plan in this domain. After executing some part of the plan, suppose that she obtains information about the current state of the world, …and notices that she is not at a correct state relative to the given trajectories. How can she find an explanation (a point of failure) for such a discrepancy? An answer to this question can be useful for different purposes. In the context of execution monitoring, points of failure can determine some checkpoints that specify when to check for discrepancies, and they can sometimes be used for recovering from discrepancies that cause plan failures. At the modeling level, points of failure may provide useful insight into the action domain for a better understanding of the domain, or reveal errors in the formalization of the domain. We study the question above in a general logic-based knowledge representation framework, which can accommodate nondeterminism and concurrency. In this framework, we define a discrepancy and an explanation for it, and analyze the computational complexity of detecting discrepancies and finding explanations for them. We introduce a method for computing explanations, and report about a realization of this method using DLV^K , which is a logic-programming based system for reasoning about actions and change. Show more

Keywords: knowledge representation, reasoning about actions, logic-based planning, explanations, execution monitoring, computational complexity

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 25-69, 2007

Authors: Herman, Grzegorz | Paterson, Tim | Soltys, Michael

Article Type: Research Article

Abstract: We introduce a new propositional proof system, which we call H, that allows quantification over permutations. In H we may write (∃ab)α and (∀ab)α, which is semantically equivalent to α(a,b)∨α(b,a) and α(a,b)∧ α(b,a), respectively. We show that H with cuts restricted to Σ_1 formulas (we denote this system H_1 ) simulates efficiently the Hajós calculus (HC) for constructing graphs which are non-3-colorable. This shows that short proofs over formulas …that assert the existence of permutations can capture polynomial time reasoning (as by [9], HC is equivalent in strength to EF, which in turn captures polytime reasoning). We also show that EF simulates efficiently H^*_1 , which is H_1 with proofs restricted to being tree-like. In short, we show that H^*_1 ⩽_p EF⩽_p H_1 . Show more

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 71-83, 2007

Authors: Nguyen, Linh Anh

Article Type: Research Article

Abstract: We give formulations for modal deductive databases and present a modal query language called MDatalog. We define modal relational algebras and give the seminaive evaluation algorithm, the top-down evaluation algorithm, and the magic-set transformation for MDatalog queries. The results of this paper like soundness and completeness of the top-down evaluation algorithm or correctness of the magic-set transformation are proved for the multimodal logics of belief KDI4_s 5, KDI45, KD4_s 5_s …, KD45_{(m)} , KD4I_g 5_a , and the class of serial context-free grammar logics. We also show that MDatalog has PTIME data complexity in the logics KDI4_s 5, KDI45, KD4_s 5_s , and KD45_{(m)} . Show more

Keywords: modal logics, deductive databases, modal logic programming, relational algebra, seminaive evaluation, query-subquery evaluation, magic-set transformation, data complexity

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 85-135, 2007

Authors: Rabinovich, Alexander

Article Type: Research Article

Abstract: Composition theorems are tools which reduce sentences about some compound structure to sentences about its parts. A seminal example of such a theorem is the Feferman-Vaught Theorem [3] which reduces the first-order theory of generalized products to the first order theory of its factors and the monadic second-order theory of index structure. Shelah [23] used the composition theorem for linear orders as one of the main tools for obtaining very strong decidability results for the …monadic second-order theory of linear orders. The main technical contribution of our paper is (1) a definition of a generalized sum of structures and (2) a composition theorem for first-order logic over the generalized sum. One of our objectives is to emphasize the work-out of the composition method. Show more

Keywords: Composition Theorem, first-order logic, expressibility, decidability

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 137-167, 2007

Authors: Sadowski, Zenon

Article Type: Research Article

Abstract: We advocate the thesis that the following general statements are equivalent: the existence of an optimal proof system, the existence of an optimal acceptor (an algorithm with optimality property stated only for input strings which are accepted), and the existence of a suitable recursive presentation of the class of all easy (polynomial-time recognizable) subsets of TAUT (SAT). We prove three concrete versions of this thesis with different variants of notions appearing in it. These versions give …alternative characterizations of the following problems: the existence of a p-optimal proof system for SAT, the existence of an optimal proof system for TAUT, and the existence of an optimal and automatizable proof system for TAUT. Show more

Keywords: abstract propositional proof systems, automatizable proof systems, recursive presentability, disjoint NP-pairs

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 169-185, 2007

Authors: Vennekens, Joost | Wittocx, Johan | Mariën, Maarten | Denecker, Marc

Article Type: Research Article

Abstract: We study the transformation of "predicate introduction" in non-monotonic logics. By this, we mean the act of replacing a complex formula by a newly defined predicate. From a knowledge representation perspective, such transformations can be used to eliminate redundancy or to simplify a theory. From a more practical point of view, they can also be used to transform a theory into a normal form imposed by certain inference programs or theorems. In this paper, we study …predicate introduction in the algebraic framework of "approximation theory"; this is a fixpoint theory for nonmonotone operators that generalizes all main semantics of various non-monotonic logics, including logic programming, default logic and autoepistemic logic. We prove an abstract, algebraic equivalence result in this framework. This can then be used to show that, in logic programming, certain transformations are equivalence preserving under, among others, both the stable and well-founded semantics. Based on this result, we develop a general method of eliminating universal quantifiers in the bodies of rules. Our work is, however, also applicable beyond logic programming. In a companion paper, we demonstrate this, by using the same algebraic results to derive a transformation which reduces the nesting depth of the modal operator K in autoepistemic logic. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 187-208, 2007

Authors: Vennekens, Joost | Wittocx, Johan | Mariën, Maarten | Denecker, Marc

Article Type: Research Article

Abstract: We study the transformation of "predicate introduction" in non-monotonic logics. By this, we mean the act of replacing a complex formula by a newly defined predicate. From a knowledge representation perspective, such transformations can be used to eliminate redundancy or to simplify a theory. From a more practical point of view, they can also be used to transform a theory into a normal form imposed by certain inference programs or theorems. In a companion paper, we …developed an algebraic theory that considers predicate introduction within the framework of "approximation theory", a fixpoint theory for non-monotone operators that generalizes all main semantics of various non-monotonic logics, including logic programming, default logic and autoepistemic logic. We then used these results to show that certain logic programming transformations are equivalence preserving under, among others, both the stable and well-founded semantics. In this paper, we now apply the same algebraic results to autoepistemic logic and prove that a transformation to reduce the nesting depth of modal operators is equivalence preserving under a family of semantics for this logic. This not only provides useful theorems for autoepistemic logic, but also demonstrates that our algebraic theory does indeed capture the essence of predicate introduction in a generally applicable way. Show more

Citation: Fundamenta Informaticae, vol. 79, no. 1-2, pp. 209-227, 2007