A First Peek into Preferential Logics with Team Semantics
                         Kai Sauerwald1 , Juha Kontinen2
                         1
                             FernUniversität in Hagen, Hagen, Germany
                         2
                             University of Helsinki, Helsinki, Finland


                                           Abstract
                                           This paper considers KLM-style preferential non-monotonic reasoning in the setting of propositional team semantics. We show that
                                           team-based propositional logics naturally give rise to cumulative non-monotonic entailment relations. Motivated by the non-classical
                                           interpretation of disjunction in team semantics, we give a precise characterization for preferential models for propositional dependence
                                           logic satisfying all of System P postulates. Furthermore, we show how classical entailment and dependence logic entailment can be
                                           expressed in terms of non-trivial preferential models.

                                           Keywords
                                           KLM, non-monotonic logic, System P, triangle-property, team logic, team semantics, preferential reasoning



                         1. Introduction                                                                                                  and an analogue non-monotonic entailment =(𝑏, 𝑓 ) |∼ ¬𝑝
                                                                                                                                          can be read as
                         We define non-monotonic versions of team-based logics and
                         study their axiomatics regarding System P. The logics are                                                        “when whether it is a bird (𝑏) determines whether it flies (𝑓 ),
                         defined with the aid of preferential models in the style of                                                               then it is usually not a penguin (¬𝑝)”.
                         Kraus, Lehmann and Magidor [1] (KLM).
                                                                                                                                          Alternatively to the interpretation above, one can under-
                            Team semantics is a logical framework for studying con-
                                                                                                                                          stand non-monotonic inferences from a team perspective.
                         cepts and phenomena that arise in the presence of plurality
                                                                                                                                          For example, =(𝑏, 𝑓 ) |∼ ¬𝑝 reads then as “a team that usu-
                         of data. Prime examples of such concepts are, e.g., functional
                                                                                                                                          ally satisfies =(𝑏, 𝑓 ) also satisfies ¬𝑝”. For the latter kind
                         dependence ubiquitous in database theory and conditional
                                                                                                                                          of expression, there is no obvious way to formulate it in ex-
                         independence of random variables in statistics. The begin-
                                                                                                                                          isting team-based logic, so injecting non-monotonicity is a
                         ning of the field of team semantics can be traced back to
                                                                                                                                          valuable extension of team logics. Note that “=(𝑏, 𝑓 ) |∼ ¬𝑝”
                         the introduction of (first-order) dependence logic in [2]. In
                                                                                                                                          does not imply that = (𝑏, 𝑓 ) ∧ 𝑝 is inconsistent. The seman-
                         dependence logic, formulas are interpreted by sets of as-
                                                                                                                                          tics of team logic is developed with emphasis on teams. De-
                         signments (teams). Syntactically, dependence logic extends
                                                                                                                                          pended on the application context, one reads =(𝑏, 𝑓 ) |∼ ¬𝑝,
                         first-order logic by dependence atoms =(⃗     𝑥, 𝑦) expressing
                                                                                                                                          e.g., as follows:
                         that the values of the variables ⃗𝑥 functionally determine the
                         value of the variable 𝑦. Inclusion logic [3] is another promi-                                                   Database Interpretation: “When the value of 𝑏 determines
                         nent logic in this context that extends first-order logic by                                                     the value of 𝑓 in a database, then usually the value of 𝑝 is 0.”
                         inclusion atoms ⃗ 𝑥⊆⃗   𝑦 , whose interpretation corresponds                                                     Possible World Interpretation. “When the agent is convinced
                         exactly to that of inclusion dependencies in database theory.                                                    that whether 𝑓 holds in a world always depends on 𝑏, then
                         During the past decade, the expressivity and complexity                                                          usually the agent believes that 𝑝 does not hold.”
                         aspects of logics in team semantics have been extensively                                                          There are several approaches to non-monotonic reason-
                         studied. Fascinating connections have been drawn to areas                                                        ing, e.g., circumscription, autoepistemic logic, Reiters de-
                         such as database theory [4, 5], verification [6], real-valued                                                    fault logic, see Gabbay (1993) for an overview. For a start,
                         computation [7], inquisitive logic [8], and epistemic logic                                                      one can rely on the basic systems of non-monotonic reason-
                         [9]. These works have focused on logics in the first-order,                                                      ing. The very most basic denominator of non-monotonic
                         propositional and modal team semantics, and more recently                                                        reasoning is often denoted cumulative reasoning, which is
                         also in the multiset [10], probabilistic [11] and semiring set-                                                  given axiomatically by System C [18]. In extension to cu-
                         tings [12]. As far as the authors know, a merger of logics in                                                    mulative reasoning, non-monotonic reasoning in the style
                         team semantics and non-monotonic reasoning has not been                                                          of KLM is considered as the “conservative core of non-
                         studied so far.                                                                                                  monotonic reasoning” [19, 18]. KLM-style non-monotonic
                            Non-monotonicity is one of the core phenomenons of                                                            reasoning has two prominent representations [1]:
                         reasoning that are deeply studied in knowledge represen-
                         tation and reasoning; see Gabbay et al. (1993) and Brewka                                                        (KLM.1) reasoning over preferential models; and
                         et al. (1997) for an overview, with, e.g., connections to
                                                                                                                                          (KLM.2) an axiomatic characterization, called System P,
                         belief change [15] and human-like reasoning [16]. Non-
                                                                                                                                                  which is an extension of System C.
                         monotonic inference 𝜙 |∼ 𝜓 is often understood as “when
                         𝜙 holds, then usually 𝜓 holds”, where usually can be un-                                                         Because of (KLM.1), KLM-style reasoning is also denoted
                         derstood in the sense of expected [17]. One can imagine                                                          preferential reasoning. Common for both representations
                         adapting this notion of non-monotonic inference to propo-                                                        of KLM-style reasoning is, that they are parametric in the
                         sitional team logics. For instance, in dependence logic, an                                                      sense that they make use of some underlying classical logic
                         entailment =(𝑏, 𝑓 ) |= ¬𝑝 states that                                                                            L , e.g., propositional logic or first-order logic.
                         “when whether it is a bird (𝑏) determines whether it flies (𝑓 ),                                                    In this paper, we define preferential team logics via pref-
                                         then it is not a penguin (¬𝑝)”                                                                   erential models (as in KLM.1). The rationale is that we think
                          22nd International Workshop on Nonmonotonic Reasoning, November 2-4,                                            that preferential models capture the original intention of
                          2024, Hanoi, Vietnam                                                                                            preferential logic best, and, as we demonstrate, it shows
                                       © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License
                                       Attribution 4.0 International (CC BY 4.0).                                                         standard non-monotonic behaviour. Furthermore, we study

CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
                                                                                                                                      1
Kai Sauerwald et al. CEUR Workshop Proceedings                                                                                                       1–7



the relationship of preferential teams logic to System P (as                            • 𝑋 |= 𝛼 ∧ 𝛽 iff 𝑋 |= 𝛼 and 𝑋 |= 𝛽;
in KLM.2). Our axiomatic studies show that for general                                  • 𝑋 |= 𝛼 ∨ 𝛽 iff there exist 𝑌, 𝑍 ⊆ 𝑋 such that
team-based logics, (KLM.1) and (KLM.2) do not induce the                                  𝑋 = 𝑌 ∪ 𝑍, 𝑌 |= 𝛼 and 𝑍 |= 𝛽.
same non-monotonic inference relations. This is of interest,
e.g., because it gives a negative answer to the question of                       The set of all teams 𝑋 with 𝑋 |= 𝛼 is written as J𝛼K. Logical
whether the relationship between (KLM.1) and (KLM.2) by                           entailment and equivalence are defined as usual. For any
KLM (1990) generalize beyond the assumptions by KLM1 .                            set ∆ ∪ 𝛼 of classical formulas, we write ∆ |= 𝛼 if for any
We give a condition for preferential models that is sufficient                    team 𝑋, 𝑋 |= 𝛿 for all 𝛿 ∈ ∆ implies 𝑋 |= 𝛼. We write
to reestablish satisfaction of System P in all preferential team                  simply 𝛼 |= 𝛽 for {𝛼} |= 𝛽. Write 𝛼 ≡ 𝛽 if both 𝛼 |= 𝛽
logics. Specifically for preferential dependence logic, we also                   and 𝛽 |= 𝛼.
show that this condition exactly characterizes those pref-
                                                                                  Proposition 4. Let 𝛼 be a PL-formula. Then the following
erential models such that System P is satisfied. Moreover,
                                                                                  properties hold:
when using specific (non-trivial) preferences, preferential
dependence logic becomes dependence logic, respectively,                          Flatness: 𝑋 |= 𝛼 ⇐⇒ for all 𝑣 ∈ 𝑋, {𝑣} |= 𝛼.
it is equivalent to classical propositional entailment.
                                                                                  Empty team property: ∅ |= 𝛼.

2. Background: Team-Based Logics                                                  Downwards closure: If 𝑋 |= 𝛼 and 𝑌 ⊆ 𝑋, then 𝑌 |= 𝛼.

In this section we present the background on propositional                        Union closure: If 𝑋 |= 𝛼 and 𝑌 |= 𝛼, then 𝑋 ∪ 𝑌 |= 𝛼.
logics with team semantics, propositional dependence logic                           For any PL-formula 𝛼, it further holds that
and propositional inclusion logic (see [20] for a survey on
team-based logics).                                                                                    {𝑣} |= 𝛼 ⇐⇒ 𝑣 |= 𝛼,

                                                                                  and hence for classical formulas, ∆ |=𝑐 𝛼 ⇐⇒ ∆ |= 𝛼.
2.1. Propositional Logic with Team
     Semantics
                                                                                  2.2. Propositional Dependence and
We denote by Prop = {𝑝𝑖 : 𝑖 ∈ N} the set of propositional                              Inclusion Logic
variables. We will use letters 𝑝, 𝑞, 𝑟, . . . (with or without
subscripts) to stand for elements of Prop. In this article, we                    A (propositional) dependence atom is a string =(𝑎1 . . . 𝑎𝑘 , 𝑏),
consider only formulas in negation normal form.                                   and a (propositional) inclusion atom is a string 𝑎1 . . . 𝑎𝑘 ⊆
                                                                                  𝑏1 . . . 𝑏𝑘 , in which 𝑎1 , . . . , 𝑎𝑘 , 𝑏, 𝑏1 , . . . , 𝑏𝑘 are proposi-
Definition 1 (Classical propositional logic (PL)). Well                           tional variables from Prop. The team semantics of these
formed PL-formulas 𝛼 are formed by the grammar:                                   two types of atoms is defined as follows, whereby ⃗𝑎 stands
                                                                                  for 𝑎1 , . . . , 𝑎𝑘 :
                𝛼 ::= 𝑝 | ¬𝑝 | ⊥ | ⊤ | 𝛼 ∧ 𝛼 | 𝛼 ∨ 𝛼
                                                                                        • 𝑋 |= =(⃗𝑎, 𝑏) iff for all 𝑣, 𝑣 ′ ∈ 𝑋, 𝑣(⃗𝑎) = 𝑣 ′ (⃗𝑎)
   In team semantics, one usually considers a non-empty fi-                               implies 𝑣(𝑏) = 𝑣 ′ (𝑏).
nite subset 𝑁 ⊆ Prop of propositional variables and defined
                                                                                        • 𝑋 |= ⃗𝑎 ⊆ ⃗𝑏 iff for all 𝑣 ∈ 𝑋, there exists 𝑣 ′ ∈ 𝑋
for valuations 𝑣 : 𝑁 → {0, 1} over 𝑁 and PL-formulas 𝛼:
                                                                                          such that 𝑣(⃗𝑎) = 𝑣 ′ (⃗𝑏).
                J𝛼K𝑐 := {𝑣 : 𝑁 → {0, 1} | 𝑣 |= 𝛼}.
                                                                                    We define propositional dependence logic (denoted as
We write 𝑣 |= 𝑝 in case 𝑣(𝑝) = 1, and 𝑣 ̸|= 𝑝 otherwise. The                      PL(=(,))) as the extension of PL-formulas with dependence
valuation function 𝑣 is extended to the set of all PL-formulas                    atoms. Similarly, propositional inclusion logic (denoted as
in the usual way.                                                                 PL(⊆)) is the extension of PL by inclusion atoms. In this
                                                                                  paper, we use propositional team logic to refer to any of the
Definition 2. For any set ∆ ∪ {𝛼} of PL-formulas, we                              logics PL, PL(=(,)) and PL(⊆).
write ∆ |=𝑐 𝛼 if for any valuation 𝑣, 𝑣 |= 𝛿 for all 𝛿 ∈ ∆                          It is straightforward to check that dependence atoms do
implies 𝑣 |= 𝛼. We write simply 𝛼 |=𝑐 𝛽 for {𝛼} |=𝑐 𝛽 and                         not have the union closure property and inclusion atoms
𝛼 ≡𝑐 𝛽 if both 𝛼 |=𝑐 𝛽 and 𝛽 |=𝑐 𝛼.                                               the downwards closure property. However, the following
                                                                                  holds.
  Next we define team semantics for PL-formulas (cf. [21,
22]). A team 𝑋 is a set of valuations for some finite set                         Proposition 5. Formulas of PL(=(,)) and PL(⊆) have the
𝑁 ⊆ Prop. We write dom(𝑋) for the domain 𝑁 of 𝑋.                                  empty team property. Moreover, PL(=(,))-formulas have the
                                                                                  downwards closure property, while PL(⊆)-formulas have the
