Search

We study the topological μ-calculus, based on both Cantor derivative and closure modalities, proving completeness, decidability, and finite model property over general topological spaces, as well as over T0 and TD spaces. We also investigate the relational μ-calculus, providing general completeness results for all natural fragments of the μ-calculus over many different classes of relational frames. Unlike most other such proofs for μ-calculi, ours is model theoretic, making an innovative use of a known method from modal logic (the 'final' submodel of the canonical model), which has the twin advantages of great generality and essential simplicity. [ABSTRACT FROM AUTHOR]

We prove that a plactic monoid of any finite rank has decidable first order theory. This resolves other open decidability problems about the finite rank plactic monoids, such as the Diophantine problem and identity checking. This is achieved by interpreting a plactic monoid of arbitrary rank in Presburger arithmetic, which is known to have decidable first order theory. We also prove that the interpretation of the plactic monoids into Presburger Arithmetic is in fact a bi-interpretation, hence any two plactic monoids of finite rank are bi-interpretable with one another. The algorithm generating the interpretations is uniform, which answers positively the decidability of the Diophantine problem for the infinite rank plactic monoid. [ABSTRACT FROM AUTHOR]

This paper offers a comprehensive retrospective on the development and results in the field of insertion-deletion systems over the past 15 years, building upon an earlier foundational overview from 2010. We review key theoretical developments, new extensions, and variations that have emerged, examining their impact on the computational power of insertion-deletion systems. This retrospective aims to update the field's understanding of the model, providing insights into the latest progress and identifying promising directions for future research. [ABSTRACT FROM AUTHOR]

This paper studies a combined system of intuitionistic and classical propositional logic from proof-theoretic viewpoints. Based on the semantic treatment of Humberstone (J Philos Log 8:171–196, 1979) and del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996), a sequent calculus G (C + J) is proposed. An approximate idea of obtaining G (C + J) is adding rules for classical implication on top of the intuitionistic multi-succedent sequent calculus by Maehara (Nagoya Math J 7:45–64, 1954). However, in the semantic treatment, some formulas do not satisfy heredity, which leads to the necessity of a restriction on the right rule for intuitionistic implication to keep the soundness of the calculus. The calculus G (C + J) enjoys cut elimination and Craig interpolation, whose detailed proofs are described in this paper. Cut elimination enables us to show the decidability of this combination both directly and syntactically. This paper also employs a canonical model argument to establish the strong completeness of Hilbert system C + J proposed by del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996). [ABSTRACT FROM AUTHOR]

We extend results of Vidaux and Videla concerning the set of Julia Robinson numbers.

This paper offers a comprehensive retrospective on the development and results in the field of insertion-deletion systems over the past 15 years, building upon an earlier foundational overview from 2010. We review key theoretical developments, new extensions, and variations that have emerged, examining their impact on the computational power of insertion-deletion systems. This retrospective aims to update the field's understanding of the model, providing insights into the latest progress and identifying promising directions for future research.

This paper extends the investigations into logical properties of the quantified argument calculus (Quarc) by suggesting a series of proper subsystems which, although retaining the entire vocabulary of Quarc, restrict quantification in such a way as to make the result decidable. The proof of decidability is via a procedure that prunes the infinite branches of a derivation tree in what is a syntactic counterpart of semantic filtration. We demonstrate an application of one of these systems by showing that Aristotle's assertoric syllogistic is embeddable within, thus also providing another method of showing its decidability. [ABSTRACT FROM AUTHOR]

We show that the finite sequentiality problem is decidable for finitely ambiguous max-plus tree automata. A max-plus tree automaton is a weighted tree automaton over the max-plus semiring. A max-plus tree automaton is called finitely ambiguous if the number of accepting runs on every tree is bounded by a global constant. The finite sequentiality problem asks whether for a given max-plus tree automaton, there exist finitely many deterministic max-plus tree automata whose pointwise maximum is equivalent to the given automaton. [ABSTRACT FROM AUTHOR]

Copyright of Transfer: Zeitschrift für Kommunikation & Markenmanagement is the property of Deutsche Werbewissenschaftliche Gesellschaft and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

AbstractThe “somewhat vague, intuitive” notion from computability theory of an effective procedure (method) or algorithm can be fairly precisely defined even if it is not sufficiently formal and precise to belong to mathematics proper (in a narrow sense)—and even if (as many have asserted) for that reason the Church–Turing thesis is unprovable. It is proved logically that the class of effective procedures is not decidable, i.e., that there is no effective procedure for ascertaining whether a given procedure is effective. This result is proved directly from the notion itself of an effective procedure, without reliance on any (partly) mathematical lemma, conjecture, or thesis invoking recursiveness or Turing-computability. In fact, there is no reliance on anything very mathematical. The proof does not even appeal to a precise definition of ‘effective procedure’. Instead, it relies solely and entirely on a basic grasp of the intuitive notion of an effective procedure. Though the result that effectiveness is undecidable is not surprising, it is also not without significance. It has the consequence, for example, that the solution to a decision problem, if it is to be complete, must be accompanied by a separate argument that the proposed ascertainment procedure invariably terminates with the correct verdict.

We construct an example of a group G=Z2×G0 for a finite abelian group G0, a subset E of G0, and two finite subsets F1,F2 of G, such that it is undecidable in ZFC whether Z2×E can be tiled by translations of F1,F2. In particular, this implies that this tiling problem is aperiodic, in the sense that (in the standard universe of ZFC) there exist translational tilings of E by the tiles F1,F2, but no periodic tilings. Previously, such aperiodic or undecidable translational tilings were only constructed for sets of eleven or more tiles (mostly in Z2). A similar construction also applies for G=Zd for sufficiently large d. If one allows the group G0 to be non-abelian, a variant of the construction produces an undecidable translational tiling with only one tile F. The argument proceeds by first observing that a single tiling equation is able to encode an arbitrary system of tiling equations, which in turn can encode an arbitrary system of certain functional equations once one has two or more tiles. In particular, one can use two tiles to encode tiling problems for an arbitrary number of tiles.

The “somewhat vague, intuitive” notion from computability theory of an effective procedure (method) or algorithm can be fairly precisely defined, even if it does not have a purely mathematical definition—and even if (as many have asserted) for that reason, the Church–Turing thesis (that the effectively calculable functions on natural numbers are exactly the general recursive functions), cannot be proved. However, it is logically provable from the notion of an effective procedure, without reliance on any (partially) mathematical thesis or conjecture concerning effective procedures, such as the Church–Turing thesis, that the class of effective procedures is undecidable, i.e., that there is no effective procedure for ascertaining whether a given procedure is effective. The proof does not even appeal to a precise definition of ‘effective procedure’. Instead, it relies solely and entirely on a basic grasp of the intuitive notion of such a procedure. Though the result itself is not surprising, it is also not without significance. It has the consequence, for example, that the solution to a decision problem, if it is to be complete, must be accompanied by a separate argument that the proposed ascertainment procedure is, in fact, a decision procedure, i.e., effective—for example, that it invariably terminates with the correct verdict.

We show that every distributive lattice-ordered pregroup can be embedded into a functional algebra over an integral chain, thus improving the existing Cayley/Holland-style embedding theorem. We use this result to show that the variety of all distributive lattice-ordered pregroups is generated by the functional algebra on the integers. Finally, we show that the equational theory of the variety is decidable. [ABSTRACT FROM AUTHOR]

Decidability of monadic first-order classical logic was established by L¨owenheim in 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3- style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T. [ABSTRACT FROM AUTHOR]

We introduce the infix inclusion problem of two languages S and T that decides whether or not S is a subset of the set of all infixes of T. This problem is motivated by the need for identifying malicious computation patterns according to their semantics, which are often disguised with additional sub-patterns surrounding information. In other words, malicious patterns are embedded as an infix of the whole pattern. We examine the infix inclusion problem for the case where a source S and a target T are finite, regular or context-free languages. We prove that the problem is 1) co-NP-complete when one of the languages is finite, 2) PSPACE-complete when both S and T are regular, 3) EXPTIME-complete when S is context-free and T is regular, 4) undecidable when S is either regular or context-free and T is context-free and 5) undecidable when one of S and T is in a language class where the emptiness of its languages is undecidable, even if the other is finite. We, furthermore, explore the infix inclusion problem for visibly pushdown languages, a subclass of context-free languages. [ABSTRACT FROM AUTHOR]

Fitch's knowability paradox shows that for each unknown truth there is also an unknowable truth, a result which has been thought both odd in itself and at odds with views which impose epistemic constraints on truth and/or meaningfulness. Here a solution is considered which has received little attention in the debate but which carries prima facie plausibility. The decidability solution is to accept that Fitch sentences are unknowably true but deny the significance of this on the grounds that Fitch sentences are nevertheless decidable. The decidability solution is particularly attractive for those whose primary concern is an epistemic constraint on meaningfulness ('verificationists'). For those whose main concern is truth ('anti‐realists'), the situation is more complex: Melia takes the solution to exonerate anti‐realism completely; Williamson sees it as completely irrelevant. The truth lies between these two extremes: there is one broad anti‐realist commitment to which the solution does not apply, but there is also one, the "fundamental tenet" of anti‐realism according to Dummett, to which it does. [ABSTRACT FROM AUTHOR]

