Miika Hannula
Abstract
We study the expressive power of fragments of inclusion logic under the so-called lax team semantics. The fragments are defined either by restricting the number of universal quantifiers, the number of inclusion atoms, or the arity of inclusion atoms. We show that the whole expressive power of inclusion logic can be captured using only five inclusion atoms in finite ordered models or, alternatively, only one universal quantifier in general. The arity hierarchy is shown to be strict by relating the question to the study of arity hierarchies in fixed point logics.
- Samson Abramsky and Jouko Väänänen. 2009. From IF to BI. Synthese 167, 2, 207--230.Google Scholar
Cross Ref
- Miklos Ajtai. 1983. Σ<sup>1</sup><sub>1</sub>-Formulae on finite structures. Annals of Pure and Applied Logic 4, 1, 1--48.Google ScholarCross Ref
- William W. Armstrong. 1974. Dependency structures of data base relationships. In Proceedings of the IFIP World Computer Congress. 580--583.Google Scholar
- Marco A. Casanova, Ronald Fagin, and Christos H. Papadimitriou. 1984. Inclusion dependencies and their interaction with functional dependencies. Journal of Computer Systems and Sciences 28, 1, 29--59.Google ScholarCross Ref
- Arnaud Durand and Juha Kontinen. 2012. Hierarchies in dependence logic. ACM Transactions on Computational Logic 13, 4, 31. Google ScholarDigital Library
- Pietro Galliani. 2012. Inclusion and exclusion dependencies in team semantics: On some logics of imperfect information. Annals of Pure and Applied Logic 163, 1 (2012), 68--84.Google ScholarCross Ref
- Pietro Galliani, Miika Hannula, and Juha Kontinen. 2013. Hierarchies in independence logic. In Computer Science Logic 2013 (CSL’13), Leibniz International Proceedings in Informatics (LIPIcs), Simona Ronchi Della Rocca (Ed.), Vol. 23. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 263--280.Google Scholar
- Pietro Galliani and Lauri Hella. 2013. Inclusion logic and fixed point logic. In Computer Science Logic 2013 (CSL’13), Leibniz International Proceedings in Informatics (LIPIcs), Simona Ronchi Della Rocca (Ed.), Vol. 23. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 281--295.Google Scholar
- Pietro Galliani and Jouko A. Väänänen. 2014. On dependence logic. In Johan van Benthem on Logical and Informational Dynamics, A. Baltag and S. Smets (Eds.). Springer, 101--119.Google Scholar
- Dan Geiger, Azaria Paz, and Judea Pearl. 1991. Axioms and algorithms for inferences involving probabilistic independence. Information and Computation 91, 1, 128--141. Google ScholarDigital Library
- Erich Grädel. 2013. Model-checking games for logics of imperfect information. Theoretical Computer Science 493, 2--14. Google ScholarDigital Library
- Erich Grädel and Jouko Väänänen. 2013. Dependence and independence. Studia Logica 101, 2, 399--410. Google ScholarDigital Library
- Etienne Grandjean and Frédéric Olive. 2004. Graph properties checkable in linear time in the number of vertices. J.ournal of Computer Systems and Sciences 68, 3, 546--597. Google ScholarDigital Library
- Martin Grohe. 1996. Arity hierarchies. Annals of Pure and Applied Logic 82, 2, 103--163.Google ScholarCross Ref
- Miika Hannula and Juha Kontinen. 2015. Hierarchies in independence and inclusion logic with strict semantics. Journal of Logic and Computation 25, 3, 879--897.Google ScholarCross Ref
- Wilfrid Hodges. 1997. Compositional semantics for a language of imperfect information. Journal of the Interest Group in Pure and Applied Logics 5, 4, 539--563.Google Scholar
- Ehud Hrushovski. 1992. Extending partial isomorphisms of graphs.Combinatorica 12, 4, 411--416. http://dblp.uni-trier.de/db/journals/combinatorica/combinatorica12.html#Hrushovski92.Google Scholar
- Henrik Imhof. 1996. Computational aspects of arity hierarchies. In CSL’09, Lecture Notes in Computer Science, Dirk van Dalen and Marc Bezem (Eds.), Vol. 1258. Springer, Berlin, 211--225. http://dblp.uni-trier.de/db/conf/csl/csl96.html#Imhof96. Google ScholarDigital Library
- Neil Immerman. 1986. Relational queries computable in polynomial time. Information and Control 68, 1-3, 86--104. Google ScholarDigital Library
- Neil Immerman. 1987. Languages that capture complexity classes. SIAM Journal on Computing 16, 4, 760--778. Google ScholarDigital Library
- Neil Immerman. 1999. Descriptive Complexity. Springer.Google Scholar
- Jarmo Kontinen. 2010. Coherence and computational complexity of quantifier-free dependence logic formulas. In Proceedings of Dependence and Independence in Logic, Juha Kontinen and Jouko Väänänen (Eds.). ESSLLI’10, 58--77.Google Scholar
- Juha Kontinen, Sebastian Link, and Jouko A. Väänänen. 2013. Independence in database relations. In Proceedings of Logic, Language, Information, and Computation — 20th International Workshop (WoLLIC’13), Darmstadt, Germany, August 20-23, 2013.179--193. Google ScholarDigital Library
- Leonid Libkin. 2004. Elements of Finite Model Theory. Springer. Google ScholarDigital Library
- Yiannis N. Moschovakis. 1974. Elementary Induction on Abstract Structures (Studies in Logic and the Foundations of Mathematics). Elsevier. Google ScholarDigital Library
- Jouko Väänänen. 2007. Dependence Logic. Cambridge University Press, Cambridge, UK.Google Scholar
- Moshe Y Vardi. 1982. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing. ACM, 137--146. Google ScholarDigital Library
- Fan Yang. 2013. Expressing second-order sentences in intuitionistic dependence logic. Studia Logica 101, 2, 323--342. STLOEQ Google ScholarDigital Library
Index Terms
- Hierarchies in Inclusion Logic with Lax Semantics
Recommendations
Tractability Frontier of Data Complexity in Team Semantics
We study the data complexity of model checking for logics with team semantics. We focus on dependence, inclusion, and independence logic formulas under both strict and lax team semantics. Our results delineate a clear tractability/intractability frontiers ...
Undefinability in Inquisitive Logic with Tensor
Logic, Rationality, and InteractionAbstractLogics based on team semantics, such as inquisitive logic and dependence logic, are not closed under uniform substitution. This leads to an interesting separation between expressive power and definability: it may be that an operator O can be added ...
Dependence Logic with a Majority Quantifier
We study the extension of dependence logic $$\mathcal {D}$$D by a majority quantifier $$\mathsf{M}$$M over finite structures. We show that the resulting logic is equi-expressive with the extension of second-order logic by second-order majority ...
Reviews
Wolfgang Schreiner
A natural interest of computational logic is to investigate decidable subsets of first-order logic. One such subset is the formalism of inclusion logic (FOI), introduced by Galliani as an evolution of dependence logic [1], which investigates functional dependencies that arise in database theory. FOI allows as an atomic predicate only tuple inclusion (a generalization of the subset predicate to multiple components); the semantics of FOI are defined not only over single assignments of variables to values, but also over sets of assignments called "teams." This paper investigates the properties of inclusion logic under lax team semantics, where a disjunction is also satisfied if overlapping subsets of teams satisfy each of its parts. In particular, it shows: (1) the full expressiveness of FOI is already achieved if formulas are restricted to a single universal quantifier; (2) already in finite models, a logic FOI k that restricts inclusion to tuples of length k is strictly less expressive than a logic FOI( k +1) (which gives rise to an infinite expressiveness hierarchy); and (3) in finite ordered models, the expressiveness of FOI is already achieved if formulas are restricted to five inclusion atoms. The proofs of these results, in particular for the main result (2), represent the core of the paper. This paper nicely complements and extends Galliani's results; for more background on FOI and its motivation, readers should study the corresponding references first. It also raises open questions for future research, such as generalizing property to ordered models or to unordered ones.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments