Superposition as a Decision Procedure for Timed Automata

The success of superposition-based theorem proving in first-order logic relies in particular on the fact that the superposition calculus can be turned into a decision procedure for various decidable fragments of first-order logic and has been successfully used to identify new decidable classes. In this paper, we extend this story to the hierarchic combination of linear arithmetic and first-order superposition. We show that decidability of reachability in timed automata can be obtained by instantiation of an abstract termination result for SUP(LA), the hierarchic combination of linear arithmetic and first-order superposition.     

The Degree of Decidable Categoricity of a Model with Infinite Solutions for Complete Formulas

Algebra and Logic - We construct a decidable prime model in which the degree of a set of complete formulas is equal to 0', infinitely many tuples of elements comply with every complete formula,...     

Certain Partial Conservativeness Properties of Intuitionistic Set Theory with the Principle of Double Complement of Sets

The Zermelo–Fraenkel set theory with the underlying intuitionistic logic (for brevity, we refer to it as the intuitionistic Zermelo–Fraenkel set theory) in a two-sorted language (where the sort 0 is assigned to numbers and the sort 1, to sets) with the collection scheme used as the replacement scheme of axioms (the ZFI2C theory) is considered. Some partial conservativeness properties of the intuitionistic Zermelo–Fraenkel set theory with the principle of double complement of sets (DCS) with respect to a certain class of arithmetic formulas (the class all so-called AEN formulas) are proved. Namely, let T be one of the theories ZFI2C and ZFI2C + DCS. Then (1) the theory T+ECT is conservative over T with respect to the class of AEN formulas; (2) the theory T+ECT+M is conservative over T+M{su?} with respect to the class of AEN formulas. Here ECT stands for the extended Church’s thesis, Mis the strong Markov principle, and M{su?} is the weak Markov principle. The following partial conservativeness properties are also proved: (3) T+ECT+M is conservative over T with respect to the class of negative arithmetic formulas; (4) the classical theory ZF2 is conservative over ZFI2C with respect to the class of negative arithmetic formulas.     

The completeness of Peano multiplication

It is shown that the set of all theorems of Peano Arithmetic which mention only multiplication is a complete theory in the corresponding restricted language. The notion of a complete decidable covering of a theory is introduced. The author was partially supported by N.S.F. Grant No. MC578-02224.     

Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic

A saturated calculus for the so-called Horn-like sequents of a complete class of a linear temporal logic of the first order is described. The saturated calculus contains neither induction-like postulates nor cut-like rules. Instead of induction-like postulates the saturated calculus contains a finite set of “saturated” sequents, which (1) capture and reflect the periodic structure of inductive reasoning (i.e., a reasoning which applies induction-like postulates); (2) show that “almost nothing new” can be obtained by continuing the process of derivation of a given sequent; (3) present an explicit way of generating the so-called invariant formula in induction-like rules. The saturated calculus for Horn-like sequents allows one: (1) to prove in an obvious way the completeness of a restricted linear temporal logic of the first order; (2) to construct a computer-aided proof system for this logic; (3) to prove the decidability of this logic for logically decidable Horn-like sequents. Bibliography: 15 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 220, 1995, pp. 123–144. Translated by R. Pliuškevičius.     

Countably categorical theories

A series of countably categorical theories are constructed based on the Fra?sse method. In particular, an example of a decidable countably categorical theory in a finite signature is given for which no decidable model has an infinite computable set of order indiscernibles. Such a theory is used to refute Ershov’s conjecture on the representability of models of c-simple theories over linear orders.     

Distributive lattices with a decidable monadic second order theory

A class of finite distributive lattices has a decidable monadic second order theory iff (a) the join irreducible elements of its members have a decidable monadic second order theory, and (b) the width of the lattices is bounded. Similar results are obtained for the monadic chain and the monadic antichain theory where quantification is restricted to chains and antichains, resp. Furthermore, there is no (up to finite difference) maximal set of finite distributive lattices with a decidable monadic (chain or antichain, resp.) theory. Received December 6, 2000; accepted in final form May 30, 2002.     

Temporal logic of linearly ordered <Emphasis Type="Italic">α</Emphasis>-spaces

Using the language of temporal logic, we construct a decidable calculus L* α and prove that the calculus is complete w.r.t. the class of all strictly linearly ordered α-frames. Supported by RFBR (project No. 06-01-00358) and by the Council for Grants (under RF President) and State Aid of Leading Scientific Schools (grant NSh-335.2008.1). __________ Translated from Algebra i Logika, Vol. 47, No. 6, pp. 723–749, November–December, 2008.     

Hierarchic Markov processes and their applications in replacement models

In this paper a new notion of a hierarchic Markov process is introduced. It is a series of Markov decision processes called subprocesses built together in one Markov decision process called the main process. The hierarchic structure is specially designed to fit replacement models which in the traditional formulation as ordinary Markov decision processes are usually very large. The basic theory of hierarchic Markov processes is described and examples are given of applications in replacement models. The theory can be extended to fit a situation where the replacement decision depends on the quality of the new asset available for replacement.     

The polynomial bounds of proof complexity in Frege systems

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.     

Automata transformations of prefix decidable and decidable by Buchi superwords

We show that the set of prefix decidable superwords is closed under finite automata and asynchronous automata transformations. We prove that structures of degrees of finite automata and asynchronous automata transformations contain an atom which consists of prefix decidable superwords with undecidable monadic theory (or undecidable by Buchi). Also we prove that the structure of degrees of asynchronous automata transformations contains an atom which consists of superwords with decidable monadic theory (decidable by Buchi).     

