This paper presents a simple decidable logic of functional dependence LFD, based on an extension of classical propositional logic with dependence atoms plus dependence quantifiers treated as modalities, within the setting of generalized assignment semantics for first order logic. The expressive strength, complete proof calculus and meta-properties of LFD are explored. Various language extensions are presented as well, up to undecidable modal-style logics for independence and dynamic logics of changing dependence models. Finally, more concrete settings for dependence are discussed: continuous dependence in topological models, linear dependence in vector spaces, and temporal dependence in dynamical systems and games.
In this paper, we study logics of dependence on the propositional level. We prove that several interesting propositional logics of dependence, including propositional dependence logic, propositional intuitionistic dependence logic as well as propositional inquisitive logic, are expressively complete and have disjunctive or conjunctive normal forms. We provide deduction systems and prove the completeness theorems for these logics.
We study hidden-variable models from quantum mechanics, and their abstractions in purely probabilistic and relational frameworks, by means of logics of dependence and independence, based on team semantics. We show that common desirable properties of hidden-variable models can be defined in an elegant and concise way in dependence and independence logic. The relationship between different properties, and their simultaneous realisability can thus been formulated and a proved on a purely logical level, as problems of entailment and satisfiability of logical formulae. Connections between probabili…
Modern logics of dependence and independence are based on team semantics, which means that formulae are evaluated not on a single assignment of values to variables, but on a set of such assignments, called a team. This leads to high expressive power, on the level of existential second-order logic. As an alternative, Baltag and van Benthem have proposed a local variant of dependence logic, called logic of functional dependence (LFD). While its semantics is also based on a team, the formulae are evaluated locally on just one of its assignments, and the team just serves as the supply of the possi…
In recent years, the logic of questions and dependencies has been investigated in the closely related frameworks of inquisitive logic and dependence logic. These investigations have assumed classical logic as the background logic of statements, and added formulas expressing questions and dependencies to this classical core. In this paper, we broaden the scope of these investigations by studying questions and dependency in the context of intuitionistic logic. We propose an intuitionistic team semantics, where teams are embedded within intuitionistic Kripke models. The associated logic is a cons…
We study LFD, a base logic of functional dependence introduced by Baltag and van Benthem (2021) and its connections with the guarded fragment GF of first-order logic. Like other logics of dependence, the semantics of LFD uses teams: sets of permissible variable assignments. What sets LFD apart is its ability to express local dependence between variables and local dependence of statements on variables. Known features of LFD include decidability, explicit axiomatization, finite model property, and a bisimulation characterization. Others, including the complexity of satisfiability, remained open …
Recently, Baltag and van Benthem arXiv:2103.14946 [cs.LO] introduced a new decidable logic of functional dependence (LFD) with local dependence formulas and dependence quantifiers. The language is interpreted over dependence models, which are pairs of first-order structures with a set of available variable assignments, also called a team. The team associated with a dependence model can be seen as a labelled transition system over which LFD becomes a modal logic, where the dependence quantifiers become modalities and local dependence formulas are treated as special atoms. In this paper, we intr…
The Workshops on (Constraint) Logic Programming (WLP) are the annual meeting of the German Society of Logic Programming (Gesellschaft für Logische Programmierung e.V., GLP) and bring together researchers interested in logic programming, constraint programming, answer set programming, and related areas like databases and artificial intelligence (not only from Germany). The International Workshops on Functional and (Constraint) Logic Programming (WFLP) aim at bringing together researchers, students, and practitioners interested in functional programming, logic programming, and their integration.…
We study the enumeration of answers to ontology-mediated queries when the ontology is formulated in a description logic that supports functional roles and the query is a CQ. In particular, we show that enumeration is possible with linear preprocessing and constant delay when a certain extension of the CQ (pertaining to functional roles) is acyclic and free-connex acyclic. This holds both for complete answers and for partial answers. We provide matching lower bounds for the case where the query is self-join free.
Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of $λ$-calculus with parallelism and communication primitives, called $λ_{\unicode{8523}}$. We shall prove that $λ_{\unicode{8523}}$ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.
Representation Theorems for Cumulative Propositional Dependence Logics
Department of Mathematics and Statistics, University of Helsinki（赫尔辛基大学数学与统计学系）；Theoretical Computer Science, Leibniz University Hannover（汉诺威莱比锡大学理论计算机科学系）；Faculty of Mathematics and Computer Science, FernUniversität in Hagen（哈根应用科学大学数学与计算机科学学院）
In this paper, we investigate the parameterized complexity of model checking for Dependence Logic which is a well studied logic in the area of Team Semantics. We start with a list of nine immediate parameterizations for this problem, namely: the number of disjunctions (i.e., splits)/(free) variables/universal quantifiers, formula-size, the tree-width of the Gaifman graph of the input structure, the size of the universe/team, and the arity of dependence atoms. We present a comprehensive picture of the parameterized complexity of model checking and obtain a division of the problem into tractable…
本文主要研究模态依赖逻辑.它是由Jouko Vääanänen在2007年引入的，作为一阶的扩展（分别为。模态）逻辑的依赖运算符=（）。一阶（resp.）命题）变量x_1，...，x_n，=（x_1，...，x_n）直观地说明x_n的值由x_1，.，x_n-1。我们认为片段的模态依赖逻辑通过限制允许模态和命题连接词的集合。我们对这些片段的可满足性和模型检查问题的复杂性进行了分类。对于可满足性，我们获得了从P over NP，Sigma_P^2和PSPACE到NEXP的复杂度，而对于模型检查，我们只根据它们的易处理性对片段进行分类，即我们在P中显示NP-完全性或包含性。对于这个扩展，我们再次分类的复杂性模型检查问题的片段。在这里，我们获得了从P over NP和coNP到PSPACE的复杂度。最后，我们分析了一阶依赖逻辑、独立友好逻辑及其二元片段。我们证明了两个变量的依赖逻辑的可满足性是NEXP-完全的，而两个变量的独立友好的逻辑，它是不可判定的，并使用这一点来证明，后者也比前者更有表现力。
模态依赖逻辑最近由Väänänen引入。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n，=（p_1，...，p_（n-1）;p_n）直观地说明p_n的值由p_1，.，p_（n-1）。Sevenster（J. Logic and Computation，2009）表明，对于非确定性指数时间，模态依赖逻辑的可满足性是完全的。在本文中，我们考虑片段的模态依赖逻辑得到的限制允许命题连接词的集合。我们证明了穷人依赖逻辑的可满足性，这种语言由使用合取、必要性和可能性（即，不允许分离），保持NEXPTIME-完全。如果我们只允许单调公式（没有否定，但有析取），复杂性下降到PSPACE完全性。我们还扩展了Väänänen的语言，允许经典的析取除了依赖析取，并表明可满足性问题仍然是NEXPTIME完全的。如果我们不允许否定和依赖析取，那么对于多项式层次的第二层来说，可满足性是完全的。通过这种方式，我们对Väänänen和Sevenster考虑的命题和依赖运算符的所有限制的可满足性问题的计算复杂性进行了完全分类。
This volume constitutes the pre-proceedings of the 26th International Workshop on Functional and Logic Programming (WFLP 2018). It is formed of those papers selected by the program committee for presentation at the workshop. After discussion at the workshop, the program committee will select a number of papers to be invited for the second round of refereeing and selection for the formal proceedings.
Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed-point logic. Inclusion logic is not axiomatizable in full, but its first-order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first-order consequences in inclusion logic.
Dependence logics are a modern family of logics of independence and dependence which mimic notions of database theory. In this paper, we aim to initiate the study of enumeration complexity in the field of dependence logics and thereby get a new point of view on enumerating answers of database queries. Consequently, as a first step, we investigate the problem of enumerating all satisfying teams of formulas from a given fragment of propositional dependence logic. We distinguish between restricting the team size by arbitrary functions and the parametrised version where the parameter is the team s…
On the Complexity and Properties of Preferential Propositional Dependence Logic
Artificial Intelligence Group, University of Hagen（汉内斯大学人工智能小组）；Theoretical Computer Science, Leibniz University Hannover（汉诺威莱比锡大学理论计算机科学）；Department of Mathematics and Statistics, University of Helsinki（赫尔辛基大学数学与统计学系）
本文研究命题依赖逻辑中的 KLM 风格偏好推理，刻画其满足 System P 的条件，分析与团队命题逻辑的差异，并给出模型表示及两种表示下的复杂性结果。
We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schönfinkel-Ramsey prefix classes of dependence logic.
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof assistant Isabelle/HOL. This allows us to make notions which are often unclear in textbooks precise, to experiment with definitions by executing them, and to prove metatheoretical theorems in full detail. We have surveyed student perceptions of our teaching approach to determine its usefulness and found that students felt that our formalizations helped them underst…
Strategy Logic (SL) is a very expressive logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in th…
Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence, a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification m…
