Browsing by Subject "math.LO"

Sort by: Order: Results:

Now showing items 1-6 of 6
  • Hannula, Miika; Kontinen, Juha (Springer Science+Business Media, 2014)
    Lecture Notes in Computer Science
    We present a complete finite axiomatization of the unrestricted implication problem for inclusion and conditional independence atoms in the context of dependence logic. For databases, our result implies a finite axiomatization of the unrestricted implication problem for inclusion, functional, and embedded multivalued dependencies in the unirelational case.
  • Hannula, Miika; Kontinen, Juha; Virtema, Jonni; Vollmer, Heribert (2018)
    We classify the computational complexity of the satisfiability, validity, and model-checking problems for propositional independence, inclusion, and team logic. Our main result shows that the satisfiability and validity problems for propositional team logic are complete for alternating exponential-time with polynomially many alternations.
  • Hannula, Miika; Kontinen, Juha; Bussche, Jan Van den; Virtema, Jonni (IEEE Computer Society, 2020)
    We introduce a novel variant of BSS machines called Separate Branching BSS machines (S-BSS in short) and develop a Fagin-type logical characterisation for languages decidable in non-deterministic polynomial time by S-BSS machines. We show that NP on S-BSS machines is strictly included in NP on BSS machines and that every NP language on S-BSS machines is a countable union of closed sets in the usual topology of R^n. Moreover, we establish that on Boolean inputs NP on S-BSS machines without real constants characterises a natural fragment of the complexity class existsR (a class of problems polynomial time reducible to the true existential theory of the reals) and hence lies between NP and PSPACE. Finally we apply our results to determine the data complexity of probabilistic independence logic.
  • Kontinen, Juha; Yang, Fan (Springer-Verlag, 2019)
    Lecture Notes in Computer Science
    In this paper, we introduce a logic based on team semantics, called FOT, whose expressive power coincides with first-order logic both on the level of sentences and (open) formulas, and we also show that a sublogic of FOT, called FOT${}^\downarrow$, captures exactly downward closed first-order team properties. We axiomatize completely the logic FOT, and also extend the known partial axiomatization of dependence logic to dependence logic enriched with the logical constants in FOT${}^\downarrow$.
  • Ilin, Julia; Jongh, Dick de; Yang, Fan (2021)
    NNIL-formulas, introduced by Visser in 1983-1984 in a study of Sigma(1)-subsitutions in Heyting arithmetic, are intuitionistic propositional formulas that do not allow nesting of implication to the left. The first results about these formulas were obtained in a paper of 1995 by Visser et al. In particular, it was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. Recently, Bezhanishvili and de Jongh observed that NNIL-formulas are also reflected by the colour-preserving monotonic maps of Kripke models. In the present paper, we first show how this observation leads to the conclusion that NNIL-formulas are preserved by arbitrary substructures not necessarily satisfying the topo-subframe condition. Then, we apply it to construct universal models for NNIL. It follows from the properties of these universal models that NNIL-formulas are also exactly the formulas that are reflected by colour-preserving monotonic maps. By using the method developed in constructing the universal models, we give a new direct proof that the logics axiomatized by NNIL-axioms have the finite model property.
  • Hella, Lauri; Väänänen, Jouko (de Gruyter, 2015)
    Ontos Mathematical Logic
    We introduce a refinement of the usual Ehrenfeucht-Fra\"{\i}ss\'e game. The new game will help us make finer distinctions than the traditional one. In particular, it can be used to measure the size formulas needed for expressing a given property. We will give two versions of the game: the first version characterizes the size of formulas in propositional logic, and the second version works for first-order predicate logic.