Switch to: References

Add citations

You must login to add citations.
  1. On the Elementary Theory of Banach Algebras.Angus Macintyre - 1971 - Annals of Pure and Applied Logic 3 (3):239.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • The Monadic Second-Order Logic of Graphs IV: Definability Properties of Equational Graphs.Bruno Courcelle - 1990 - Annals of Pure and Applied Logic 49 (3):193.
  • A Uniform Method for Proving Lower Bounds on the Computational Complexity of Logical Theories.Kevin J. Compton & C. Ward Henson - 1990 - Annals of Pure and Applied Logic 48 (1):1.
    A new method for obtaining lower bounds on the computational complexity of logical theories is presented. It extends widely used techniques for proving the undecidability of theories by interpreting models of a theory already known to be undecidable. New inseparability results related to the well known inseparability result of Trakhtenbrot and Vaught are the foundation of the method. Their use yields hereditary lower bounds . By means of interpretations lower bounds can be transferred from one theory to another. Complicated machine (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  • Deciding the Unguarded Modal -Calculus.Oliver Friedmann & Martin Lange - 2013 - Journal of Applied Non-Classical Logics 23 (4):353-371.
    The modal -calculus extends basic modal logic with second-order quantification in terms of arbitrarily nested fixpoint operators. Its satisfiability problem is EXPTIME-complete. Decision procedures for the modal -calculus are not easy to obtain though since the arbitrary nesting of fixpoint constructs requires some combinatorial arguments for showing the well-foundedness of least fixpoint unfoldings. The tableau-based decision procedures so far also make assumptions on the unfoldings of fixpoint formulas, e.g., explicitly require formulas to be in guarded normal form. In this paper (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Monadic Generalized Spectra.Ronald Fagin - 1975 - Mathematical Logic Quarterly 21 (1):89-96.
  • Separation Logics and Modalities: A Survey.Stéphane Demri & Morgan Deters - 2015 - Journal of Applied Non-Classical Logics 25 (1):50-99.
    Like modal logic, temporal logic, and description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Model-Theoretic Complexity of Automatic Structures.Bakhadyr Khoussainov & Mia Minnes - 2009 - Annals of Pure and Applied Logic 161 (3):416-426.
  • Combining Temporal Logic Systems.Marcelo Finger & Dov Gabbay - 1996 - Notre Dame Journal of Formal Logic 37 (2):204-232.
    This paper investigates modular combinations of temporal logic systems. Four combination methods are described and studied with respect to the transfer of logical properties from the component one-dimensional temporal logics to the resulting combined two-dimensional temporal logic. Three basic logical properties are analyzed, namely soundness, completeness, and decidability. Each combination method comprises three submethods that combine the languages, the inference systems, and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional temporal languages with varying expressivity and varying (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  • Temporal Logics of Agency.Johan van Benthem & Eric Pacuit - 2010 - Journal of Logic, Language and Information 19 (4):389-393.
  • Propositional Quantification in the Topological Semantics for S.Philip Kremer - 1997 - Notre Dame Journal of Formal Logic 38 (2):295-313.
    Fine and Kripke extended S5, S4, S4.2 and such to produce propositionally quantified systems , , : given a Kripke frame, the quantifiers range over all the sets of possible worlds. is decidable and, as Fine and Kripke showed, many of the other systems are recursively isomorphic to second-order logic. In the present paper I consider the propositionally quantified system that arises from the topological semantics for S4, rather than from the Kripke semantics. The topological system, which I dub , (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Book Reviews. [REVIEW][author unknown] - 2002 - History and Philosophy of Logic 23 (1):51-76.
    Direct download  
     
    Export citation  
     
    Bookmark  
  • A System of Dynamic Modal Logic.Maarten de Rijke - 1998 - Journal of Philosophical Logic 27 (2):109-142.
    In many logics dealing with information one needs to make statements not only about cognitive states, but also about transitions between them. In this paper we analyze a dynamic modal logic that has been designed with this purpose in mind. On top of an abstract information ordering on states it has instructions to move forward or backward along this ordering, to states where a certain assertion holds or fails, while it also allows combinations of such instructions by means of operations (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Decidability of Quantified Propositional Intuitionistic Logic and S4 on Trees of Height and Arity ≤Ω.Richard Zach - 2004 - Journal of Philosophical Logic 33 (2):155-164.
    Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers ∀p, ∃p, where the propositional variables range over upward-closed subsets of the set of worlds in a Kripke structure. If the permitted accessibility relations are arbitrary partial orders, the resulting logic is known to be recursively isomorphic to full second-order logic (Kremer, 1997). It is shown that if the Kripke structures are restricted to trees of at height and width at most ω, the resulting logics are decidable. (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  • A First-Order Axiomatization of the Theory of Finite Trees.Rolf Backofen, James Rogers & K. Vijay-Shanker - 1995 - Journal of Logic, Language and Information 4 (1):5-39.
    We provide first-order axioms for the theories of finite trees with bounded branching and finite trees with arbitrary (finite) branching. The signature is chosen to express, in a natural way, those properties of trees most relevant to linguistic theories. These axioms provide a foundation for results in linguistics that are based on reasoning formally about such properties. We include some observations on the expressive power of these theories relative to traditional language complexity classes.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  • Quantification Over Sets of Possible Worlds in Branching-Time Semantics.Alberto Zanardo - 2006 - Studia Logica 82 (3):379-400.
    Temporal logic is one of the many areas in which a possible world semantics is adopted. Prior's Ockhamist and Peircean semantics for branching-time, though, depart from the genuine Kripke semantics in that they involve a quantification over histories, which is a second-order quantification over sets of possible worlds. In the paper, variants of the original Prior's semantics will be considered and it will be shown that all of them can be viewed as first-order counterparts of the original semantics.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Modal Logic of Time Division.Tero Tulenheimo - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 363-387.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Model Theory for Tense Logics.Dov M. Gabbay - 1975 - Annals of Pure and Applied Logic 8 (1):185.
  • Decidability Results in Non-Classical Logics. Part I.Dov M. Gabbay - 1975 - Annals of Mathematical Logic 8 (3):237.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  • Automata and Logics Over Finitely Varying Functions.Fabrice Chevalier, Deepak D’Souza, M. Raj Mohan & Pavithra Prabhakar - 2009 - Annals of Pure and Applied Logic 161 (3):324-336.
    We extend some of the classical connections between automata and logic due to Büchi [5] and McNaughton and Papert [12] to languages of finitely varying functions or “signals”. In particular, we introduce a natural class of automata for generating finitely varying functions called ’s, and show that it coincides in terms of language definability with a natural monadic second-order logic interpreted over finitely varying functions Rabinovich [15]. We also identify a “counter-free” subclass of ’s which characterise the first-order definable languages (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  • Computability. Computable Functions, Logic, and the Foundations of Mathematics. [REVIEW]R. Zach - 2002 - History and Philosophy of Logic 23 (1):67-69.
    Epstein and Carnielli's fine textbook on logic and computability is now in its second edition. The readers of this journal might be particularly interested in the timeline `Computability and Undecidability' added in this edition, and the included wall-poster of the same title. The text itself, however, has some aspects which are worth commenting on.
    Direct download  
     
    Export citation  
     
    Bookmark  
  • Decidable Fragments of First-Order Temporal Logics.Ian Hodkinson, Frank Wolter & Michael Zakharyaschev - 2000 - Annals of Pure and Applied Logic 106 (1-3):85-134.
    In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  • Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems.Bruno Courcelle & Igor Walukiewicz - 1998 - Annals of Pure and Applied Logic 92 (1):35-62.
    We prove that every monadic second-order property of the unfolding of a transition system is a monadic second-order property of the system itself. An unfolding is an instance of the general notion of graph covering. We consider two more instances of this notion. A similar result is possible for one of them but not for the other.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • The Structure of the Models of Decidable Monadic Theories of Graphs.D. Seese - 1991 - Annals of Pure and Applied Logic 53 (2):169-195.
    In this article the structure of the models of decidable monadic theories of planar graphs is investigated. It is shown that if the monadic theory of a class K of planar graphs is decidable, then the tree-width in the sense of Robertson and Seymour of the elements of K is universally bounded and there is a class T of trees such that the monadic theory of K is interpretable in the monadic theory of T.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Moderate Families in Boolean Algebras.Lutz Heindorf - 1992 - Annals of Pure and Applied Logic 57 (3):217-250.
    Heidorf, L., Moderate families in Boolean algebras, Annals of Pure and Applied Logic 57 217–250. A subset F of a Boolean algebra B will be called moderate if no element of B splits infinitely many elements of F . Disjoint moderate sets occur in connection with a product construction that is systematically studied in this paper. In contrast to the usual full direct product, these so-called moderate products preserve many properties of their factors. This can be used, for example, to (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Recursive Unary Algebras and Trees.Bakhadyr Khoussainov - 1994 - Annals of Pure and Applied Logic 67 (1-3):213-268.
    A unary algebra is an algebraic system A = , where ƒ 0 ,…,ƒ n are unary operations on A and n ∈ ω. In the paper we develop the theory of effective unary algebras. We investigate well-known questions of constructive model theory with respect to the class of unary algebras. In the paper we construct unary algebras with a finite number of recursive isomorphism types. We give the notions of program, uniform, and algebraic dimensions of models, and then we (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Progress Measures, Immediate Determinacy, and a Subset Construction for Tree Automata.Nils Klarlund - 1994 - Annals of Pure and Applied Logic 69 (2-3):243-268.
    Using the concept of progress measure, we give a new proof of Rabin's fundamental result that the languages defined by tree automata are closed under complementation. To do this we show that for certain infinite games based on tree automata, an immediate determinacy property holds for the player who is trying to win according to a Rabin acceptance condition. Immediate determinancy is stronger than the forgetful determinacy of Gurevich and Harrington, which depends on more information about the past, but applies (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Thue Trees.Jerzy Marcinkowski & Leszek Pacholski - 2003 - Annals of Pure and Applied Logic 119 (1-3):19-59.
    In this paper we introduce a new technique of proving undecidability results. This technique is based on the notion of a Thue tree. We also give examples of applications of this method to term rewriting, Horn implication problem and database dependencies.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Monadic Theory of Order and Topology in ZFC.Yuri Gurevich & Saharon Shelah - 1982 - Annals of Mathematical Logic 23 (2-3):179-198.
  • Recursive Categoricity and Recursive Stability.John N. Crossley, Alfred B. Manaster & Michael F. Moses - 1986 - Annals of Pure and Applied Logic 31 (2):191-204.
  • Algorithmic Uses of the Feferman–Vaught Theorem.J. A. Makowsky - 2004 - Annals of Pure and Applied Logic 126 (1-3):159-213.
    The classical Feferman–Vaught Theorem for First Order Logic explains how to compute the truth value of a first order sentence in a generalized product of first order structures by reducing this computation to the computation of truth values of other first order sentences in the factors and evaluation of a monadic second order sentence in the index structure. This technique was later extended by Läuchli, Shelah and Gurevich to monadic second order logic. The technique has wide applications in decidability and (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • Simple Monadic Theories and Partition Width.Achim Blumensath - 2011 - Mathematical Logic Quarterly 57 (4):409-431.
    We study tree-like decompositions of models of a theory and a related complexity measure called partition width. We prove a dichotomy concerning partition width and definable pairing functions: either the partition width of models is bounded, or the theory admits definable pairing functions. Our proof rests on structure results concerning indiscernible sequences and finitely satisfiable types for theories without definable pairing functions. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  • Relating Word and Tree Automata.Orna Kupferman, Shmuel Safra & Moshe Y. Vardi - 2006 - Annals of Pure and Applied Logic 138 (1):126-146.
    In the automata-theoretic approach to verification, we translate specifications to automata. Complexity considerations motivate the distinction between different types of automata. Already in the 60s, it was known that deterministic Büchi word automata are less expressive than nondeterministic Büchi word automata. The proof is easy and can be stated in a few lines. In the late 60s, Rabin proved that Büchi tree automata are less expressive than Rabin tree automata. This proof is much harder. In this work we relate the (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  • Succinct Definitions in the First Order Theory of Graphs.Oleg Pikhurko, Joel Spencer & Oleg Verbitsky - 2006 - Annals of Pure and Applied Logic 139 (1):74-109.
    We say that a first order sentence A defines a graph G if A is true on G but false on any graph non-isomorphic to G. Let L ) denote the minimum length of such a sentence. We define the succinctness function s ) to be the minimum L ) over all graphs on n vertices.We prove that s and q may be so small that for no general recursive function f we can have f)≥n for all n. However, for (...))
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Logical Aspects of Cayley-Graphs: The Group Case.Dietrich Kuske & Markus Lohrey - 2004 - Annals of Pure and Applied Logic 131 (1):263-286.
    We prove that a finitely generated group is context-free whenever its Cayley-graph has a decidable monadic second-order theory. Hence, by the seminal work of Muller and Schupp, our result gives a logical characterization of context-free groups and also proves a conjecture of Schupp. To derive this result, we investigate general graphs and show that a graph of bounded degree with a high degree of symmetry is context-free whenever its monadic second-order theory is decidable. Further, it is shown that the word (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Entscheidbarkeit von Theorien in Logiken mit verallgemeinerten Quantoren.Heinrich Herre & Helmut Wolter - 1975 - Mathematical Logic Quarterly 21 (1):229-246.
    No categories
    Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  • On Vaught’s Conjecture and Finitely Valued MV Algebras.Antonio Di Nola & Giacomo Lenzi - 2012 - Mathematical Logic Quarterly 58 (3):139-152.
    We show that the complete first order theory of an MV algebra has equation image countable models unless the MV algebra is finitely valued. So, Vaught's Conjecture holds for all MV algebras except, possibly, for finitely valued ones. Additionally, we show that the complete theories of finitely valued MV algebras are equation image and that all ω-categorical complete theories of MV algebras are finitely axiomatizable and decidable. As a final result we prove that the free algebra on countably many generators (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  • Iterated Pushdown Automata and Sequences of Rational Numbers.Séverine Fratani & Géraud Sénizergues - 2006 - Annals of Pure and Applied Logic 141 (3):363-411.
  • The Complexity of Temporal Logic Over the Reals.Mark Reynolds - 2010 - Annals of Pure and Applied Logic 161 (8):1063-1096.
    It is shown that the decision problem for the temporal logic with until and since connectives over real-numbers time is PSPACE-complete. This is the most practically useful dense time temporal logic.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   6 citations