Definition 3 (Team semantics of PL). Let 𝑋 be a team. For                         union closure property.
any PL-formula 𝛼 with dom(𝑋) ⊇ Prop(𝛼), the satisfac-
tion relation 𝑋 |= 𝛼 is defined inductively as:                                      A dependence atom with the empty sequence in the first
                                                                                  component will be abbreviated as =(𝑝) and called constancy
         • 𝑋 |= 𝑝 iff for all 𝑣 ∈ 𝑋, 𝑣 |= 𝑝;                                      atoms. The team semantics of constancy atoms is reduced
         • 𝑋 |= ¬𝑝 iff for all 𝑣 ∈ 𝑋, 𝑣 ̸|= 𝑝;                                    to
         • 𝑋 |= ⊥ iff 𝑋 = ∅;
         • 𝑋 |= ⊤ is always the case;                                                   • 𝑋 |= =(𝑝) iff for all 𝑣, 𝑣 ′ ∈ 𝑋, 𝑣(𝑝) = 𝑣 ′ (𝑝).

1
    KLM assume a compact Tarskian logic with Boolean connectives. In              Example 6. Consider the team 𝑋 over {𝑝, 𝑞, 𝑟} defined
    team logics (by default), there is no negation, and disjunction is non-       by:
    classical, i.e., it does not behave like Boolean disjunction.




                                                                              2
Kai Sauerwald et al. CEUR Workshop Proceedings                                                                                      1–7


                             𝑝    𝑞    𝑟                               3.2. Axiomatic Characterization by System P
                       𝑣1    1    0    0
                       𝑣2    0    1    0                               We make use of the following rules for non-monotonic en-
                       𝑣3    0    1    0                               tailment |∼ :

We have 𝑋 |= =(𝑝, 𝑞) and 𝑋 |= =(𝑟). Moreover, 𝑋 |=
=(𝑝) ∨ =(𝑝) but 𝑋 ̸|= =(𝑝). It is worth noting that PL(⊆)-                                                  𝛼 |= 𝛽     𝛾 |∼ 𝛼
                                                                                                    (Ref)                     (RW)
formulas 𝜑 satisfy                                                                        𝛼 |∼ 𝛼                 𝛾 |∼ 𝛽
                       𝜑≡𝜑∨𝜑                                                   𝛼≡𝛽    𝛼 |∼ 𝛾                𝛼 |∼ 𝛽    𝛼 |∼ 𝛾
                                                                                             (LLE)                               (CM)
because of the union closure property.                                           𝛽 |∼ 𝛾                        𝛼 ∧ 𝛽 |∼ 𝛾
                                                                          𝛼 ∧ 𝛽 |∼ 𝛾    𝛼 |∼ 𝛽              𝛼 |∼ 𝛾    𝛽 |∼ 𝛾
  We can define the flattening 𝜑𝑓 of a PL(=(,))-formula                                        (Cut)                              (Or)
by replacing all dependence atoms by ⊤. It is easy to check                      𝛼 |∼ 𝛾                        𝛼 ∨ 𝛽 |∼ 𝛾
that 𝜑 |= 𝜑𝑓 and that
                                                                       Note that |= is the entailment relation of the underlying
                    {𝑠} |= 𝜑 ⇔ 𝑠 |= 𝜑𝑓                      (1)        monotonic logic L . The rules (Ref), (RW), (LLE), (CM) and
                                                                       (Cut) forming System C. The rule (CM) goes back to the
for all assignments 𝑠 using the fact that dependence atoms             foundational paper on non-monotonic reasoning system
are always satisfied by singletons.                                    by Gabbay (1984) and is a basic wakening of monotonicity.
                                                                       System P consists of all rules of System C and the rule (Or).
                                                                       The rule of (Or) is motivated by reasoning by case [19].
3. Background: Preferential Logics                                     KLM showed a direct correspondence between preferential
                                                                       entailment relations and entailment relations that satisfy
In this section, we present background on preferential logics          System P.
in style of Kraus, Lehmann and Magidor [1].
                                                                       Proposition 9 (Kraus et al. 1990). Let L be a compact
3.1. Preferential Models and Entailment                                Tarskian logic with all Boolean connectives. A entailment
                                                                       relation |∼ ⊆ L × L satisfies System P if and only if |∼ is
In preferential logic, an entailment 𝜙 |∼ 𝜓 holds, when min-           preferential.
imal models of 𝜙 are models of 𝜓. This is formalized via
preferential models, which we introduce in the following.
   For a strict partial order ≺ ⊆ 𝒮 × 𝒮 on a set 𝒮 and a               4. Preferential Team Logics
subset 𝑆 ⊆ 𝒮, an element 𝑠 ∈ 𝑆 is called minimal in 𝑆
with respect to ≺ if for each 𝑠′ ∈ 𝑆 holds 𝑠′ ̸≺ 𝑠. Then,              For propositional team-based logics, we restrict ourselves
min(𝑆, ≺) is the set of all 𝑠 ∈ 𝑆 that are minimal in 𝑆 with           to preferential models that we call standard.
respect to ≺.                                                          Definition 10. A preferential model W = ⟨𝒮, ℓ, ≺⟩ is
Definition 7 ([1]). Let L be a logic and Ω be the set of               called standard if
interpretations for L . A preferential model for L is a triple         (S1) There is no state 𝑠 ∈ 𝒮 such that ℓ(𝑠) = ∅
W = ⟨𝒮, ℓ, ≺⟩ where 𝒮 is a set, ℓ : 𝒮 → Ω, ≺ is a strict
partial order on 𝒮, and the following condition is satisfied:          (S2) For all non-empty teams 𝑋 there is some state 𝑠 ∈ 𝒮
                                                                            such that ℓ(𝑠) = 𝑋
        [Smoothness] 𝑆(𝜙) = {𝑠 ∈ 𝒮 | ℓ(𝑠) |= 𝜙} is
        smooth with respect to ≺ for every formula 𝜙 ∈ L ,                The rationale for (S1) and (S2) is to make the models
        i.e, for each 𝑠 ∈ 𝑆(𝜙) holds                                   concise and meaningful, i.e., containing explicit, yet neces-
            – 𝑠 is minimal in 𝑆(𝜙) with respect to ≺ or                sary information for specifying reasoning. By (S1) we are
            – there exists an 𝑠′ ∈ 𝑆(𝜙) that is minimal in             excluding the empty team ∅ from 𝒮, because team logics
              𝑆(𝜙) with respect to ≺ with 𝑠′ ≺ 𝑠.                      considered here have the empty-team property. Hence, ∅ is
                                                                       trivially a model of every formula and including it provides
 Smoothness guarantees the existence of minimal ele-                   no extra information. Condition (S2) ensures that every
ments.                                                                 "non-trivial" model is included, and thus, its preference sta-
                                                                       tus is explicitly given in the preferential model.
