{'fraction_non_alphanumeric': 0.060160532498042284, 'fraction_numerical': 0.013429913860610806, 'mean_word_length': 3.6530333394060848, 'pattern_counts': {'":': 0, '<': 20, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 86, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A logic for reasoning about upper probabilities

We present a propositional logic %which can be used to reason about the uncertainty of events, where the uncertainty is modeled by a set of probability measures assigning an interval of probability to each event. We give a sound and complete axiomatization for the logic, and show that the satisfiability problem is NP-complete, no harder than satisfiability for propositional logic.


Introduction
Various measures exist that attempt to quantify uncertainty. For many trained in the use of probability theory, probability measures are an obvious choice. However, probability cannot easiliy capture certain situations of interest. Consider a simple example: suppose we have a bag of 100 marbles; we know 30 are red and we know the remaining 70 are either blue or yellow, although we do not know the exact proportion of blue and yellow. If we are modeling the situation where we pick a ball from the bag at random, we need to assign a probability to three different events: picking up a red ball (red-event), picking up a blue ball (blue-event), and picking up a yellow ball (yellow-event). We can clearly assign a probability of .3 to red-event, but there is no clear probability to assign to blue-event or yellow-event.
One way to approach this problem is to represent the uncertainty using a set of probability measures, with a probability measure for each possible proportion of blue and yellow balls. For instance, we could use the set of probabilities P = {µ α : α ∈ [0, .7]}, where µ α gives red-event probability .3, blue-event probability α, and yellow-event probability .7 − α. To any set of probabilities P we can assign a pair of functions, the upper and lower probability measure, that for an event X give the supremum (respectively, the infimum) of the probability of X according to the probability measures in P. These measures can be used to deal with uncertainty in the manner described above, where the lower and upper probability of an event defines a range of probability for that event. 1 (This example can be viewed as giving a frequentist interpretation of upper probabilities. Upper probabilities can also be given a subjective interpretation, for example, by considering the odds at which someone would be willing to accept or reject a bet (Smith, 1961;Walley, 1991).) Given a measure of uncertainty, one can define a logic for reasoning about it. Fagin, Halpern and Megiddo (1990) (FHM from now on) introduce a logic for reasoning about probabilities, with a possible-worlds semantics that assigns a probability to each possible world. They provide an axiomatization for the logic, which they prove sound and complete with respect to the semantics. They also show that the satisfiability problem for the logic, somewhat surprisingly, is NP-complete, and hence no harder than the satisfiability problem for propositional logic. They moreover show how their logic can be extended to other notions of uncertainty, such as inner measures (Fagin & Halpern, 1991) and Dempster-Shafer belief functions (Shafer, 1976).
In this paper, we describe a logic for reasoning about upper probability measures, along the lines of the FHM logic. The logic allows reasoning about linear inequalities involving upper probabilities measures. Like the logics considered in FHM, our logic is agnostic as to the interpretation of upper probabilities, whether frequentist or subjectivist. The main challenge is to derive a provably complete axiomatization of the logic; to do this, we need a characterization of upper probability measures in terms of properties that can be expressed in the logic. Many semantic characterizations of upper probability measures have been proposed in the literature. The characterization of Anger and Lembcke (1985) turns out to be best suited for our purposes. Even though we are reasoning about potentially infinite sets of probability measures, the satisfiability problem for our logic remains NPcomplete. Intuitively, we need guess only a small number of probability measures to satisfy any given formula, polynomially many in the size of the formula. Moreover, these probability measures can be taken to be defined on a finite state space, again polynomial in the size of the formula. Thus, we need to basically determine polynomially many values-a value for each probability measure at each state-to decide the satisfiability of a formula.
The rest of this paper is structured as follows. In Section 2, we review the required material from probability theory and the theory of upper probabilities. In Section 3, we present the logic and an axiomatization. In Section 4, we prove that the axiomatization is sound and complete with respect to the natural semantic models expressed in terms of upper probability spaces. Finally, in Section 5, we prove that the decision problem for the logic is NP-complete. The proofs of the new, more technical results are given in Appendix A. To make the paper self-contained, we also review Anger and Lembcke's results in Appendix B.

Characterizing Upper Probability Measures
We start with a brief review of the relevant definitions. Recall that a probability measure is a function µ : Σ → [0, 1] for Σ an algebra of subsets of Ω (that is Σ is closed under complements and unions), satisfying µ(∅) = 0, µ(Ω) = 1, and µ(A ∪ B) = µ(A) + µ(B) for all disjoint sets A, B in Σ. 2 A probability space is a tuple (Ω, Σ, µ), where Ω is a set, Σ is an algebra of subsets of Ω (the measurable sets), and µ is a probability measure defined on Σ. Given a set P of probability measures, let P * be the upper probability measure defined 2. If Ω is infinite, we could also require that Σ be a σ-algebra (i.e., closed under countable unions) and that µ be countably additive. Requiring countable additivity would not affect our results, since we show that we can take Ω to be finite. For ease of exposition, we have not required it.
by P * (X) = sup{µ(X) : µ ∈ P} for X ∈ Σ. 3 Similarly, P * (X) = inf{µ(X) : µ ∈ P} is the lower probability of X ∈ Σ. A straightforward derivation shows that the relationship P * (X) = 1−P * (X) holds between upper and lower probabilities, where X is the complement of X in Ω. Because of this duality, we restrict the discussion to upper probability measures in this paper, with the understanding that results for lower probabilities can be similarly derived. Finally, an upper probability space is a tuple (Ω, Σ, P) where P is a set of probability measures on Σ. We would like a set of properties that completely characterizes upper probability measures. In other words, we would like a set of properties that allow us to determine if a function f : Σ → R (for an algebra Σ of subsets of Ω) is an upper probability measure, that is, whether there exists a set P of probability measures such that for all X ∈ Σ, P * (X) = f (X). 4 One approach to the characterization of upper probability measures is to adapt the characterization of Dempster-Shafer belief functions; these functions are known to be the lower envelope of the probability measures that dominate them, and thus form a subclass of the class of lower probability measures. By the duality noted earlier, a characterization of lower probability measures would yield a characterization of upper probability measures. The characterization of belief functions is derived from a generalization of the following inclusion-exclusion principle for probabilities (obtained by replacing the equality with an inequality): It seems reasonable that a characterization of lower (or upper) probability measures could be derived along similar lines. However, as is well known, most properties derivable from the inclusion-exclusion principle (which include most of the properties reported in the literature) are insufficient to characterize upper probability measures. Huber (1981, p. 257) and Walley (1991, p. 85) give examples showing the insufficiencies of such properties.
To give a sense of the insufficiency of simple properties, consider the following "inclusionexclusion"-style properties, some of which are taken from (Walley, 1991). To simplify the statement of these properties, let P −1 = P * and P +1 = P * . (1) 3. In the literature, the term upper probability is sometimes used in a more restricted sense than here. For example, Dempster (1967) uses the term to denote a class of measures which were later characterized as Dempster-Shafer belief functions (Shafer, 1976); belief functions are in fact upper probability measures in our sense, but the converse is not true (Kyburg, 1987). In the measure theory literature, what we call upper probability measures are a special case of upper envelopes of measures, which are defined as the sup of sets of general measures, not just probability measures. 4. It is possible to define a notion of upper probability over an arbitrary set of subsets of Ω, not necessearily an algebra, by simply requiring that f coincides with P * on its domain, for some set P of probability measures. See Walley (1991) for details.
(4) P * (A) + P * (B) ≤ P * (A ∪ B) + P * (A ∩ B) ≤ P * (A) + P * (B), Note that without the alternation between upper probabilities and lower probabilities, (1) and (2) would just be the standard notions of subadditivity and superadditivity, respectively. While subadditivity and superadditivity hold for upper and lower probabilities, respectively, (1) and (2) are stronger properties. It is easily verified that all five properties hold for upper probability measures. The question is whether they completely characterize the class of upper probability measures. We show the inherent incompleteness of these properties by proving that they are all derivable from the following simple property, which is by itself insufficient to characterize upper probability measures: Proposition 2.1: Property (6) implies properties (1)-(5).
Observe that our property (6) is already given by Walley (1991, p. 84), as properties (d) and (e). The following example shows the insufficiency of Property (6). Let P be the set of probability measures {µ 1 , µ 2 , µ 3 , µ 4 } over Ω = {a, b, c, d} (with Σ containing all subsets of Ω) defined on singletons by and extended by additivity to all of Σ. This defines an upper probability measure P * over Σ. Consider the function υ ǫ : Σ → [0, 1] defined by We claim that the function υ ǫ , for small enough ǫ > 0, satisfies property (6), but cannot be an upper probability measure.
Proposition 2.2: For 0 < ǫ < 1 8 , the function υ ǫ satisfies property (6), but is not an upper probability measure. That is, we cannot find a set P ′ of probability measures such that υ ǫ = (P ′ ) * .
This example clearly illustrates the need to go beyond the inclusion-exclusion principle to find properties that characterize upper probability measures. As it turns out, various complete characterizations have been described in the literature (Lorentz, 1952;Huber, 1976Huber, , 1981Williams, 1976;Wolf, 1977;Giles, 1982;Anger & Lembcke, 1985;Walley, 1991). Most of these characterizations are obtained by considering upper and lower expectations, rather than working directly with upper and lower probabilities. Anger and Lembcke (1985) give a characterization in terms of upper and lower probabilities. Since their characterization is particularly well-suited to the logic presented in the next section, we review it here.
The characterization is based on the notion of set cover. A set A is said to be covered n times by a multiset {{A 1 , . . . , A m }} of sets if every element of A appears in at least n sets from A 1 , . . . , A m : for all x ∈ A, there exists distinct i 1 , . . . , i n in {1, . . . , m} such that for all j ≤ n, x ∈ A i j . It is important to note here that {{A 1 , . . . , A m }} is a multiset, not a set; the A i 's are not necessarily distinct. (We use the {{ }} notation to denote multisets.) An (n, k)-cover of (A, Ω) is a multiset {{A 1 , . . . , A m }} that covers Ω k times and covers A n + k times. The notion of (n, k)-cover is the key concept in Anger and Lembcke's characterization of upper probability measures.
Theorem 2.3: (Anger & Lembcke, 1985) Suppose that Ω is a set, Σ is an algebra of subsets of Ω, and υ : Σ → R. Then there exists a set P of probability measures with υ = P * if and only if υ satisfies the following three properties:

UP3. for all natural numbers m, n, k and all subsets
Proof: We reproduce a proof of this result in Appendix B.
We need to strengthen Theorem 2.3 in order to prove the main result of this paper, namely, the completeness of the axiomatization of the logic we introduce in the next section. We show that if the cardinality of the state space Ω is finite, then we need only finitely many instances of property UP3. Notice that we cannot derive this from Theorem 2.3 alone: even if |Ω| is finite, UP3 does not provide any bound on m, the number of sets to consider in an (n, k) cover of a set A. Indeed, there does not seem to be any a priori reason why the value of m, n, and k can be bounded. Bounding this value of m (and hence of n and k, since they are no larger than m) is one of the key technical results of this paper, and a necessary foundation for our work. Property UPF3 is significantly weaker than UP3. In principle, checking that UP3 holds for a given function requires checking that it holds for arbitrarily large collections of sets, even if the underlying set Ω is finite. On the other hand, UPF3 guarantees that if Ω is finite, then it is in fact sufficient to look at collections of size at most B |Ω| . This observation is key to the completeness result.
Theorem 2.4 does not prescribe any values for the constants B 0 , B 1 , . . . . Indeed, the proof found in Appendix A relies on a Ramsey-theoretic argument that does not even provide a bound on the B i 's. We could certainly attempt to obtain such bounds, but obtaining them is completely unnecessary for our purposes. To get completeness of the axiomatization of the logic introduced in the next section, it is sufficient for there to exist finite constants B 0 , B 1 , . . . .

The Logic
The syntax for the logic is straightforward, and is taken from FHM. We fix a set Φ 0 = {p 1 , p 2 , . . . } of primitive propositions. The set Φ of propositional formulas is the closure of Φ 0 under ∧ and ¬. We assume a special propositional formula true, and abbreviate ¬true as false. We use p to represent primitive propositions, and ϕ and ψ to represent propositional formulas. A term is an expression of the form θ 1 l(ϕ 1 ) + · · · + θ k l(ϕ k ), where θ 1 , . . . , θ k are reals and k ≥ 1. A basic likelihood formula is a statement of the form t ≥ α, where t is a term and α is a real. A likelihood formula is a Boolean combination of basic likelihood formulas. We use f and g to represent likelihood formulas. We use obvious abbreviations where needed, such as l(ϕ) − l(ψ) ≥ a for l(ϕ) + (−1)l(ψ) ≥ a, l(ϕ) ≥ l(ψ) for l(ϕ) − l(ψ) ≥ 0, l(ϕ) ≤ a for −l(ϕ) ≥ −a, l(ϕ) < a for ¬(l(ϕ) ≥ a) and l(ϕ) = a for (l(ϕ) ≥ a) ∧ (l(ϕ) ≤ a). Define the length |f | of the likelihood formula f to be the number of symbols required to write f , where each coefficient is counted as one symbol. Let L QU be the language consisting of likelihood formulas. (The QU stands for quantitative uncertainty. The name for the logic is taken from (Halpern, 2001).) In FHM, the operator l was interpreted as either "probability" or "belief" (in the sense of Dempster-Shafer). Under the first interpretation, a formula such as l(ϕ) + l(ψ) ≥ 2/3 would be intereted as "the probability of ϕ plus the probability of ψ is at least 2/3". Here we interpret l as upper probaiblity. Thus, the logic allows us to make statements about inequalities involving upper probabilities.
To capture this interpretation, we assign a semantics to formulas in L QU using an upper probability space, as defined in Section 2. Formally, an upper probability structure is a tuple M = (Ω, Σ, P, π) where (Ω, Σ, P) is an upper probability space and π associates with each state (or world) in Ω a truth assignment on the primitive propositions in Φ 0 . Thus, is measurable for all propositional formulas ϕ. In this paper, we restrict our attention to measurable upper probability structures. Extend π(s) to a truth assignment on all propositional formulas in a standard way, and associate with each propositional formula the set [[ϕ]] M = {s ∈ Ω : π(s)(ϕ) = true}. An easy structural induction shows that Note that L QU can express lower probabilities: it follows from the duality between upper and lower probabilities that Consider the following axiomatization AX up of upper probability, which we prove sound and complete in the next section. The key axioms are simply a translation into L QU of the characterization of upper probability given in Theorem 2.3. As in FHM, AX up is divided into three parts, dealing respectively with propositional reasoning, reasoning about linear inequalities, and reasoning about upper probabilities.

Propositional reasoning
Taut. All instances of propositional tautologies in L QU (see below).
MP. From f and f =⇒ g infer g.
On the other hand, interpreting l as an upper probability measure is more in keeping with the literature on upper probabilities. 6. Note that, according to the syntax of L QU , ϕ1, . . . , ϕm must be propositional formulas.
UP3. Note that in the same way that UP1 follows from UP2 and UP3, axiom L1 (as well as L3) follows from L2 and L4.
Instances of Taut include all formulas of the form f ∨ ¬f , where f is an arbitrary formula in L QU . We could replace Taut by a simple collection of axioms that characterize propositional reasoning (see, for example, (Mendelson, 1964)), but we have chosen to focus on aspects of reasoning about upper probability.
As in FHM, the axiom Ineq includes "all valid formulas about linear inequalities." An inequality formula is a formula of the form a 1 x 1 + · · · + a n x n ≥ c, over variables x 1 , . . . , x n . An inequality formula is said to valid if it is true under every possible assignment of real numbers to variables. To get an instance of Ineq, we replace each variable x i that occurs in a valid inequality formula by a primitive likelihood term of the form l(ϕ i ) (naturally each occurence of the variable x i must be replaced by the same primitive likelihood term l(ϕ i )). As with Taut, we can replace Ineq by a sound and complete axiomatization for Boolean combinations of linear inequalities. One such axiomatization is given in FHM.

Soundness and Completeness
A formula f is provable in an axiom system AX if f can be proven using the axioms and rules of inferences of AX. AX is sound with respect to a class M of structures if every formula provable in AX is valid in M (i.e., valid in every structure in M); AX is complete with respect to M if every formula valid in M is provable in AX.
Our goal is to prove that AX up is a sound and complete axiomatization for reasoning about upper probability (i.e., with respect to upper probability structures). The soundness of AX up is immediate from our earlier disscussion. Completeness is, as usual, harder. Unfortunately, the standard technique for proving completeness in modal logic, which involves considering maximal consistent sets and canonical structures (see, for example, (Popkorn, 1994)) does not work. We briefly review the approach, just to point out the difficulties.
The standard approach uses the following definitions. A formula σ is consistent with an axiom system AX if ¬σ is not provable from AX. A finite set of formulas {σ 1 , . . . , σ n } is consistent with AX if the formula σ 1 ∧ · · · ∧ σ n is consistent with AX; an infinite set of formulas is consistent with AX if all its finite subsets are consistent with AX. F is a maximal AX-consistent set if F is consistent with AX and no strict superset of F is consistent with AX. If AX includes Taut and MP, then it is not hard to show, using only propositional reasoning, that every AX-consistent set of formulas can be extended to a maximal AX-consistent set.
To show that AX is complete with respect to some class M of structures, we must show that every formula that is valid in M is provable in AX. To do this, it is sufficient to show that every AX-consistent formula is satisfiable in some structure in M. Typically, this is done by constructing what is called a canonical structure M c in M whose states are the maximal AX-consistent sets, and then showing that a formula σ is satisfied in a world w in M c iff σ is one of the formulas in the canonical set associated with world w.
Unfortunately, this approach cannot be used to prove completeness here. To see this, consider the set of formulas This set is clearly AX up -consistent according to our definition, since every finite subset is satisfiable in an upper probability structure and AX up is sound with respect to upper probability structures. It thus can be extended to a maximal AX up -consistent set F . However, the set F ′ of formulas is not satisfiable: it is not possible to assign l(ϕ) a value that will satisfy all the formulas at the same time. Hence, F is not satisfiable. Thus, the canonical model approach, at least applied naively, simply will not work. We take a different approach here, similar to the one taken in FHM. We do not try to construct a single canonical model. Of course, we still must show that if a formula f is AX up -consistent then it is satisfiable in an upper probability structure. We do this by an explicit construction, depending on f . We proceed as follows.
By a simple argument, we can easily reduce the problem to the case where f is a conjunction of basic likelihood formulas and negations of basic likelihood formulas. Let p 1 , . . . , p N be the primitive propositions that appear in f . Observe that there are 2 2 N inequivalent propositional formulas over p 1 , . . . , p N . The argument goes as follows. Let an atom over p 1 , . . . , p N be a formula of the form q 1 ∧ . . . ∧ q N , where q i is either p i or ¬p i . There are clearly 2 N atoms over p 1 , . . . , p N . Moreover, it is easy to see that any formula over p 1 , . . . , p N can be written in a unique way as a disjunction of atoms. There are 2 2 N such disjunctions, so the claim follows.
Thus, the formula f gives rise in a natural way to a system of inequalities of the form: We can express (1) as a conjunction of inequality formulas, by replacing each occurrence of l(ρ i ) in (1) by x i . Call this inequality formula f .
If f is satisfiable in some upper probability structure M , then we can take x i to be the upper probability of ρ i in M ; this gives a solution of f . However, f may have a solution without f being satisfiable. For example, if f is the formula l(p) = 1/2 ∧ l(¬p) = 0, then f has an obvious solution; f , however, is not satisfiable in an upper probability structure, because the upper probability of the set corresponding to p and the upper probability of the set corresponding to ¬p must sum to at least 1 in all upper probability structures. Thus, we must add further constraints to the solution to force it to act like an upper probability.
UP1-UP3 or, equivalently, the axioms L1-L4, describe exactly what additional constraints are needed. The constraint corresponding to L1 (or UP1) is just x 1 = 0, since we have assumed ρ 1 is the formula false. Similarly, the constraint corresponding to L2 is x 2 2 N = 1. The constraint corresponding to L3 is x i ≥ 0, for i = 1, . . . , 2 2 N . What about L4? This seems to require an infinite collection of constraints, just as UP3 does. 7 This is where UPF3 comes into play. It turns out that, if f is satisfiable at all, it is satisfiable in a structure with at most 2 N worlds, one for each atom over p 1 , . . . , p N . Thus, we need to add only instances of L4 where k, m, n < B 2 N and ϕ 1 , . . . , ϕ m , ϕ are all among ρ 1 , . . . , ρ 2 2 N . Although this is a large number of formulas (in fact, we do not know exactly how large, since it depends on B 2 N , which we have not computed), it suffices for our purposes that it is a finite number. For each of these instances of L4, there is an inequality of the form a 1 x 1 + · · · + a 2 2 N x 2 2 N ≥ k. Letf , the inequality formula corresponding to f , be the conjunction consisting of f , together with all the inequalities corresponding to the relevant instances of L4, and the equations and inequalities x 1 = 0, x 2 2 N = 1, and x i ≥ 0 for i = 1, . . . , 2 2 N , corresponding to axioms L1-L3.
Proposition 4.1: The formula f is satisfiable in an upper probability structure iff the inequality formulaf has a solution. Moreover, iff has a solution, then f is satisfiable in an upper probability structure with at most 2 |f | worlds.
Theorem 4.2: The axiom system AX up is sound and complete for upper probability structures.
Proof: For soundness, it is easy to see that every axiom is valid for upper probability structures, including L4, which represents UP3.
For completeness, we proceed as in the discussion above. Assume that formula f is not satisfiable in an upper probability structure; we must show that f is AX up -inconsistent.
We first reduce f to a canonical form. Let g 1 ∨ · · · ∨ g r be a disjunctive normal form expression for f (where each g i is a conjunction of basic likelihood formulas and their negations). Using propositional reasoning, we can show that f is provably equivalent to this disjunction. Since f is unsatisfiable, each g i must also be unsatisfiable. Thus, it is sufficient to show that any unsatisfiable conjunction of basic likelihood formulas and their negations is inconsistent. Assume that f is such a conjunction. Using propositional reasoning and axiom L5, f is equivalent to a likelihood formula f ′ that refers to 2 2 N propositional formulas, say ρ 1 , . . . , ρ 2 2 N . Since f is unsatisfiable, so is f ′ . By Proposition 4.1, the inequality formulâ f ′ corresponding to f ′ has no solution. Thus, by Ineq, the formula ¬f ′′ that results by replacing each instance of x i inf ′ by l(ρ i ) is AX up -provable. All the conjuncts of f ′′ that are instances of axioms L1-L4 are AX up -provable. It follows that ¬f ′ is AX up -provable, and hence so is ¬f .

Decision Procedure
Having settled the issue of the soundness and completeness of the axiom system AX up , we turn to the problem of the complexity of deciding satisfiability. Recall the problem of 7. Although we are dealing with only finitely many formulas here, ρ1, . . . , ρ 2 2 N , recall that the formulas ϕ1, . . . , ϕm in L4 need not be distinct, so there are potentially infinitely many instances of L4 to deal with.
satisfiability: given a likelihood formula f , we want to determine if there exists an upper probability structure M such that M |= f . As we now show, the satisfiability problem is NP-complete, and thus no harder than satisfiability for propositional logic.
For the decision problem to make sense, we need to restrict our language slightly. If we allow real numbers as coefficients in likelihood formulas, we have to carefully discuss the issue of representation of such numbers. To avoid these complications, we restrict our language (in this section) to allow only integer coefficients. Note that we can still express rational coefficients by the standard trick of "clearing the denominator". For example, we can express 2 3 l(ϕ) ≥ 1 by 2l(ϕ) ≥ 3 and l(ϕ) ≥ 2 3 by 3l(ϕ) ≥ 2. Recall that we defined |f | to be the length of f , that is, the number of symbols required to write f , where each coefficient is counted as one symbol. Define ||f || to be the length of the longest coefficient appearing in f , when written in binary. The size of a rational number a b , denoted || a b ||, where a and b are relatively prime, is defined to be ||a|| + ||b||.
A preliminary result required for the analysis of the decision procedure shows that if a formula is satisfied in some upper probability structure, then it is satisfied in a structure (Ω, Σ, P, π), which is "small" in terms of the number of states in Ω, the cardinality of the set P of probability measures, and the size of the coefficients in f .
Theorem 5.2: The problem of deciding whether a likelihood formula is satisfiable in an upper probability structure is NP-complete.
Proof: For the lower bound, it is clear that a given propositional formula ϕ is satisfiable iff the likelihood formula l(ϕ) > 0 is satisfiable, therefore the satisfiability problem is NP-hard. For the upper bound, given a likelihood formula f , we guess a "small" satisfying structure M = (Ω, Σ, P, π) for f of the form guaranteed to exist by Theorem 5.1. We can describe such a model M in size polynomial in |f | and ||f ||. (The fact that π(w)(p) = false for every world w ∈ Ω and every primitive proposition p not appearing in f means that we must describe π only for propositions that appear in f .) We verify that M |= f as follows. Let l(ψ) be an arbitrary likelihood term in f . We compute [[ψ]] M by checking the truth assignment of each s ∈ Ω and seeing whether this truth assignment makes ψ true. We then replace each occurence of l(ψ) in f by max µ∈P { s∈ [[ψ]] M µ(s)} and verify that the resulting expression is true.

Conclusion
We have considered a logic with the same syntax as the logic for reasoning about probability, inner measures, and belief presented in FHM, with uncertainty interpreted as the upper probability of a set of probability measures. Under this interpretation, we have provided a sound and complete axiomatization for the logic. We further showed that the satisfiability problem is NP-complete (as it is for reasoning about probability, inner measures, and beliefs), despite having to deal with probability structures with possibility infinitely many states and infinite sets of probability measures. The key step in the axiomatization involves finding a characterization of upper probability measures that can be captured in the logic. The key step in the complexity result involves showing that if a formula is satisfiable at all, it is satisfiable in a "small" structure, where the size of the state space, as well as the size of the set of probability measures and the size of all probabilities involved, are polynomial in the length of the formula.
Given the similarity in spirit of the results for the various interpretations of the uncertainty operator (as a probability, inner measure, belief function, and upper probability), including the fact that the complexity of the decision problem is NP-complete in all cases, we conjecture that there is some underlying result from which all these results should follow. It would be interesting to make that precise.
In FHM, conditional probabilities as well as probabilities are investigated. We have not, in this paper, discussed conditional upper probabilities. The main reason for this is that, unlike probability, we cannot characterize conditional upper probabilities in terms of (unconditional) upper probabilities. Thus, our results really tell us nothing about conditional upper probabilities. It might be of interest to consider a logic that allows conditional upper probabilities as primitive likelihood terms (that is, allows likelihood terms of the form l(ϕ | ψ)). While there is no intrinsic difficult giving semantics to such a language, it is far from clear what an appropriate axiomatization would be, or the effect of this extension on complexity.
Finally, it is worth noting that the semantic framework developed here and in FHM is in fact rich enough to talk about gambles (that is, real-valued functions over the set of states) and the expectation of such gambles. Expectation functions can be defined for the different measures of uncertainty, including upper probabilities, and it is not difficult to extend the FHM logic in order to reason about expectation. One advantage of working with expectation functions is that they are typically easier to characterize than the corresponding measures; for instance, the characterization of expected upper probabilities is much simpler than that of upper probabilities (Huber, 1981;Walley, 1981Walley, , 1991. However, getting a complete axiomatization is quite nontrivial. We refer the reader to (Halpern & Pucella, 2002) for more details on this subject. We remark that Wilson and Moral (1994) take as their starting point Walley's notion of lower and upper previsions. They consider when acceptance of one set of gambles implies acceptance of another gamble. Since acceptance involves expectation, it cannot be expressed in the logic considered in this paper; however, it can be expressed easiliy in the logic of (Halpern & Pucella, 2002).

Acknowledgments
A preliminary version of this paper appears in Uncertainty in Artificial Intelligence, Proceedings of the Seventeenth Conference, 2001. Thanks to Dexter Kozen, Jon Kleinberg, and Hubie Chen for discussions concerning set covers. Vicky Weissman read a draft of this paper and provided numerous helpful comments. We also thank the anonymous UAI and JAIR reviewers for their useful comments and suggestions. This work was supported in part by NSF under grants IRI-96-25901 and IIS-0090145, and ONR under grants N00014-00-1-03-41, N00014-01-10-511, and N00014-01-1-0795. The first author was also supported in part by a Guggenheim and a Fulbright Fellowship while on sabbatical leave; sabbatical support from CWI and the Hebrew University of Jerusalem is also gratefully acknowledged.
For the next implications, given A, B, let Z = A ∩ B.
Proof: We are given 0 < ǫ < 1 8 . It is easy to check mechanically that υ ǫ satisfies (6). We now show that there is no set P ′ such that υ ǫ = (P ′ ) * . By way of contradiction, assume there is such a P ′ . By the properties of sup, this means that there is a µ ∈ P ′ such that µ({a, b, c}) > 3 4 , since υ ǫ ({a, b, c}) = 3 4 + ǫ > 3 4 . Consider this µ in detail. Since µ ∈ P, we must have for all X ∈ Σ, X = {a, b, c}, that µ(X) ≤ (P ′ ) * (X) = P * (X). In particular, µ({a, b}), µ({b, c}), µ({a, c}) ≤ 1 2 . Therefore, However, from standard properties of probability, it follows that which contradicts (2). Therefore, µ, and therefore P ′ cannot exist, and υ ǫ is not an upper probability measure.  We need some terminology before proceeding. An exact (n, k)-cover of (A, Ω) is a cover C of A with the property that every element of A appears in exactly n + k sets in C, and every element of Ω − A appears in exactly k sets in C. Thus, while an (n, k)-cover of (A, Ω) can have many extra sets, as long as the sets cover A at least n + k times and Ω k times, an exact cover has only the necessary sets, with the right total number of elements. An exact (n, k)-cover C of (A, Ω) is decomposable if there exists an exact (n 1 , k 1 )-cover C 1 and an exact (n 2 , k 2 )-cover C 2 of (A, Ω) such that C 1 and C 2 form a nontrivial partition of C, with n = n 1 + n 2 and k = k 1 + k 2 . Intuitively, an exact cover C is decomposable if it can be split into two exact covers. It follows easily by induction that for any exact (n, k)cover, there exists a (not necessarily unique) finite set of nondecomposable exact covers C 1 , . . . , C m , with C i an exact (n i , k i )-cover, such that the C i 's a nontrivial partition of C with n = m i=1 n i and k = m i=1 . (If C is itself nondecomposable, we can take m = 1 and C 1 = C.) One can easily verify that if C is an exact (n, k)-cover of (A, Ω) and C ′ ⊆ C is an exact (n ′ , k ′ )-cover of (A, Ω) with n ′ + k ′ < n + k, then C is decomposable.
The following lemma highlights the most important property of exact covers from our perspective. It says that for any set A ∈ Σ, there cannot be a "large" nondecomposable exact cover of (A, Ω).
Proof: It is clearly sufficient to show that for any finite Ω we can find a B |Ω| with the required properties. Fix a Ω. Given A ⊆ Ω, we first show that there exists N A such that if n > N A or k > N A , every exact (n, k)-cover of (A, Ω) is decomposable. Suppose for the sake of contradiction that this is not the case. This means that we can find an infinite sequence C 1 , C 2 , . . . such that C i is a nondecomposable exact (n i , k i )-cover of (A, Ω), with either n 1 < n 2 < . . . or k 1 < k 2 < . . . . To derive a contradiction, we use the following lemma, known as Dickson's Lemma (Dickson, 1913).
Lemma A.2: Every infinite sequence of d-dimensional vectors over the natural numbers contains a monotonically nondecreasing subsequence in the pointwise ordering (where x ≤ y in the pointwise ordering iff x i ≤ y i for all i).
Proof: It is straightforward to prove by induction on k that if k ≤ d, then every infinite sequence of vectors x 1 , x 2 , . . . contains a subsequence x i 1 , x i 2 , . . . such that x i 1 j , x i 2 j , . . . is a nondecreasing sequence of natural numbers for all j ≤ k. The base case is immediate from the observation that every infinite sequence of natural numbers contains a nondecreasing subsequence. For the inductive step, observe that if x i 1 , x i 2 , . . . is a subsequence such that x i 1 j , x i 2 j , . . . is a nondecreasing sequence of natural numbers for all j ≤ k, then the sequence x i 1 k+1 , x i 2 k+1 , . . . of natural numbers must have a nondecreasing subsequence. This determines a subsequence of the original sequence with the appropriate property for all j ≤ k + 1.
Let S 1 , . . . , S 2 |Ω| be an arbitrary ordering of the 2 |Ω| subsets of Ω. We can associate with any cover C a 2 |Ω| -dimensional vector x C = (x C 1 , . . . , x C 2 |Ω| ), where x C i is the number of times the subset S i of Ω appears in the multiset C. The key property of this association is that if C ′ and C are multisets, then C ′ ⊆ C iff x C ′ ≤ x C in the pointwise ordering.
Consider the sequence of vectors x C 1 , x C 2 , . . . associated with the sequence C 1 , C 2 , . . . of nondecomposable exact covers of (A, Ω). By Lemma A.2, there is a nondecreasing subsequence of vectors, x C i 1 ≤ x C i 2 ≤ · · · . But this means that C i 1 ⊆ C i 2 ⊆ · · · . Since n 1 < n 2 < . . . or k 1 < k 2 < . . . , every cover in the chain must be distinct. But any pair of exact covers in the chain is such that C i ⊆ C i+1 , meaning C i+1 is decomposable, contradicting our assumption. Therefore, there must exist an N A such that any exact (n, k)-cover of A with n > N A or k > N A is decomposable. Now define B ′ |Ω| = max{N A : A ⊆ {1, . . . , |Ω|}}. It is easy to see that this choice works.
The first step is to show that, without loss of generality, C is an exact (n, k)-cover of (A, Ω). Let B i consist of those states s ∈ A i such that either s ∈ A and s appears in more than n + k sets in A 1 , . . . , A i−1 or s ∈ Ω − A and s appears in more than k sets in It is easy to check that C ′ is an exact (n, k)-cover of (A, Ω). For if s ∈ A, then s appears in exactly n + k sets in C ′ (it appears in A ′ j iff A j is among the first n + k sets in C in which s appeared) and, similarly, if s ∈ Ω − A, then s appears in exactly k sets in C ′ . Clearly if UP3 holds for C ′ , then it holds for C, since υ(A ′ i ) ≤ υ(A i ) for i = 1, . . . , m. Thus, we can assume without loss of generality that C is an exact (n, k)-cover of A.
We can also assume without loss of generality that no set in C is empty (otherwise, we can simply remove the empty sets in C; the resulting set is still an (n, k)-cover of (A, Ω)). There are now two cases to consider. If max(m, n, k) ≤ B |Ω| , the desired result follows from UPF3. If not, consider a decomposition of C into multisets C 1 , . . . , C p , where C h is an exact (n h , k h )-cover of (A, Ω) and is not further decomposable. We claim that max(|C h |, n h , k h ) ≤ B |Ω| for h = 1, . . . , p. If n h > B |Ω| or k h > B |Ω| , then it is immediate from Lemma A.1 that C h can be further decomposed, contradicting the fact that C h is not decomposable. And if |C h | > B |Ω| , then observe that X∈C h |X| ≥ |C h |.
Since |C h | > B |Ω| = 2|Ω|B ′ |Ω| , there must be some s ∈ Ω which appears in at least 2B ′ |Ω| sets in C h . Since C h is an exact (n h , k h )-cover, it follows that either n h > B ′ |Ω| or k h > B ′ |Ω| . But then, by Lemma A.1, C h is decomposable, again a contradiction. Now we can apply UPF3 to each of C 1 , . . . , C k to get Since the C h 's form a decomposition of C, we have By decomposition, n = p h=1 n h and k = p h=1 k h , and therefore m i=1 υ(A i ) − nυ(A) ≥ k, showing that UP3 holds, as desired.
Proposition 4.1: The formula f is satisfiable in an upper probability structure iff the inequality formulaf has a solution. Moreover, iff has a solution, then f is satisfiable in an upper probability structure with at most 2 |f | worlds.
Thus, x * is a solution to the inequality formulas corresponding to L4. Hence, x * is a solution tof .
For the converse, assume that x * is a solution tof . We construct an upper probability structure M = (S, E, P, π) such that M |= f as follows. Let p 1 , . . . , p N be the primitive propositions appearing in f . Let S = {δ 1 , . . . , δ 2 N } be the atoms over p 1 , . . . , p N . Let E be the set of all subsets of S. As observed earlier, every propositional formula over p 1 , . . . , p n is equivalent to a unique disjunction of atoms. Thus, we can get a canonical collection ρ 1 , . . . , ρ 2 2 N of inequivalent formulas over p 1 , . . . , p n by identifying each formula ρ i with a different element of E, where ρ 1 corresponds to the empty set and ρ 2 2 N corresponds to all of S. Define a set function υ by taking υ({δ i 1 , . . . , It is now sufficient to show that υ is an upper probability (of a set P of probability measures), since then it is clear that (S, E, P, π) |= f (since x * is a solution tof , the system of inequalities derived from formula f ). To do this, by Theorem 2.4, it suffices to verify UPF1, UPF2, and UPF3, using B 2 N in UPF3, since |S| = 2 N . UPF1: υ(∅) = x * 1 = 0. UPF2: υ(S) = x * 2 2 N = 1. UPF3: Suppose that A and A 1 , . . . , A m are in E and satisfy the premises of property UPF3, with k, m, n ≤ B 2 N . Let ρ i 1 , . . . , ρ im , ρ i m+1 be the canonical formulas corresponding to A 1 , . . . , A m , A, respectively. Clearly, A ⊆ J⊆{1,... ,m}, |J|=k+n j∈J A i j iff ρ i m+1 ⇒ J⊆{1,... ,m}, |J|=k+n j∈J ρ i j is a propositional tautology and similarly Ω ⊆ J⊆{1,... ,m}, |J|=k j∈J A i j iff J⊆{1,... ,m}, |J|=k j∈J ρ i j is a propositional tautology. Thus, m j=1 x i j − x i m+1 ≥ k is one of the inequality formulas inf . Thus, it follows that m j=1 x * i j − x * i m+1 ≥ k, as desired. By our definition of υ, we therefore have k + nυ(A) ≤ m i=1 υ(A i ), and so UPF3 holds.
Proof: The first step in the proof involves showing that if P is a set of probability measures defined on an algebra Σ of a finite space Ω, we can assume without loss of generality that for each set X ∈ Σ, there is a probability measure µ X ∈ P such that µ X (X) = P * (X) (rather than P * (X) just being the sup of µ(X) for µ ∈ P).
Lemma A.3: Let P be a set of probability measures defined on an algebra Σ over a finite set Ω. Then there exists a set P ′ of probability measures such that, for each X ∈ Σ, P * (X) = (P ′ ) * (X); moreover, there is a probability measure µ X ∈ P ′ such that µ X (X) = P * (X). In addition, for any interpretation π, if M = (Ω, Σ, P, π) and M = (Ω, Σ, P ′ , π), then for all likelihood formulas f , M |= f iff M ′ |= f .
Proof: Since Σ is finite, to show that P ′ exists, it clearly suffices to show that, for each X ∈ Σ, there is a probability measure µ X such that µ X (X) = P * (X) and, if P ′ = P ∪ {µ X }, then P * (Y ) = (P ′ ) * (Y ) for all Y ∈ Σ. Given X, if there exists µ ∈ P such that µ(X) = P * (X), then we are done. Otherwise, we construct a sequence µ 1 , µ 2 , . . . of probability measures in P such that lim i µ i (X) = P * (X) and, for all Y ∈ Σ, the sequence µ i (Y ) converges to some limit. Let X 1 , . . . , X n be an enumeration of the sets in Σ, with X 1 = X. We inductively construct a sequence of measures µ m1 , µ m2 , . . . in P for m ≤ n such that µ mi (X j ) converges to a limit for i ≤ k and lim i→∞ µ mi (X) = P * (X). For m = 1, we know there must be a sequence µ 11 , µ 12 , . . . of measures in P such that µ 1i (X) converges to P * (X). For the inductive step, if m < n, suppose we have constructed an appropriate sequence µ m1 , µ m2 , . . . . Consider the sequence of real numbers µ mi (X m+1 ). Using the Bolzano-Weierstrass theorem (Rudin, 1976) (which says that every sequence of real numbers has a convergent subsequence), this sequence has a convergent subsequence. Let µ (m+1)1 , µ (m+1)2 , . . . be the subsequence of µ m1 , µ m2 , . . . which generates this convergent subsequence. This sequence of probability measures clearly has all the required properties. This completes the inductive step.
The others cases are trivial.
Just as in FHM, to prove Theorem 5.1, we make use of the following lemma which can be derived from Cramer's rule (Shores, 1999) and simple estimates on the size of the determinant (see also (Chvátal, 1983) for a simpler variant): Lemma A.4: If a system of r linear equalities and/or inequalities with integer coefficients each of length at most l has a nonnegative solution, then it has a nonnegative solution with at most r entries positive, and where the size of each member of the solution is O(rl +r log(r)).
Continuing with the proof of Theorem 5.1, suppose that f is satisfiable in an upper probability structure. By Proposition 4.1, the systemf of equality formulas has a solution, so f is satisfied in a upper probability structure with a finite state space. Thus, by Lemma A.3, f is satisfied in a structure M = (Ω, Σ, P, π) such that for all X ∈ Σ, there exists µ X ∈ P such that µ X (X) = P * (X).
As in the completeness proof, we can write f in disjunctive normal form. Each disjunct g is a conjunction of at most |f | − 1 basic likelihood formulas and their negations. Since M |= f , there must be some disjunct g such that M |= g. Suppose that g is the conjunction of r basic likelihood formulas and s negations of basic likelihood formulas. Let p 1 , . . . , p N be the primitive formulas appearing in f . Let δ 1 , . . . , δ 2 N be the atoms over p 1 , . . . , p N . As in the proof of completeness, we derive a system of equalities and inequalities from g. It is a slightly more complicated system, however. Recall that each propositional formula over p 1 , . . . , p N is a disjunction of atoms. Let ϕ 1 , . . . , ϕ k be the propositional formulas that appear in g. Notice that k < |f | (since there are some symbols in f , such as the coefficients, that are not in the propositional formulas). The system of equations and inequalities we construct involve variables x ij , where i = 1, . . . , k and j = 1, . . . , 2 N . Intuitively, . Thus, the system includes k < |f | equations of the following form, for each pair i, i ′ such that i = i ′ . For each conjunct in g of the form θ 1 l(ϕ 1 ) + · · · + θ n l(ϕ k ) ≥ α, there is a corresponding inequality where, roughly speaking, we replace l(ϕ Negations of such formulas correspond to a negated inequality formula; as before, this is equivalent to a formula of the form Notice that there are at most |f | inequalities corresponding to the conjuncts of g. Thus, altogether, there are at most k(k − 1) + 2|f | < |f | 2 equations and inequalities in the system (since k < |f |). We know that the system has a nonnegative solution (taking ). It follows from Lemma A.4 that the system has a solution x * = (x * 11 , . . . , x * 12 N , . . . , x * k1 , . . . , x * k2 N ) with t ≤ |f | 2 entries positive, and with each entry of size O(|f | 2 ||f || + |f | 2 log(|f |)).
We use this solution to construct a small structure satisfying the formula f . Let I = {i : x * ij is positive, for some j}; suppose that I = {i 1 , . . . , i t ′ }, for some t ′ ≤ t. Let M = (S, E, P, π) where S has t ′ states, say s 1 , . . . , s t ′ , and E consists of all subsets of S. Let π(s h ) be the truth assignment corresponding to the formula δ i h , that is, π(s h )(p) = true if and only if δ i h ⇒ p (and where π(s h )(p) = false if p does not appear in f ). Define where, by construction, the size of x * i h j is O(|f | 2 ||f || + |f | 2 log(|f |)), the theorem follows.
8. For simplicity here, we are implicitly assuming that each of the formulas ϕi appears in each conjunct of g. This is without loss of generality, since if ϕi does not appear, we can put it in, taking θi = 0.

Appendix B. Proof of the Characterization of Upper Probabilities
To make this paper self-contained, in this appendix we give a proof of Theorem 2.3. The proof we give is essentially that of Anger and Lembcke (1985). Walley (1991) gives an alternate proof along somewhat similar lines. Note that the functionalg we define in our proof corresponds to the construction in Walley's Natural Extension Theorem, which is needed in his version of this result. , so k + nP * (A) ≤ m j=1 P * (A j ), as required. As for the "only if" direction, we first prove a general lemma relating the problem to the Hahn-Banach Theorem. Some general definitions are needed. Suppose that we are given a space W and an algebra F of subsets of W . Let K be the vector space generated by the indicator functions 1 X defined by for X ∈ F. A sublinear functional on K is a mapping c : K → R such that c(αh) = αc(h) for α ≥ 0 and c(h 1 + h 2 ) ≤ c(h 1 ) + c(h 2 ) for all h 1 , h 2 . A sublinear functional is increasing if h ≥ 0 implies c(h + h ′ ) ≥ c(h ′ ) for all h ′ ∈ K. The following result is a formulation of the well-known Hahn-Banach Theorem (see, for example, (Conway, 1990)).
Theorem (Hahn-Banach): Let K be a vector space over R, and let g be a sublinear functional on K. If M is a linear subspace in K and λ : M → R is a linear functional such that λ(x) ≤ g(x) for all x in M, then there is a linear functional λ ′ : K → R such that λ ′ | M = λ and λ ′ (x) ≤ g(x) for all x in K.
Lemma B.1: Let g : F → [0, 1] be such that g(W ) = 1 and suppose that there is an increasing sublinear functionalg on K such that 1.g(1 K ) = g(K) for K ∈ F;
Then g is an upper probability measure.
The main result follows by showing how to construct, from a function υ satisfying the properties of Theorem 2.3, a sublinear functional c on K with the required properties.
Suppose that g : Σ → R is a function satisfying UP1-UP3. As we show in the discussion after Theorem 2.3 in the text, UP1-UP3 show that the range of g is in fact [0, 1]. Since g satisfies UP3, if {{K 1 , . . . , K m }} is an (n, k)-cover of (K, Ω), we have k +ng(K) ≤ m i=1 K i . This is equivalent to saying that k + n1 K ≤ m i=1 1 K i . Hence, for all K 1 , . . . , K m such that This observation motivates the following definition of the functionalg : K → R ∪ {−∞, ∞}: g(K i ) : m, n, k ∈ N, m, n > 0, K 1 , . . . , K m ∈ F, − k n Our goal now is to show thatg satisfies the conditions of Lemma B.1.
• It is immediate from the definition ofg thatg(1 K ) ≤ g(K) for K ∈ F; the fact that g(1 K ) = g(K) now follows from (3).
Since the conditions of Lemma B.1 are satisfied, g is an upper probability measure.