Propositional modal logic over relational frames is naturally extended with propositional quantifiers by letting them range over arbitrary sets of worlds of the relevant frame. This is also known as second-order propositional modal logic. The propositionally quantified modal logic of a class of relational frames is often not axiomatizable, although there are known exceptions, most notably the case of frames validating the strong modal logic $\mathrm {S5}$. Here, we develop new general methods with which many of the open questions in this area can be answered. We illustrate the usefulness of these methods by applying them to a range of examples, which provide a detailed picture of which normal modal logics define classes of relational frames whose propositionally quantified modal logic is axiomatizable. We also apply these methods to establish new results in the multimodal case. [ABSTRACT FROM AUTHOR]

We provide an alternative proof of the decidability of the equational theory of lattices. The proof presented here is quite short and elementary. [ABSTRACT FROM AUTHOR]

A sequent calculus $ \mathfrak {S} $ S for the variety $ \mathsf {tqBa} $ tqBa of all topological quasi-Boolean algebras is established. Using a construction of syntactic finite algebraic model, the finite model property of $ \mathfrak {S} $ S is shown, and thus the decidability of $ \mathfrak {S} $ S is obtained. We also introduce two non-distributive variants of topological quasi-Boolean algebras. For the variety $ \mathsf {TDM5} $ TDM 5 of all topological De Morgan lattices with the axiom 5, we establish a sequent calculus $ \mathfrak {S}_5 $ S 5 and prove that the cut elimination holds for it. Consequently the decidability of $ \mathfrak {S}_5 $ S 5 is established. Furthermore, this proof-theoretic method is applied to some subvarieties of $ \mathsf {TDM5} $ TDM 5 . [ABSTRACT FROM AUTHOR]

This paper is dedicated to studying the algorithmic properties of unars with an injective function. We prove that the theory of every such unar admits quantifier elimination if the language is extended by a countable set of predicate symbols. Necessary and sufficient conditions are established for the quantifier elimination to be effective, and a criterion for decidability of theories of such unars is formulated. Using this criterion, we build a unar such that its theory is decidable, but the theory of the unar of its subsets is undecidable. [ABSTRACT FROM AUTHOR]