Definition 8 ([1]). The entailment relation |∼W ⊆ L × L                   We define the family of preferential team logics as those
for a preferential model W over a logic L is given by                  that are induced by some standard preferential model.
   𝜙 |∼W 𝜓 if for all 𝑠 ∈ min(𝑆(𝜙), ≺) holds ℓ(𝑠) |= 𝜓                 Definition 11. A entailment relation |∼ over some propo-
                                                                       sitional team logic is called (standard) preferential, if there is
An entailment relation |∼ ⊆ L × L is called preferential if            some standard preferential model W such that |∼ = |∼W .
there is a preferential model W for L such that |∼ = |∼W .
                                                                          The next example is the bird-penguin example, demon-
   Because there are many preferential models for a logic              strating that preferential team logics are indeed non-
L , we may have for one logic L with multiple preferential             monotonic.
logics that are based on L . More precisely, when one con-
siders a logical language ℒ, an entailment relation |= over            Example 12. Fix the set of propositional variables 𝑁 =
ℒ that is based on a model theory with interpretations Ω,              {𝑏, 𝑝, 𝑓 } ⊆ Prop, with the following intended meanings: 𝑏
then there are (infinitely) many different preferential mod-           stands for “it is a bird”, 𝑝 stands for “it is a penguin”, and
els W1 , W2 , . . . for this logic. Many of these preferential
models yield different entailment relations |∼W1 , |∼W2 , . . ..



                                                                   3
Kai Sauerwald et al. CEUR Workshop Proceedings                                                                                    1–7



𝑓 stands for “it is able to fly”. We construct a (standard)                    𝑋 is a model of 𝐴 ∨ 𝐵, then there are teams 𝑌, 𝑍
preferential model, by using the following teams:                              with 𝑋 = 𝑌 ∪ 𝑍 such that 𝑌 |= 𝐴 and 𝑍 |= 𝐵.
                                                                               Because 𝑌, 𝑍 are models of 𝐶 and because PL has
𝑋𝑏𝑝𝑓 =
                  𝑏    𝑝    𝑓
                                   𝑋𝑏𝑝𝑓 =
                                                    𝑏    𝑝    𝑓                the union closure property (see Proposition 5), we
           𝑣1     1    0    1                 𝑣2    1    1    0                obtain that 𝑋 is also a model of 𝐶. Hence, 𝐴 ∨
                                                                               𝐵 |= 𝐶. The proof of statement (b) for PL(⊆) is the
Let Wpeng = ⟨𝒮peng , ℓpeng , ≺peng ⟩ be the preferential model                 same.
such that 𝒮peng = {𝑠𝑋 | 𝑋 is a non-empty team} and
ℓpeng (𝑠𝑋 ) = 𝑋; for all singleton teams 𝑋 different from                 Note that Example 6 is a witness for the second part of
𝑋𝑏𝑝𝑓 and 𝑋𝑏𝑝𝑓 we define:                                                the statement (a) of Proposition 13, i.e., PL(=(,)) violates
                                                                        (Or).
                  𝑋𝑏𝑝𝑓 ≺peng 𝑋𝑏𝑝𝑓 ≺peng 𝑋

for all non-empty teams 𝑌 and non-empty non-singleton                   5.2. System P and Preferential Team Logics
teams 𝑍 we define:                                                      Generally, System C is satisfied by preferential team logics.
                      𝑌 ≺peng 𝑍 if 𝑌 ⊊ 𝑍                                Proposition 14. Let W = ⟨𝒮, ℓ, ≺⟩ be a preferential model
                                                                        for a propositional team logic. The preferential entailment
Then, for |∼ = |∼Wpeng we obtain the following inference:               relation |∼W satisfies System C.

            𝑏 |∼ 𝑓                          (“birds usually fly”)       Proof. We show that |∼W satisfies all rules of System C, i.e.,
           𝑝 |∼ ¬𝑓              (“penguins usually do not fly”)         Ref, LLE, RW, Cut, and CM.
       𝑏 ∧ 𝑝 |̸ ∼ 𝑓        (“penguin birds usually do not fly”)              [Ref.] Considering the definition of |∼W yields that
                                                                               𝛼 |∼W 𝛼 if for all minimal 𝑠 ∈ 𝑆(𝛼) holds ℓ(𝑠) |= 𝛼.
This is because we have:                                                       By the definition of 𝑆(𝛼), we have 𝑠 ∈ 𝑆(𝛼) if
                                                                               ℓ(𝑠) |= 𝛼. Consequently, we have 𝛼 |∼W 𝛼.
                           min(J𝑏K, ≺peng ) = {𝑋𝑏𝑝𝑓 } ⊆ J𝑓 K
min(J𝑝K, ≺peng ) = min(J𝑏 ∧ 𝑝K, ≺peng ) = {𝑋𝑏𝑝𝑓 } ⊆ J¬𝑓 K                    [LLE.] Suppose that 𝛼 ≡ 𝛽 and 𝛼 |∼W 𝛾 holds. From
                                                                               𝛼 ≡ 𝛽, we obtain that 𝑆(𝛼) = 𝑆(𝛽) holds. By using
  Note that Example 12 is agnostic about the concrete team                     this last observation and the definition of |∼W , we
logic used, i.e., it applies to PL, PL(=(,)), and PL(⊆).                       obtain 𝛽 |∼W 𝛾 from 𝛼 |∼W 𝛾.
                                                                             [RW.] Suppose that 𝛼 |= 𝛽 and 𝛾 |∼W 𝛼 holds. Clearly,
5. General Axiomatic Evaluation                                                by definition of 𝛼 |= 𝛽 we have J𝛼K ⊆ J𝛽K. From
                                                                               the definition of 𝛾 |∼W 𝛼, we obtain that ℓ(𝑠) |= 𝛼
We will now present general results on whether System P                        holds for each minimal 𝑠 ∈ 𝑆(𝛾). The condition
holds for non-preferential and preferential team logics.                       ℓ(𝑠) |= 𝛼 in the last statement is equivalent to stat-
                                                                               ing ℓ(𝑠) ∈ J𝛼K. Because of J𝛼K ⊆ J𝛽K, we also have
5.1. System P and Non-Preferential Team                                        ℓ(𝑠) ∈ J𝛽K; and hence, ℓ(𝑠) |= 𝛽 for each minimal
                                                                               𝑠 ∈ 𝑆(𝛾). This shows that 𝛾 |∼W 𝛽 holds.
     Logics
                                                                             [Cut.] Suppose that 𝛼 ∧ 𝛽 |∼W 𝛾 and 𝛼 |∼W 𝛽 holds.
For the entailment |= of propositional team logics, we obtain
                                                                               By unfolding the definition of |∼W , we obtain
that System P is not satisfied by PL(=(,)). For PL and
                                                                               min(𝑆(𝛼 ∧ 𝛽), ≺) ⊆ 𝑆(𝛾) from 𝛼 ∧ 𝛽 |∼W 𝛾. Anal-
