The logic of action lattices is undecidable
We prove algorithmic undecidability of the (in)equational theory of residuated Kleene lattices (action lattices), thus solving a problem left open by D. Kozen, P. Jipsen, W. Buszkowski.
The textbook contains the basic information of formal logical systems. It is Boolean functions, Post’s theorem on functional completeness, the k-valued logic, derivatives of Boolean functions, axiomatic calculi for propositions, for predicates, for sequentions, for resolutions. Programming language Prolog and axiomatic programming language OBJ3 are introduced. Problems of monadic logic, of finite automata and of the represented by them languages, of temporal logic are considered. Many examples are shown. It is put in a basis of the book long-term experience of teaching by authors the discipline «Discrete mathematics» at the business informatics faculty, at the computer science faculty of National research university Higher school of economics, and at the automatics and computer technique faculty of National research university Moscow power engineering institute. The book is intended for the students of a bachelor degree, trained at the computer science faculties in the directions 09.03.01 Informatics and computational technique, 09.03.02 Informational systems and technologies, 09.03.03 Applied informatics, 09.03.04 Software Engineering, and also for IT experts and developers of software products.
The book contains the necessary information from the algorithm theory, graph theory, combinatorics. It is considered partially recursive functions, Turing machines, some versions of the algorithms (associative calculus, the system of substitutions, grammars, Post's productions, Marcov's normal algorithms, operator algorithms). The main types of graphs are described (multigraphs, pseudographs, Eulerian graphs, Hamiltonian graphs, trees, bipartite graphs, matchings, Petri nets, planar graphs, transport nets). Some algorithms often used in practice on graphs are given. It is considered classical combinatorial configurations and their generating functions, recurrent sequences. It is put in a basis of the book long-term experience of teaching by authors the discipline «Discrete mathematics» at the business informatics faculty, at the computer science faculty of National Research University Higher School of Economics, and at the automatics and computer technique faculty of National research university Moscow power engineering institute. The book is intended for the students of a bachelor degree, trained at the computer science faculties in the directions 09.03.01 Informatics and computational technique, 09.03.02 Informational systems and technologies, 09.03.03 Applied informatics, 09.03.04 Software Engineering, and also for IT experts and developers of software products.
In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model is undecidable even for purely propositional formulas in this language.
The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models.
Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained.
In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI.
Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called “Minimal Boolean BI”, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete.
All of our undecidability results are obtained by means of a direct encoding of Minsky machines.
Key Words and Phrases: Separation logic, undecidability, memory models, bunched logic
Language and relational models, or L-models and R-models, are two natural classes of models for the Lambek calculus. Completeness w.r.t. L-models was proved by Pentus and completeness w.r.t. R-models by Andréka and Mikulás. It is well known that adding both additive conjunction and disjunction together yields incompleteness, because of the distributive law. The product-free Lambek calculus enriched with conjunction only, however, is complete w.r.t. L-models (Buszkowski) as well as R-models (Andréka and Mikulás). The situation with disjunction turns out to be the opposite: we prove that the product-free Lambek calculus enriched with disjunction only is incomplete w.r.t. L-models as well as R-models. If the empty premises are allowed, the product-free Lambek calculus enriched with conjunction only is still complete w.r.t. L-models but in which the empty word is allowed. Both versions are decidable (PSPACE-complete in fact). Adding the multiplicative unit to represent explicitly the empty word within the L-model paradigm changes the situation in a completely unexpected way. Namely, we prove undecidability for any L-sound extension of the Lambek calculus with conjunction and with the unit, whenever this extension includes certain L-sound rules for the multiplicative unit, to express the natural algebraic properties of the empty word. Moreover, we obtain undecidability for a small fragment with only one implication, conjunction, and the unit, obeying these natural rules. This proof proceeds by the encoding of two-counter Minsky machines.
We consider the quantifier-free languages, Bc and Bc°, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of Rn (n ≥ 2) and, additionally, over the regular closed semilinear sets of Rn. The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric Qualitative Spatial Reasoning. We prove that the satisfiability problem for Bc is undecidable over the regular closed semilinear sets in all dimensions greater than 1, and that the satisfiability problem for Bc and Bc° is undecidable over both the regular closed sets and the regular closed semilinear sets in the Euclidean plane. However, we also prove that the satisfiability problem for Bc° is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed semilinear sets is ExpTime-complete. Our results show, in particular, that spatial reasoning is much harder over Euclidean spaces than over arbitrary topological spaces.
Modal logics, both propositional and predicate, have been used in computer science since the late 1970s. One of the most important properties of modal logics of relevance to their applications in computer science is the complexity of their satisﬁability problem. The complexity of satisﬁability for modal logics is rather high: it ranges from NP-complete to undecidable for propositional logics and is undecidable for predicate logics. This has, for a long time, motivated research in drawing the borderline between tractable and intractable fragments of propositional modal logics as well as between decidable and undecidable fragments of predicate modal logics. In the present thesis, we investigate some very natural restrictions on the languages of propositional and predicate modal logics and show that placing those restrictions does not decrease complexity of satisﬁability. For propositional languages, we consider restricting the number of propositional variables allowed in the construction of formulas, while for predicate languages, we consider restricting the number of individual variables as well as the number and arity of predicate letters allowed in the construction of formulas. We develop original techniques, which build on and develop the techniques known from the literature, for proving that satisﬁability for a ﬁnite-variable fragment of a propositional modal logic is as computationally hard as satisﬁability for the logic in the full language and adapt those techniques to predicate modal logics and prove undecidability of fragments of such logics in the language with a ﬁnite number of unary predicate letters as well as restrictions on the number of individual variables. The thesis is based on four articles published or accepted for publication. They concern propositional dynamic logics, propositional branchingand alternating-time temporal logics, propositional logics of symmetric rela tions, and ﬁrst-order predicate modal and intuitionistic logics. In all cases, we identify the “minimal,” with regard to the criteria mentioned above, fragments whose satisﬁability is as computationally hard as satisﬁability for the entire logic.
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called “Lambek’s restriction,” that is, the antecedent of any provable sequent should be non-empty. In this paper we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. We present several versions of the Lambek calculus extended with exponential modalities and prove that those extensions are undecidable, even if we take only one of the two divisions provided by the Lambek calculus.