Positive Presentations of Families Relative to <Emphasis Type="Italic">e</Emphasis>-Oracles

We introduce the notion of A-numbering which generalizes the classical notion of numbering. All main attributes of classical numberings are carried over to the objects considered here. The problem is investigated of the existence of positive and decidable computable A-numberings for the natural families of sets e-reducible to a fixed set. We prove that, for every computable A-family containing an inclusion-greatest set, there also exists a positive computable A-numbering. Furthermore, for certain families we construct a decidable (and even single-valued) computable total A-numbering when A is a low set; we also consider a relativization containing all cases of total sets (this in fact corresponds to computability with a usual oracle).     

一种基于集对分析的模糊多属性决策方法

针对属性权重和决策矩阵的属性值均为梯形模糊数的模糊多属性决策问题,提出了一种基于集对分析的决策方法.方法具有如下特点:通过借鉴集对分析理论和论域三划分的思想,把梯形模糊数属性值转化成联系数的形式,能有效处理决策过程中的不确定因素;对于权重向量和决策矩阵中的梯形模糊数采取不同的处理方法;用联系数决策理论的概念来刻画备选方案与正、负理想方案组成集对的同一对立程度;基于可能势的联系数排序能够准确反映联系数间的同一对立程度,方法直观,概念明确,易于实际操作.实例计算表明,方法是求解模糊多属性决策问题的一种有效工具.     

Some Decidability Results for ℤ[G]-Modules when G is Cyclic of Squarefree Order

We extend the analysis of the decision problem for modules over a group ring ?[G] to the case when G is a cyclic group of squarefree order. We show that separated ?[G]-modules have a decidable theory, and we discuss the model theoretic role of these modules within the class of all ?[G]-modules. The paper includes a short analysis of the decision problem for the theories of (finitely generated) modules over ?[ζ_m], where m is a positive integer and ζ_m is a primitive mth root of 1. Mathematics Subject Classification: 03C60, 03B25.     

Algebraic geometry in first-order logic

In every variety of algebras Θ, we can consider its logic and its algebraic geometry. In previous papers, geometry in equational logic, i.e., equational geometry, has been studied. Here we describe an extension of this theory to first-order logic (FOL). The algebraic sets in this geometry are determined by arbitrary sets of FOL formulas. The principal motivation of such a generalization lies in the area of applications to knowledge science. In this paper, the FOL formulas are considered in the context of algebraic logic. For this purpose, we define special Halmos categories. These categories in algebraic geometry related to FOL play the same role as the category of free algebras Θ⁰ play in equational algebraic geometry. This paper consists of three parts. Section 1 is of introductory character. The first part (Secs. 2–4) contains background on algebraic logic in the given variety of algebras Θ. The second part is devoted to algebraic geometry related to FOL (Secs. 5–7). In the last part (Secs. 8–9), we consider applications of the previous material to knowledge science. __________ Translated from Sovremennaya Matematika i Ee Prilozheniya (Contemporary Mathematics and Its Applications), Vol. 22, Algebra and Geometry, 2004.     

CCC forcing and splitting reals

The results of this paper were motivated by a problem of Prikry who asked if it is relatively consistent with the usual axioms of set theory that every nontrivial ccc forcing adds a Cohen or a random real. A natural dividing line is into weakly distributive posets and those which add an unbounded real. In this paper I show that it is relatively consistent that every nonatomic weakly distributive ccc complete Boolean algebra is a Maharam algebra, i.e. carries a continuous strictly positive submeasure. This is deduced from theP-ideal dichotomy, a statement which was first formulated by Abraham and Todorcevic [AT] and later extended by Todorcevic [T]. As an immediate consequence of this and the proof of the consistency of theP-ideal dichotomy we obtain a ZFC result which says that every absolutely ccc weakly distributive complete Boolean algebra is a Maharam algebra. Using a previous theorem of Shelah [Sh1] it also follows that a modified Prikry conjecture holds in the context of Souslin forcing notions, i.e. every nonatomic ccc Souslin forcing either adds a Cohen real or its regular open algebra is a Maharam algebra. Finally, I also show that every nonatomic Maharam algebra adds a splitting real, i.e. a set of integers which neither contains nor is disjoint from an infinite set of integers in the ground model. It follows from the result of [AT] that it is consistent relative to the consistency of ZFC alone that every nonatomic weakly distributive ccc forcing adds a splitting real.     

On the λY calculus

The λY calculus is the simply typed λ calculus augmented with the fixed point operators. We show three results about λY: (a) the word problem is undecidable, (b) weak normalisability is decidable, and (c) higher type fixed point operators are not definable from fixed point operators at smaller types.     

The logical representation of extensive games

Given an extensive formG, we associate with every choice an atomic sentence and with every information set a set of well-formed formulas (wffs) of prepositional calculus. The set of such wffs is denoted by Γ(G). Using the so-called topological semantics for propositional calculus (which differs from the standard one based on truth tables), we show that the extensive form yields a topological model of Γ(G), that is, every wff in Γ(G), is “true in G”. We also show that, within the standard truth-table semantics for propositional calculus, there is a one-to-one and onto correspondence between the set of plays ofG and the set of valuations that satisfy all the wffs in Γ(G).