PL(⊆), we obtain that they satisfy System P.
                                                                               ogously, 𝛼 |∼W 𝛽 unfolds to min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛽).
Proposition 13. The following statements hold for |=:                          Moreover, employing basic set theory yields that
                                                                               𝑆(𝛼∧𝛽) = 𝑆(𝛼)∩𝑆(𝛽) ⊆ 𝑆(𝛼) holds. From 𝑆(𝛼∧
(a) PL(=(,)) satisfies System C, but violates System P.                        𝛽) ⊆ 𝑆(𝛼) and min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛽), we obtain
                                                                               min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛼 ∧ 𝛽). Consequently, we also
(b) PL (under team semantics) and PL(⊆) satisfy System P.
                                                                               have that min(𝑆(𝛼), ≺) = min(𝑆(𝛼∧𝛽), ≺) holds.
Proof. We show both statements.                                                Using the last observation and min(𝑆(𝛼 ∧ 𝛽), ≺) ⊆
                                                                               𝑆(𝛾), we obtain min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛾). Hence also
     (a) Satisfaction of System C is a corollary of Proposi-                   𝛼 |∼W 𝛾 holds.
        tion 14 and (b) of Proposition 23. The violation of
        (Or) is witnessed by choosing 𝛼, 𝛽 and 𝛾 to be the                   [CM.] Suppose that 𝛼 |∼W 𝛽 and 𝛼 |∼W 𝛾 holds.
        formula =(𝑝) in Example 6.                                             By unfolding the definition of |∼W , we obtain
                                                                               min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛽) and min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛾).
     (b) We start with satisfaction of System C. Note that one                 We have to show that min(𝑆(𝛼 ∧ 𝛽), ≺) ⊆ 𝑆(𝛾)
        can reconstruct non-preferential entailment |= of PL                   holds. Let 𝑠 be element of min(𝑆(𝛼 ∧ 𝛽), ≺).
        by using a preferential model where all teams are                      Clearly, we have that 𝑠 ∈ 𝑆(𝛼) holds. We show
        incomparable. In such a preferential model W one                       by contradiction that 𝑠 is minimal in 𝑆(𝛼). Assume
        has min(J𝛼K, ≺) = J𝛼K. Hence, we have 𝛼 |∼W 𝛽                          that 𝑠 is not minimal in 𝑆(𝛼). From the smoothness
        if and only if J𝛼K ⊆ J𝛽K if and only if 𝛼 |= 𝛽. By                     condition, we obtain that there is an 𝑠′ ∈ 𝑆(𝛼) such
        using this, satisfaction of System C is a corollary of                 that 𝑠′ ≺ 𝑠 and 𝑠′ is minimal in 𝑆(𝛼) with respect
        Proposition 14.                                                        to ≺. Because 𝑠′ is minimal and because we have
        It remains to show that (Or) is satisfied. Let 𝐴, 𝐵 and                min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛽), we also have that 𝑠′ ∈ 𝑆(𝛽)
        𝐶 be PL-formulas such that 𝐴 |= 𝐶 and 𝐵 |= 𝐶. If                       holds and hence that 𝑠′ ∈ 𝑆(𝛼∧𝛽) holds. The latter



                                                                    4
Kai Sauerwald et al. CEUR Workshop Proceedings                                                                                                 1–7



            contradicts the minimality of 𝑠 in 𝑆(𝛼 ∧ 𝛽). Con-                    a preferential model W = ⟨𝒮, ℓ, ≺⟩, where 𝑠, 𝑠′ ∈ 𝒮 are
            sequently, we have that 𝑠 ∈ min(𝑆(𝛼), ≺) holds.                      states:
            Because we have min(𝑆(𝛼), ≺) ⊆ 𝑆(𝛾), we obtain
            𝛼 ∧ 𝛽 |∼W 𝛾.                                                           for all 𝑠, |ℓ(𝑠)| > 1, exists 𝑠′ with ℓ(𝑠′ ) ⊊ ℓ(𝑠) and 𝑠′ ≺ 𝑠
                                                                                                                                                (△)
  The following Example 15 witnesses that, in general, (Or),                     The (△)-property demands (when understanding states as
and hence, System P, is violated by preferential team logics.                    teams) that for each non-singleton team 𝑋 exists a proper
                                                                                 subteam 𝑌 of 𝑋 that is preferred over 𝑋. For this property,
Example 15. Assume that 𝑁 = {𝑝, 𝑞} ⊆ Prop holds. The
                                                                                 we can show the following theorem.
following valuations 𝑣1 , 𝑣2 , 𝑣3 will be important:
                                                                                 Theorem 18. Let W = ⟨𝒮, ℓ, ≺⟩ be a preferential model for
𝑣1 (𝑝) = 𝑣1 (𝑞) = 𝑣2 (𝑞) = 1            𝑣2 (𝑝) = 𝑣3 (𝑝) = 𝑣3 (𝑞) = 0             PL(=(,)). The following statements are equivalent:
We consider the teams 𝑋𝑝𝑞 = {𝑣1 }, 𝑋𝑝𝑞 = {𝑣2 }, and                                (i) |∼W satisfies System P.
𝑋𝑝↔𝑞 = {𝑣1 , 𝑣3 }. Let Wpq = ⟨𝒮pq , ℓpq , ≺pq ⟩ be the prefer-
ential model such that                                                            (ii) W satisfies the △-property.

     𝒮pq = {𝑠𝑋 | 𝑋 is a non-empty team}               ℓpq (𝑠𝑋 ) = 𝑋              (iii) The (⋆)-property holds for all 𝐴, 𝐵 ∈ PL(=(,)).

holds, and such that ≺pq is the strict partial order given by2                      We will obtain the proof of the theorem via the following
                                                                                 lemmata.
               𝑋𝑝↔𝑞 ≺pq 𝑋𝑝𝑞                    𝑋𝑝𝑞 ≺pq 𝑋                            For the first lemma, assume that 𝑁 = {𝑝1 , . . . , 𝑝𝑛 }, and
                                                                                 let 𝑋 a team over 𝑁 . We define the following formula:
               𝑋𝑝↔𝑞 ≺pq 𝑋𝑝𝑞                    𝑋𝑝𝑞 ≺pq 𝑋
                                                                                                          ⋁︁ 𝑣
where 𝑋 stands for every team different from 𝑋𝑝𝑞 and                                               Θ𝑋 :=     (𝑝1 ∧ · · · ∧ 𝑝𝑣𝑛 ),
𝑋𝑝↔𝑞 . We obtain the following preferential entailments:                                                  𝑣∈𝑋


                                                                                 whereby 𝑝𝑣𝑖 stands for 𝑝𝑖 if 𝑣(𝑝1 ) = 1 holds and for ¬𝑝𝑖
           𝑝 |∼Wpq 𝑞         ¬𝑝 |∼Wpq 𝑞          𝑝 ∨ ¬𝑝 |̸ ∼Wpq 𝑞
                                                                                 if 𝑣(𝑝𝑖 ) = 0 holds. This formula is of crucial importance
                                                                                 for proving Theorem 18. It is straightforward to check the