We propose a relaxation to the definition of well-structured transition systems (WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from another. Furthermore, the monotony condition is relaxed in the same way. While this retains the decidability of non-termination and boundedness, it appears that the coverability problem is undecidable. To this end, we define a new notion of monotony, called cover-monotony, which is strictly more general than the usual monotony and still allows us to decide a restricted form of the coverability problem. [ABSTRACT FROM AUTHOR]

We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the ‘precision’ embedding Z ∋ p 7→ 2p ∈ R, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic. [ABSTRACT FROM AUTHOR]

This paper studies proof systems for the logics of super-strict implication ST 2 – ST 5 , which correspond to C.I. Lewis' systems S 2 – S 5 freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating STn in Sn and backsimulating Sn in STn , respectively (for n = 2 , ... , 5 ). Next, G 3 -style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive of G 3 -style calculi, that they are sound and complete, and it is shown that the proof search for G 3. ST 2 is terminating and therefore the logic is decidable. [ABSTRACT FROM AUTHOR]

Decidability of monadic first-order classical logic was established by Löwenheim in 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T.

Morteza Hajhosseini introduced two truth-functional and non-truth-functional systems in the second edition of his book Two Non-Classical Logic Systems, A New Outlook on Elements of Logic. In other articles, I have reviewed the natural deduction and the semantics of the truth-functional system. In this paper, I will address the semantics of the non-truth-functional system and the meta-theorems of soundness and completeness that he claimed to have proven. I demonstrate that: 1. This semantics is based on a new set theory that has not yet been formulated. 2. The definition of ‘model’ in this book defines ‘complete models,’ while all introduced models are ‘incomplete models’. 3. The truth conditions of non-truth-functional formulas are reminiscent of the truth conditions of similar formulas in C.I. Lewis’ logic of strict implication, but in the Leibnizian modal semantics. 4. This semantics is not consistent with the proof theory of the book. 5. Therefore, the soundness and the completeness metatheorems are actually incorrect and have counterexamples. 6. Negation operators in this non-truth-functional system have been considered truthfunctional, while they should be non-truth-functional. 7. A finite number of relationships (exactly five) have been introduced in this semantics, while this number is infinite. 8. Therefore, non-truth-functional logic must be undecidable, while the non-truth-functional system has been declared decidable. [ABSTRACT FROM AUTHOR]

String assembling systems are biologically inspired mechanisms that generate strings from copies out of finite sets of assembly units. The underlying mechanism is based on piecewise assembly of a double-stranded sequence of symbols, where the upper and lower strand have to match. The generation is additionally controlled by the requirement that the first symbol of a unit has to be the same as the last symbol of the strand generated so far, as well as by the distinction of assembly units that may appear at the beginning, during, or at the end of the assembling process and by a length restriction on the units. We investigate the power of these model-inherent control mechanisms by considering variants where one or more of these mechanisms are relaxed. The generative capacities and the relative power of the variants are our main interest. In particular, we prove that the power gained in the different control mechanisms may yield strictly more powerful systems and incomparable capacities. Additionally, we generalize these systems to multi-stranded systems. We obtain a strong connection to one-way multi-head finite automata and show an infinite, dense, and strict strand hierarchy. Finally, we examine the closure properties of the different variants of string assembling systems. [ABSTRACT FROM AUTHOR]

We show that the equivalence, unambiguity, and sequentiality problems are decidable for finitely ambiguous max-plus tree automata. A max-plus tree automaton is a weighted tree automaton over the max-plus semiring. A max-plus tree automaton is called finitely ambiguous if the number of accepting runs on every tree is bounded by a global constant and it is called unambiguous if there exists at most one accepting run on every tree. For the equivalence problem, we show that for two finitely ambiguous max-plus tree automata, it is decidable whether both assign the same weight to every tree. For the unambiguity and sequentiality problems, we show that for every finitely ambiguous max-plus tree automaton, both the existence of an equivalent unambiguous automaton and the existence of an equivalent deterministic automaton are decidable. [ABSTRACT FROM AUTHOR]

Many decision problems concerning cellular automata are known to be decidable in the case of algebraic cellular automata, that is, when the state set has an algebraic structure and the automaton acts as a morphism. The most studied cases include finite fields, finite commutative rings and finite commutative groups. In this paper, we provide methods to generalize these results to the broader case of group cellular automata, that is, the case where the state set is a finite (possibly non-commutative) finite group. The configuration space is not even necessarily the full shift but a subshift — called a group shift — that is a subgroup of the full shift on ℤ d , for any number d of dimensions. We show, in particular, that injectivity, surjectivity, equicontinuity, sensitivity and nilpotency are decidable for group cellular automata, and non-transitivity is semi-decidable. Injectivity always implies surjectivity, and jointly periodic points are dense in the limit set. The Moore direction of the Garden-of-Eden theorem holds for all group cellular automata, while the Myhill direction fails in some cases. The proofs are based on effective projection operations on group shifts that are, in particular, applied on the set of valid space-time diagrams of group cellular automata. This allows one to effectively construct the traces and the limit sets of group cellular automata. A preliminary version of this work was presented at the conference Mathematical Foundations of Computer Science 2020. [ABSTRACT FROM AUTHOR]

This work investigates the decidability and complexity of database query answering under guarded existential rules with nonmonotonic negation according to the classical stable model semantics. In this setting, existential quantification is interpreted via Skolem functions, and the unique name assumption is adopted. As a first result, we show the decidability of answering first-order queries based on such rules by a translation into the satisfiability problem for guarded second-order formulas having the tree-model property. To obtain precise complexity results for unions of conjunctive queries, we transform the original problem in polynomial time into an intermediate problem that is easier to analyze: query answering for guarded disjunctive existential rules with stratified negation.We obtain precise bounds for the general setting and for various restricted settings. We also consider extensions of the original formalism with negative constraints, keys, and the possibility of negated atoms in queries. Finally, we show how the above results can be used to provide decidability and complexity results for a natural adaptation of the stable model semantics to description logics such as ELHI and the DL-Lite family. [ABSTRACT FROM AUTHOR]

The present paper studies formal properties of so-called modal information logics (MILs)—modal logics first proposed in (van Benthem 1996) as a way of using possible-worlds semantics to model a theory of information. They do so by extending the language of propositional logic with a binary modality defined in terms of being the supremum of two states. First proposed in 1996, MILs have been around for some time, yet not much is known: (van Benthem 2017, 2019) pose two central open problems, namely (1) axiomatizing the two basic MILs of suprema on preorders and posets, respectively, and (2) proving (un)decidability. The main results of the first part of this paper are solving these two problems: (1) by providing an axiomatization [with a completeness proof entailing the two logics to be the same], and (2) by proving decidability. In the proof of the latter, an emphasis is put on the method applied as a heuristic for proving decidability 'via completeness' for semantically introduced logics; the logics lack the FMP w.r.t. their classes of definition, but not w.r.t. a generalized class. These results are build upon to axiomatize and prove decidable the MILs attained by endowing the language with an 'informational implication'—in doing so a link is also made to the work of (Buszkowski 2021) on the Lambek Calculus. [ABSTRACT FROM AUTHOR]