Proposition 16. The entailment relation |∼Wpq for PL, re-
                                                                                 following lemma.
spectively PL(=(,)) and PL(⊆), violates (Or).
                                                                                 Lemma 19. Θ𝑋 defines the family of subteams of 𝑋, i.e.,
   We can reestablish satisfaction of System P, by demand-                       we have
ing the (⋆)-property, which we define below in Proposi-                                      𝑌 |= Θ𝑋 ⇐⇒ 𝑌 ⊆ 𝑋.
tion 17. In the following we abuse notation and mean
by min(J𝐴K, ≺) the set of ≺-minimal states in 𝒮(𝐴), as                             The next lemma guarantees that for a sufficient large
well as the set of al models ℓ(𝑠) of 𝐴 for which a ≺-                            enough teams 𝑋 exist formulas 𝐴, 𝐵 such that 𝑋 is a
minimal states 𝑠 in 𝒮(𝐴) exists. More technically correct                        model of the disjunction 𝐴 ∨ 𝐵, but 𝑋 is not a model of
would be to write min(𝑆(𝐴), ≺) for the former, and writing                       𝐴 and 𝐵. We make use of the following notions: define
{ℓ(𝑠) | 𝑠 ∈ min(𝑆(𝐴), ≺)} for the latter.                                        down(𝑋) = {𝑌 | 𝑌 ⊆ ⋃︀     𝑋} and down(𝑋1 , . . . , 𝑋𝑛 ) =
                                                                                 down({𝑋1 , . . . , 𝑋𝑛 }) = 𝑛
                                                                                                            𝑖=1 down(𝑋𝑖 )
Proposition 17. Let W be a preferential model for some
preferential team logic. If (⋆) is satisfied for all formulas                    Lemma 20 (†). For each team 𝑋 with |𝑋| > 1 exists for-
𝐴, 𝐵, then |∼W satisfies System P, whereby3 :                                    mulas 𝐴 and 𝐵 such that

      min(J𝐴 ∨ 𝐵K, ≺) ⊆ min(J𝐴K, ≺) ∪ min(J𝐵K, ≺)                     (⋆)                                𝑋 |= 𝐴 ∨ 𝐵 ,
                                                                                                         𝑋 ̸|= 𝐴 , and
Proof. Suppose that 𝐴 |∼ 𝛾 and 𝐵 |∼ 𝛾 holds. This is the
same as min(J𝐴K, ⪯) ⊆ J𝛾K and min(J𝐵K, ⪯) ⊆ J𝛾K. Be-                                                     𝑋 ̸|= 𝐵
cause (⋆) holds, this also means that min(J𝐴 ∨ 𝐵K, ⪯) ⊆
J𝛾K holds.                                                                       Proof. Since we have |𝑋| > 1, there exists non-empty
                                                                                 𝑌, 𝑍 ⊆ 𝑋 teams such that 𝑋 = 𝑌 ∪ 𝑍 and 𝑌 ̸= 𝑋 and
                                                                                 𝑍 ̸= 𝑋. Moreover, there are formulas 𝐴 and 𝐵 such that
6. Results for Preferential                                                      J𝐴K = down(𝑌 ) and J𝐵K = down(𝑍), namely 𝐴 = Θ𝑌
                                                                                 and 𝐵 = Θ𝑍 .
   Dependence Logics
                                                                                   We will now show that the (△)-property and the (⋆)-
For preferential dependence logic, we provide additional                         property describe the same preferential models.
results to those of Section 5.
                                                                                 Lemma 21. Let W = ⟨𝒮, ℓ, ≺⟩ be a preferential model
6.1. System P and Preferential Dependence                                        over PL(=(,)). The preferential entailment relation |∼W over
                                                                                 PL(=(,)) satisfies (△) if and only if (⋆) is satisfied.
     Logic
The main contribution is a characterization of exactly those                     Proof. Assume (△) holds. Then it is easy to see that the
preferential entailment relations that satisfy all rules of Sys-                 minimal elements of the order ≺ are states that are mapped,
tem P. Central to this result is the following property for                      via ℓ, to singleton teams. Furthermore, by the downward
                                                                                 closure property, for any 𝐴∨𝐵 the minimal teams satisfying
2
    For the sake of readability we abuse notation and identify 𝑠𝑋 with 𝑋 .       the formula are all singletons. Since for singleton teams the
3
    Abbreviation: min(J𝐴K, ≺) = {ℓ(𝑠) | 𝑠 ∈ min(𝑆(𝐴), ≺)}




                                                                             5
Kai Sauerwald et al. CEUR Workshop Proceedings                                                                                                    1–7



interpretation of ∨ is equivalent with that of the Boolean                           As a last result, we consider preferential models that
disjunction the property (⋆) follows.                                             characterize the |= entailment relation, as well as the en-
   For the converse, assume that (⋆) holds and let 𝑋 be a                         tailment relation for classical formulas |=𝑐 . Let Wsub =
team with |𝑋| > 1. We will show that then there is some                           ⟨𝒮sub , ℓsub , ≺sub ⟩ and Wsup = ⟨𝒮sup , ℓsup , ≺sup ⟩ be the prefer-
team 𝑌 with                                                                       ential models such that the following holds:

                                𝑌 ⊊𝑋,                                                    𝒮sub = 𝒮sup = {𝑠𝑋 | 𝑋 is a non-empty team}
                                𝑌 ̸= ∅ , and                                             ℓsub (𝑠𝑋 ) = ℓsup (𝑠𝑋 ) = 𝑋
                                𝑌 ≺𝑋                                                     𝑌 ≺sub 𝑋 if 𝑌 ⊊ 𝑋            𝑌 ≺sup 𝑋 if 𝑋 ⊊ 𝑌

Because 𝑋 contains at least two valuations, there exist                           In Wsub and Wsup , for each team 𝑋 there is exactly one state
𝑌, 𝑍 ⊆ 𝑋 such that 𝑋 = 𝑌 ∪ 𝑍 and 𝑌 ̸= 𝑋 and                                       𝑠𝑋 that is labelled by 𝑋. In ≺sub , subsets of a team are
𝑍 ̸= 𝑋. By (the proof of) Lemma 20 there are formu-                               preferred, whereas in ≺sup superset teams are preferred.
las 𝐴 = Θ𝑌 and 𝐵 = Θ𝑍 such that 𝑋 |= 𝐴 ∨ 𝐵, yet                                      The preferential model Wsup gives rise to the PL(=(,))
𝑋 ̸|= 𝐴 and 𝑋 ̸|= 𝐵. Using this and (⋆), we obtain that                           entailment relation |=, and the preferential model Wsup gives
𝑋∈  / min(𝐴 ∨ 𝐵, ≺) holds. However, by smoothness of ≺,                           rise to classical entailment of the flattening |=𝑐 .
the set 𝑀 𝑜𝑑(𝐴 ∨ 𝐵) = 𝒫(𝑋) contains a team 𝑋 ′ such that
𝑋 ′ ≺ 𝑋. Now 𝑋 ′ is a witness for the (△)-Property.                               Proposition 23. For all PL(=(,))-formulas 𝐴, 𝐵 we have:

      Now we are ready to give the proof of Theorem 18.                           (1) 𝐴 |∼Wsub 𝐵 if and only if 𝐴𝑓 |=𝑐 𝐵 𝑓

Proof of Theorem 18. By Lemma 21, it suffices to show (⋆)                         (2) 𝐴 |∼Wsup 𝐵 if and only if 𝐴 |= 𝐵
⇒ (Or) and (Or) ⇒ (△). We show each direction indepen-
dently:                                                                           Proof. We show statements (1) and (2).

         (⋆) ⇒ (Or). This is given by Proposition 17.                                  (1) Observe at first that we have 𝐴 |∼Wsub 𝐵 exactly
         (Or) ⇒ (△). Assume, for a contradiction, that (△) fails.                         when we also have min(J𝐴K, ≺sub ) ⊆ J𝐵K. Because
            Then there exists a team 𝑋 of size 𝑗 ≥ 2 such that                            PL(=(,)) has the downwards closure property, we
            for all 𝑌 ⊆ 𝑋, 𝑌 ̸≺ 𝑋. Let 𝑗 = 𝑙 + 𝑘 (𝑙, 𝑘 ≥ 1 and                            also have that stating min(J𝐴K, ≺sub ) ⊆ J𝐵K is
            𝑙 ≤ 𝑘) and define                                                             equivalent to stating that for all singleton teams {𝑣}
                                                                                          holds that {𝑣} |= 𝐴 implies {𝑣} |= 𝐵. The latter
                          𝛼 := Θ𝑋 ∧ (𝜃 ∨ · · · ∨ 𝜃),                                      statement is equivalent to stating that for the flatten-
                                                                                          ing 𝐴𝑓 and 𝐵 𝑓 holds that for all valuations 𝑣 holds
            where 𝜃 := 1≤𝑖≤𝑛 =(𝑝𝑖 ) and 𝛼 has 𝑙 many copies                               that 𝑣 |= 𝐴𝑓 implies 𝑣 |= 𝐵 𝑓 (see also Section 2).
                         ⋀︀
            of 𝜃. It is easy to check that 𝛼 is satisfied by sub-                         Hence, we have 𝐴 |∼Wsub 𝐵 if and only if 𝐴𝑓 |=𝑐
            teams of 𝑋 of cardinality at most 𝑙. The formula 𝛽 is                         𝐵𝑓 .
            defined similarly with 𝑘 copies of 𝜃 in the disjuncts.                     (2) We obtain |= ⊆ |∼Wsup immediately by the defi-
            Now it holds that 𝛽 |= 𝛽, 𝛼 |= 𝛽 but 𝑋 ̸|= 𝛼, 𝛽. Us-
                                                                                          nition of |∼Wsup . We consider the other direction.
            ing reflexivity and right weakening, it follows that
            𝛽 |∼W 𝛽 and 𝛼 |∼W 𝛽. On the other hand, since 𝑋 is                            The statement 𝐴 |= 𝐵 is equivalent to J𝐴K ⊆ J𝐵K.
            now a minimal model of 𝛼 ∨ 𝛽 that does not satisfy                            Because J𝐴K is downward-closed, there are (pair-
            𝛽 we have shown 𝛼 ∨ 𝛽 |̸ ∼W 𝛽 and that (Or) fails for                         wise ⊆-incomparable) teams 𝑋1 , . . . , 𝑋𝑛 such that
             |∼W .                                                                        J𝐴K = down(𝑋1 , . . . , 𝑋𝑛 ). Because of the last
                                                                                          property, we have that 𝐴 |= 𝐵 holds exactly when
                                                                                          {𝑋1 , . . . , 𝑋𝑛 } ⊆ J𝐵K holds. By construction of
6.2. Relation to Dependence Logic and                                                     Wsup we have min(J𝐴K, ≺sup ) = {𝑋1 , . . . , 𝑋𝑛 } for
     Classical Entailment                                                                 𝐴. Consequently, we also have that 𝐴 |∼Wsup 𝐵 holds
Theorem 18 and the △-property imply that preferential                                     and consequently, we also have |∼Wsup ⊆ |=.
dependence logics that satisfy System P are quintessentially
the same as their flattening4 counterpart in (preferential)                          Note that, in conformance with Theorem 18 and Proposi-
propositional logic with classical (non-team) semantics.                          tion 13, Wsup violates the (△)-property and (⋆)-property.

Theorem 22. Let W = ⟨𝒮, ℓ, ≺⟩ be a preferential model
over PL(=(,)) that satisfies System P. Then 𝐴 |∼W 𝐵 iff                           7. Conclusion
𝐴𝑓 |∼W′ 𝐵 𝑓 , where W′ = ⟨𝒮 ′ , ℓ′ , ≺′ ⟩ denotes the prefer-
                                                                                  We considered preferential propositional team logics, which
ential model for classical propositional logic induced by W,
                                                                                  are non-monotonic logics in the style of Kraus et al.. Our
i.e., over |=𝑐 for PL formulas and valuations induced by the
                                                                                  results are a primer for further investigations on non-
singleton teams in 𝑊 .
                                                                                  monotonic team logics. We want to highlight that The-
Proof. Note first that by the assumption for all valuations                       orem 22 indicates that (Or) of System P is too restrictive
𝑠, 𝑠′ it holds that 𝑠 ≺′ 𝑠′ iff {𝑠} ≺ {𝑠′ }. By theorem 18, 𝑊                     for non-monotonic team logics. In future work, the authors
satisfies the (△)-property and hence the minimal elements                         plan to identify further results on preferential models, es-
of ≺ are singleton teams. Hence 𝐴 |∼ 𝐵, iff, for all minimal                      pecially with respect to axiomatic systems different from
{𝑠} ∈ J𝐴K : {𝑠} |= 𝐵, iff, for all ≺′ -minimal 𝑠 ∈ J𝐴𝑓 K :                        System P. Connected with that is to study the meaning of
𝑠 |= 𝐵 𝑓 . The last equivalence holds due to (1).                                 conditionals and related complexity issues in the setting of
                                                                                  team logics.
4
    Note that the flatting of a formula is defined at the end of Section 2.




                                                                              6
Kai Sauerwald et al. CEUR Workshop Proceedings                                                                                 1–7



References                                                          [15] D. Makinson, P. Gärdenfors, Relations between the
                                                                         logic of theory change and nonmonotonic logic, in:
 [1] S. Kraus, D. Lehmann, M. Magidor, Nonmonotonic                      A. Fuhrmann, M. Morreau (Eds.), The Logic of Theory
     reasoning, preferential models and cumulative log-                  Change, Springer, Berlin, Heidelberg, 1991, pp. 183–
     ics, Artif. Intell. 44 (1990) 167–207. URL: https://                205.
     doi.org/10.1016/0004-3702(90)90101-5. doi:10.1016/             [16] M. Ragni, G. Kern-Isberner, C. Beierle, K. Sauerwald,
     0004-3702(90)90101-5.                                               Cognitive logics - features, formalisms, and challenges,
 [2] J. Väänänen, Dependence Logic, Cambridge University                 in: G. D. Giacomo, A. Catalá, B. Dilkina, M. Milano,
     Press, 2007.                                                        S. Barro, A. Bugarín, J. Lang (Eds.), Proceedings of the
 [3] P. Galliani, Inclusion and exclusion dependencies in                24nd European Conference on Artificial Intelligence
     team semantics: On some logics of imperfect informa-                (ECAI 2020), volume 325 of Frontiers in Artificial Intelli-
     tion, Annals of Pure and Applied Logic 163 (2012) 68 –              gence and Applications, IOS Press, 2020, pp. 2931–2932.
     84.                                                                 doi:10.3233/FAIA200459.
 [4] M. Hannula, J. Kontinen, J. Virtema, Polyteam                  [17] P. Gärdenfors, D. Makinson, Nonmonotonic infer-
     semantics, J. Log. Comput. 30 (2020) 1541–1566.                     ence based on expectations, Artif. Intell. 65 (1994)
     URL: https://doi.org/10.1093/logcom/exaa048. doi:10.                197–245. URL: https://doi.org/10.1016/0004-3702(94)
     1093/logcom/exaa048.                                                90017-5. doi:10.1016/0004-3702(94)90017-5.
 [5] M. Hannula, J. Kontinen, A finite axiomatization of            [18] D. M. Gabbay, Theoretical foundations for non-
     conditional independence and inclusion dependen-                    monotonic reasoning in expert systems, in: K. R.
     cies, Inf. Comput. 249 (2016) 121–137. URL: https:                  Apt (Ed.), Logics and Models of Concurrent Sys-
     //doi.org/10.1016/j.ic.2016.04.001. doi:10.1016/j.ic.               tems - Conference proceedings, Colle-sur-Loup (near
     2016.04.001.                                                        Nice), France, 8-19 October 1984, volume 13 of NATO
 [6] J. O. Gutsfeld, A. Meier, C. Ohrem, J. Virtema, Tem-                ASI Series, Springer, 1984, pp. 439–457. URL: https://
     poral team semantics revisited, in: C. Baier, D. Fis-               doi.org/10.1007/978-3-642-82453-1_15. doi:10.1007/
     man (Eds.), LICS ’22: 37th Annual ACM/IEEE Sym-                     978-3-642-82453-1\_15.
     posium on Logic in Computer Science, Haifa, Is-                [19] J. Pearl, Probabilistic reasoning in intelligent systems
     rael, August 2 - 5, 2022, ACM, 2022, pp. 44:1–44:13.                - networks of plausible inference, Morgan Kaufmann
     URL: https://doi.org/10.1145/3531130.3533360. doi:10.               series in representation and reasoning, Morgan Kauf-
     1145/3531130.3533360.                                               mann, 1989.
 [7] M. Hannula, J. Kontinen, J. V. den Bussche, J. Virtema,        [20] A. Durand, J. Kontinen, H. Vollmer,               Expres-
     Descriptive complexity of real computation and proba-               sivity and complexity of dependence logic, in:
     bilistic independence logic, in: H. Hermanns, L. Zhang,             S. Abramsky, J. Kontinen, J. Väänänen, H. Vollmer
     N. Kobayashi, D. Miller (Eds.), LICS ’20: 35th Annual               (Eds.), Dependence Logic, Theory and Applica-
     ACM/IEEE Symposium on Logic in Computer Science,                    tions, Springer, 2016, pp. 5–32. URL: https://
     Saarbrücken, Germany, July 8-11, 2020, ACM, 2020,                   doi.org/10.1007/978-3-319-31803-5_2. doi:10.1007/
     pp. 550–563. URL: https://doi.org/10.1145/3373718.                  978-3-319-31803-5\_2.
     3394773. doi:10.1145/3373718.3394773.                          [21] M. Hannula, J. Kontinen, J. Virtema, H. Vollmer, Com-
 [8] I. Ciardelli, R. Iemhoff, F. Yang, Questions and De-                plexity of propositional logics in team semantic, ACM
     pendency in Intuitionistic Logic, Notre Dame Jour-                  Trans. Comput. Log. 19 (2018) 2:1–2:14.
     nal of Formal Logic 61 (2020) 75 – 115. URL: https:            [22] F. Yang, J. Väänänen, Propositional logics of depen-
     //doi.org/10.1215/00294527-2019-0033. doi:10.1215/                  dence, Ann. Pure Appl. Logic 167 (2016) 557–589.
     00294527-2019-0033.                                                 URL: https://doi.org/10.1016/j.apal.2016.03.003. doi:10.
 [9] P. Galliani, The doxastic interpretation of team seman-             1016/j.apal.2016.03.003.
     tics, in: Logic Without Borders, volume 5 of Ontos
     Mathematical Logic, De Gruyter, 2015, pp. 167–192.
[10] A. Durand, M. Hannula, J. Kontinen, A. Meier,
     J. Virtema, Approximation and dependence via multi-
     team semantics, Ann. Math. Artif. Intell. 83 (2018) 297–
     320. URL: https://doi.org/10.1007/s10472-017-9568-4.
[11] A. Durand, M. Hannula, J. Kontinen, A. Meier,
     J. Virtema, Probabilistic team semantics, in: Founda-
     tions of Information and Knowledge Systems - 10th
     International Symposium, FoIKS 2018, Budapest, Hun-
     gary, May 14-18, 2018, Proceedings, 2018, pp. 186–
     206. URL: https://doi.org/10.1007/978-3-319-90050-6_
     11. doi:10.1007/978-3-319-90050-6\_11.
[12] T. Barlag, M. Hannula, J. Kontinen, N. Pardal,
     J. Virtema, Unified foundations of team semantics
     via semirings, in: KR, 2023, pp. 75–85.
[13] D. M. Gabbay, C. J. Hogger, J. A. Robinson, Handbook
     of Logic in Artificial Intelligence and Logic Program-
     ming, 1993.
[14] G. Brewka, J. Dix, K. Konolige, Nonmonotonic Reason-
     ing: An Overview, volume 73 of CSLI Lecture Notes,
     CSLI Publications, Stanford, CA, 1997.



                                                                7