The Complexity of Limited Belief Reasoning—The Quantifier-Free Case

1 Introduction

The standard way of modeling knowledge and belief 1 in epistemic logic is in terms of possible worlds: an agent knows a proposition if and only if it is true in all worlds the agent considers possible. A side-effect of this model is that agents are assumed to be logically omniscient, that is, they know all the consequences of what they know [Hintikka, 1975].

Unfortunately, the assumption of logical omniscience is inappropriate for most resource-bounded agents like humans or robots: it drives up the computational cost of reasoning and is usually far beyond the their capabilities. Theories of limited belief therefore aim to lift the omniscience assumption.

A number of theories of limited belief have been proposed, predominantly in the 1980s and 1990s [Konolige, 1986; Kaplan and Schubert, 2000; Vardi, 1986; Fagin and Halpern, 1987; Levesque, 1984; Patel-Schneider, 1990; Lakemeyer, 1994; Delgrande, 1995]. A common problem with these approaches is, however, that either their model of limiting belief is too fine-grained or it misses out on simple inferences.

A novel approach to limited belief developed over a series of papers [Liu et al., 2004; Lakemeyer and Levesque, 2013; 2014; Klassen et al., 2015; Schwering and Lakemeyer, 2016;

1 We use the terms knowledge and belief interchangeably.

Lakemeyer and Levesque, 2016; Schwering, 2017] attempts to address this issue. The basic idea is to stratify beliefs into belief levels, where the first one, level 0, only comprises the explicit beliefs, that is, what is written down expressly in the knowledge base, and higher belief levels k+1 draw additional conclusions based on what is believed at level k. Semantically the logic can be characterized using sets of clauses instead of possible worlds, and through case splits, that is, by branching on all the values some term can take and propagating the value.

As an example, consider the following knowledge base:

fatherOf(Sally) = Frank ∨ fatherOf(Sally) = Fred

fatherOf(Sally) = n ⊃ rich(n) = ⊤ for n ∈ {Frank, Fred}.

Here, Sally, Frank, Fred, ⊤ name distinct individuals (⊤ is an auxiliary name for modeling propositions), whereas fatherOf and rich represent functions in the classical sense. From this knowledge we can deduce rich(Frank) = ⊤ ∨ rich(Fred) = ⊤ at level 1 by splitting on all potential fathers of Sally: if Frank is the father, then Frank is rich; if Fred is the father, then he is rich; every other potential father contradicts the first clause.

Logics of limited belief in general and the belief level mechanism in particular aim to provide means of controlling the reasoning effort in a comprehensible and explainable way, as contrasted with using a classical reasoner and terminating it after a timeout, for example. The rationale behind the belief level approach is that reasoning at small belief levels should be relatively cheap but still sufficient for the average problem a human or a robot faces during their daily operation. Experiments confirm this hypothesis for the confined domains of Sudoku and Minesweeper [Schwering, 2017].

Contribution

In this paper, we analyze reasoning with belief levels from the perspective of complexity theory. More precisely, we study the problem of deciding whether a knowledge base entails a query at a certain belief level.

For a constant belief level, the problem is indeed in PTIME and hence known to be tractable; the same holds when the knowledge base and query only mention a constant number of function terms.

However, we shall see that if both the belief level and the number of function terms are part of the problem input, then the complexity jumps to PSPACE-complete! This may come as a surprise given that classical, unlimited reasoning is in coNP. So (large) belief levels appear to make reasoning harder.

Intuitively, the jump is caused by the belief level limiting a possibly scarce resource, namely the number of case splits, which needs to be utilized in an optimal way.

The gap between PTIME and PSPACE-completeness calls for a more refined analysis, which we carry out using parameterized complexity theory. We investigate three dimensions of parameters: (1) the belief level, (2) the number of function terms mentioned in the reasoning problem (in the above example, the function terms are fatherOf(Sally), rich(Frank), rich(Fred)), and (3) the number of mentioned so-called standard names (in the example, these names are Sally, Frank, Fred, ⊤). Parameterized complexity theory offers the W- and A-hierarchies to classify problems between PTIME and NP and between NP and PSPACE, respectively. We locate the parameterized variants of our problem within these hierarchies.

A comprehensive overview of the paper's findings is given in Table 1. Figure 1 illustrates the relationships between the complexity classes we deal with in this paper.

The paper is structured as follows. The next section introduces the logic of limited belief and defines the reasoning problem that we shall study. Section 3 introduces a gadget that we use in several reductions. Section 4 begins the complexity analysis from the perspective of classical complexity theory with PTIME and PSPACE results. Section 5 refines the picture using parameterized complexity theory. Then we conclude.

Full proofs of our results can be found in [Chen et al., 2018].

2 The Logic of Limited Belief

In its most recent form, the logic of limited belief is a firstorder logic with functions, equality, and epistemic modal operators [Lakemeyer and Levesque, 2016; Schwering, 2017]. In this paper, we limit our consideration to the quantifier-free case.

This section first introduces the syntax and semantics of this logic, and then defines the reasoning problem whose complexity we will study in the remainder of the paper: if we know KB explicitly, do we believe α at level k? The definitions and results of this section are adopted from [Schwering, 2017] with some minor simplifications to ease the technical treatment; these simplifications do not affect the expressivity or complexity of the reasoning task at hand.

2.1 The Language

A term is either a standard name (or name for short) or a function term f(n1, . . . , nj), where f is a function symbol and every ni is a standard name. Standard names can be understood as special constants that satisfy the unique-names assumption and an infinitary version of domain closure. We assume an infinite supply of standard names as well as of function symbols.

A literal is an expression of the form t=n or ¬t=n, where t is a function term and n is a standard name. A formula is a literal or an expression of the form ¬α, (α∨β), or Bkα, where α, β are formulas and k ≥ 0 is a natural number. We read Bkα as "α is known at belief level k;" in case k = 0 we also say "α is known explicitly." We use the usual abbreviations t ̸= n, (α ∧ β), (α ⊃ β), and may omit brackets to ease readability.

A formula without Bk is called objective. Schwering [2017] has shown that there is a linear Turing reduction from the reasoning problem with nested beliefs to the non-nested case. Hence to simplify the presentation we henceforth assume that α in Bkα is objective. As usual, a conjunction of disjunctions of literals is said to be in conjunctive normal form (CNF).

2.2 The Semantics

The semantics of limited belief is based on clause subsumption, unit propagation, and case splits. A clause is a set of literals. We abuse notation and identify a non-empty clause {ℓ1, . . . , ℓj} with the formula (ℓ1 ∨ . . . ∨ ℓj). In the rest of this paragraph, we implicitly assume that n, n′ refer to distinct standard names. A clause c1 subsumes another clause c2 iff for every t =n ∈ c1, either t =n ∈ c2 or t ̸=n′ ∈ c2, and for every t̸=n ∈ c1, also t̸=n ∈ c2. We say two literals ℓ1, ℓ2 are complementary when they are of the form t = n and t ̸= n or of the form t = n and t = n′ . The unit propagation of a clause c and a literal ℓ is obtained by removing from c all literals complementary to ℓ. For a set of clauses s, we let UP(s) be the closure of s under unit propagation and subsumption.

The truth relation |≈ is defined between a formula α and a set of clauses s. Intuitively, s acts as a partial model. At belief level 0, α is broken down to clause level and then checked for subsumption by UP(s). Higher belief levels allow to branch on a function term t and all its values n and add t = n to s, which may then trigger unit propagation in UP(s) and thus produce new inferences. The formal definition is as follows:

1. if c is a clause: s |≈ c iff c ∈ UP(s)
2. if (α∨β) is not a clause: s |≈ (α∨β) iff s |≈ α or s |≈ β
3. s |≈ ¬(α∨ β) iff s |≈ ¬α and s |≈ ¬β
4. s |≈ ¬¬α iff s |≈ α
5. s |≈ B0α iff s |≈ α
6. s |≈ Bk+1α iff for some function term t, for all names n,

In the remainder, we refer to these definitions as Rules 1-7. As usual, a formula α is valid, written |≈ α, iff s |≈ α for every set of clauses s.

The belief level k in Bkα specifies the number of case splits, which corresponds to the maximum permitted reasoning effort for proving α. Limited belief is monotonic in the belief level:

Moreover, belief stabilizes at a high-enough belief level in the following sense:

Lemma 2 Let F contain all function terms in s and α, and let k ≥ |F|. Then s |≈ Bkα iff s |≈ B|F|α.

Example

Let us revisit the example from the introduction to illustrate how the semantics works. Let s contain the clauses

fatherOf(Sally) = Frank ∨ fatherOf(Sally) = Fred

fatherOf(Sally) ̸= Frank ∨ rich(Frank) = ⊤ fatherOf(Sally) ̸= Fred ∨ rich(Fred) = ⊤

and let c denote the clause rich(Frank) =⊤∨ rich(Fred) =⊤. Then s |≈ B1c holds by splitting the cases for Sally's father:

• UP(s ∪ {fatherOf(Sally) = Frank}) ∋ rich(Frank) = ⊤ by unit propagation with the second clause.
• UP(s ∪ {fatherOf(Sally) = Fred}) ∋ rich(Fred) = ⊤ by unit propagation with the third clause.
• UP(s ∪ {fatherOf(Sally) = n}) for n /∈ {Frank, Fred} contains the empty clause by unit propagation with the first clause.

In each case, we obtain a clause that subsumes c, so for every potential father n, c ∈ UP(s ∪ {fatherOf(Sally) = n}).

Classical Semantics

For future reference, we briefly give the classical, "unlimited" semantics of objective formulas. A world w is a function from function terms to standard names. Truth of an objective formula α in a world w, written w |= α, is defined as follows:

• w |= t =n iff w(t) = n
• w |= (α∨ β) iff w |= α or w |= β

· w |= ¬α iff w ̸|= α

We write s |= α to say that for all w, if w |= c for all c ∈ s, then w |= α. Moreover, we write |= α for ∅ |= α.

Limited belief is sound as well as eventually complete with respect to classical semantics in the following sense:

Proposition 3 For all finite s and all α, there is a (largeenough) belief level k ≥ 0 such that s |≈ Bkα iff s |= α.

Proof sketch. Soundness holds because Rule 6 branches over all names. Eventual completeness holds because k can be chosen large enough to split all terms in s, α.

2.3 The Limited Belief Reasoning Problem

The fundamental problem of reasoning about limited belief is to decide whether for a given knowledge base KB and a query α, if KB is known explicitly, then α is known at belief level k. In limited belief, KB is typically assumed to be CNF [Lakemeyer and Levesque, 2016]. The formal definition is:

Limited Belief Reasoning

Instance: Objective formulas KB and α over function terms F and standard names N , KB in CNF, belief level k ≥ 0.

Problem: Decide whether |≈ B0KB ⊃ Bkα.

We shall investigate this problem using classical complexity theory first and then refine the picture using parameterized complexity theory for parameters k, |F|, |N|. An overview of the results is in Table 1.

Since the knowledge base in Limited Belief Reasoning is assumed to be in CNF, it corresponds to a unique (modulo UP) set of clauses and the problem can be equivalently expressed as a model checking problem:

Lemma 4 Let KB be in CNF with clauses s = {c1, . . . , cj}. Then |≈ B0KB ⊃ Bkα iff s |≈ Bkα.

Thus and by Lemma 2 and Proposition 3, Limited Belief Reasoning is sound and eventually complete with respect to classical reasoning: |≈ B0KB ⊃B|F|α iff |= KB ⊃ α.

Finally, the following lemma says that in Rule 6 a finite number of function terms and standard names is sufficient.

Lemma 5 Let F (resp. N) contain all function terms (resp. standard names) in s, α, and let ˆn /∈ N be an additional name. Then s |≈ Bk+1α iff for some t ∈ F, for all n ∈ N ∪ {ˆn}, s ∪ {t = n} |≈ Bkα.

Together, Lemmas 4 and 5 give rise to a decision procedure for Limited Belief Reasoning, which works as follows. First, the problem is turned into the equivalent model checking problem using Lemma 4. Then the procedure applies Lemma 5 to reduce the belief level, and finally follows Rules 1-5 to break α down to clause level and check the clauses for subsumption. It is already known that this procedure runs in time O(2k (|KB| + |α|)k+3 ) [Schwering, 2017].

3 Ordering Gadget

It is easy to see that the ordering in which terms are split can be relevant. For example, let s contain the following four clauses:

f =n ∨ g1 =n ∨ h=n f ̸=n ∨ g2 =n ∨ h=n f =n ∨ g1 ̸=n ∨ h=n f ̸=n ∨ g2 ̸=n ∨ h=n

We can prove s |≈ B2h = n by splitting f first and then, depending on the value of f, splitting g1 or g2 next, but not the other way around.

In this section we construct a gadget that generalizes this idea in order to enforce that a goal formula can only be proved by splitting terms in a certain order (at polynomial cost in space). This gadget is used repeatedly in the proofs of Sections 4 and 5. For example, in Theorem 9 we use it to preserve the quantifier ordering of the quantified Boolean formula.

To begin with, the following lemma shows how to make sure that one of the terms from a set F is split no later than at belief level k. We use the notation [k] for {1, . . . , k}.

Lemma 6 Let F be a non-empty finite set of function terms, and L be a set of literals where every term from F occurs exactly once. Let Bkα be a formula with k ≥ 1. Let s be a set of clauses such that for all t /∈ F, for some name n, s ∪ {t = n} ̸|= ∨ℓ∈L ℓ and s ∪ {t = n} ̸|= ∨ℓ∈L ¬ℓ.

Let ℓwi , ℓoj for i ∈ [k - 1], j ∈ [k] be literals with distinct function terms f w i , f o j that do not occur in s or α. Let cok stand for ℓo1 ∨ . . . ∨ ℓok . Let sk be the least set that includes s and for every ℓ ∈ L contains the clauses

• ¬ℓ ∨ cok
• ℓ ∨ ℓw1 ∨ . . . ∨ ℓwk-1 ∨ cok
• ℓ ∨¬ℓw1 ∨ cok , . . . , ℓ ∨¬ℓwk-1 ∨ cok .

Proof. The proof proceeds in four steps.

Proof of Claim 1. By assumption, no two literals in L are complementary. Hence the only way of proving cok is by splitting some t ∈ F and f w 1 , . . . , f w k-1 , which requires belief level k. The proof is by induction on k.

Proof of Claim 2. By assumption, there is some n such that s∪{t=n} ̸|= ∨ℓ∈L(¬)ℓ for all ℓ ∈ L. Hence and since f w i , f o j do not occur in s, sk∪{t=n} ̸|≈ Bk-1cok iff sk\s ̸|≈ Bk-1cok , which holds by Claim 1.

Claim 3. For all t ∈ F, for all n, sk ∪ {t =n} |≈ Bk-1cok . Proof of Claim 3. Let t ∈ F and let n be an arbitrary name. Then for all names n1, . . . , nk, cok ∈ UP(sk ∪ {t = n, f w 1 = n1, . . . , f w k-1 = nk-1}). Thus sk ∪ {t = n} |≈ Bk-1 cok .

Proof of the lemma. For the only-if direction, by Claim 2, sk ∪ {t = n} |≈ Bk-1(cok ∧ (∨ℓ∈L ¬ℓ ∨ α)) for all n for some t ∈ F ∪ {f w 1 , . . . , f w k-1 , f o 1 , . . . , f o k }. By Claim 3 and since f w i , f o j do not occur in s or α, we can assume t ∈ F .

For the converse direction, if n is such that t =n is complementary to ¬ℓ for some ℓ ∈ L, then cok ∈ UP(sk ∪ {t = n}). Otherwise, t=n subsumes ¬ℓ for some ℓ ∈ L and by Claim 3, the remaining splits suffice to prove cok .

The next lemma represents our gadget. Despite its somewhat intimidating interface, it simply plugs together repeated applications of the previous lemma to completely determine the ordering of splitting terms from F1, . . . , Fl:

Lemma 7 Let F1, . . . , Fl be non-empty finite sets of function terms, F = F1∪. . .∪Fl, and L1, . . . , Ll be sets of literals such that every term from Fi occurs exactly once in Li. Let Bkα be a formula with k ≤ l. Let s be a set of clauses such that for all k ∈ [l], for all tl ∈ Fl, . . . , tk+1 ∈ Fk+1, tk /∈ F, for all nl, . . . , nk+1, nk, s ∪ {tk = nk, . . . , tl = nl} ̸|= ∨ℓ∈Lk ℓ.

For every set of clauses s′ , let s′i and coi be as in Lemma 6 with respect to Fi,Li, α. Let α0 be α and αi for i > 0 be coi ∧ (∨ℓ∈Li ¬ℓ ∨ αi-1).

Then

Proof. By induction on k, where Lemma 6 can be applied since s′ ̸|= ∨ℓ∈Li (¬)ℓ implies ((s′1 ) . . .)j ̸|= ∨ℓ∈Li (¬)ℓ.

4 Classical Complexity

This section analyzes the complexity of Limited Belief Reasoning using classical complexity theory. The next tractability result follows from the decision procedure from Section 2.3:

Corollary 8 Limited Belief Reasoning with constant k or constant |F| is in PTIME.

Proof. The decision procedure runs in time polynomial with degree k + 3. By Lemmas 1 and 2, k = |F| suffices.

Next, we consider the case where neither k nor |F| is constant. It comes as no surprise that the complexity then significantly increases with the number of case splits. Proposition 3 and Lemma 4 showed that Limited Belief Reasoning is sound and eventually complete with respect to classical reasoning. So clearly, Limited Belief Reasoning must be co-NP-hard, and eventual completeness may suggest that it is co-NP-complete as well. However, limiting the number of case splits further adds to the computational complexity: whereas in classical reasoning a decision procedure may "simply" split all function terms, a decision procedure for limited belief needs to make sure it makes use of the available case splits in the best possible way. This leads to the following result:

Theorem 9 Limited Belief Reasoning with constant |N| is PSPACE-complete. The result also holds when |N| is input.

Proof. Membership. The decision procedure from Section 2.3 runs in space O(m + k) where m = |KB| + |α|, since UP(s) can be represented in space O(|s|) because minimal clauses suffice.

Hardness. We reduce from True Quantified Boolean Formula, which is PSPACE-complete [Arora and Barak, 2009]. The problem input is a fully quantified Boolean formula Qkxk . . . Q1x1ψ for Qi ∈ {∀, ∃} and a propositional formula ψ. Without loss of generality, we assume that ψ mentions negation only in front of variables. The question is whether this formula evaluates to TRUE, that is, for all (if Qk = ∀) / some (if Qk = ∃) assignment(s) of xk, . . . , for all / some assignment(s) of x1, (x1, . . . , xk) satisfies ψ.

Let N = {⊤,W} contain two standard names. Let F∀ = {fi | Qi = ∀}, F∃ = {fi, f ′ i | Qi = ∃}, F = F∀ ∪ F∃, where fi, f ′ i are pairwise distinct function terms. We define a mapping ∗ from QBF to limited belief formulas: let x∗i be fi = ⊤, let (¬xi)∗ be fi ̸= ⊤ if Qi = ∀ and f ′ i = ⊤ if Qi = ∃, let (ψ1 ∨ ψ2)∗ be (ψ∗ 1 ∨ ψ∗ 2 ), and let (ψ1 ∧ ψ2)∗ be (ψ∗ 1 ∧ ψ∗ 2 ). For Qi = ∀, let Fi = {fi}, Ni = {n | name n is distinct fromW}, and Li = {fi ̸=W}; for Qi = ∃, let Fi = {fi, f ′ i }, Ni = {⊤}, and Li = {fi = ⊤, f ′ i =⊤}.

The idea is as follows. Universally quantified xi are naturally translated to literals fi =⊤ so that the truth values TRUE and FALSE of xi correspond to fi =⊤ and fi ̸=⊤, respectively. For existentially quantified xi, positive occurrences of xi are replaced with fi = ⊤ and negative ones with f ′ i =⊤ so that the truth values TRUE and FALSE of xi correspond to fi =⊤ and f ′ i =⊤. The fi or f ′ i (if Qi = ∃) then need to be split in the appropriate order.

We can show by induction on k and subinduction on ψ that φ evaluates to TRUE iff for some tk ∈ Fk, for all nk ∈ Nk, . . . , for some t1 ∈ F1, for all n1 ∈ N1, {t1 =n1, . . . , tk =nk} |≈ ψ∗ . The theorem then follows because the restriction ni ∈ Ni on the right-hand side can be lifted by replacing ψ∗ with ∨ℓ∈Li,i∈[k] ¬ℓ ∨ ψ∗ , which then reduces in polynomial time to Limited Belief Reasoning by Lemmas 7 and 4.

It is noteworthy that this reduction only uses two standard names. With a more involved reduction, even a single name suffices. Thus even the propositional case (where an atomic proposition p is simulated by p = ⊤) is PSPACE-complete.

5 Parameterized Complexity

The gap between tractability and PSPACE-completeness from the previous section calls for a more refined analysis. In this section we use parameterized complexity theory to investigate how the parameters k, |F|, and/or |N| affect the complexity of Limited Belief Reasoning.

While many unparameterized problems can be classified with the classical classes PTIME, NP, or PSPACE, parameterized versions of these problems fall into a variety of complexity classes [Flum and Grohe, 2006]. The role of PTIME in parameterized complexity is taken on by FPT, which includes problems parameterized by k that are solvable in f(k) · p(n), where f is a computable function and p a polynomial. Other important parameterized classes come from the W- and A-hierarchies: the classes W[1] ⊆ W[2] ⊆ . . . ⊆ W[SAT] ⊆ W[P] include parameterized versions of different natural NP-complete problems; similarly, the classes A[1] ⊆ A[2] ⊆ . . . ⊆ AW[SAT] ⊆ AW[P] can be seen as a parameterized version of the polynomial hierarchy. This analogy is a simplification-links between PSPACE and W[1] have recently been exhibited [Bonnet et al., 2017]-but it suffices for our purpose and we display an intuitive representation of the relationships between these classes in Figure 1.

Membership in classes of the W- and A-hierarchies can be shown using machines that restrict the number of nondeterministic steps [Chen et al., 2005]. An NRAM is a random access machine with a nondeterministic EXISTS instruction which guesses a natural number less than or equal to a certain register and stores the number in that register. A problem is in W[P] iff it is decidable by an NRAM in f(k) · p(n) steps, at most g(k) of them being nondeterministic, using at most the first f(k) · p(n) registers and only numbers ≤ f(k) · p(n). A problem is in AW[P] iff it is decidable by an ARAMwith the same constraints, where an ARAM is an NRAM with an additional nondeterministic FORALL instruction, the dual to EXISTS. Hardness in parameterized complexity is shown by way of fpt-reductions, which are reductions computable in time f(k) · p(n) and such that k′ ≤ g(k), where k and k′ are the parameters of the problems reduced from and reduced to, respectively, n is the input size, f and g are computable functions, and p is a polynomial.

Before starting our analysis, we introduce the Quantified Monotone Circuit Satisfiability problem. A circuit is a directed acyclic graph (V, E) whose vertices are partitioned into inputnodes X of in-degree 0, not-nodes of in-degree 1, and- and or-nodes of in-degree > 0, and a distinguished output-node v0 of out-degree 0. An assignment S ⊆ X sets inputs S to TRUE and the other ones to FALSE and propagates the values to the output node, whose value then determines whether or not S satisfies the circuit. A monotone circuit contains no not-nodes.

Quantified Monotone Circuit Satisfiability

Instance: A monotone circuit C with input-nodes partitioned into sets X1, . . . ,Xl.

Parameter: k1 + . . . + kl

Problem: Decide whether for all S1 ⊆ X1 with |S1| = k1, for some S2 ⊆ X2 with |S2| = k2, . . . , the assignment S1 ∪ . . . ∪ Sl satisfies C.

The following lemma states AW[P]-completeness for the problem, which has been claimed elsewhere before without explicit proof [Abrahamson et al., 1995].

Lemma 10 Quantified Monotone Circuit Satisfiability is AW[P]-complete.

Proof. It is sufficient to reduce from Quantified Circuit Satisfiability, which is AW[P]-complete [Flum and Grohe, 2006]. Consider an instance with circuit C = (V,E) and inputs X1, . . . ,Xl. By De Morgan's laws we can assume the notnodes are right above the inputs. Observe that a not-node w ∈ V with input x ∈ Xi is TRUE iff at least ki variables in Xi \ {x} are set to TRUE. The latter property can be expressed in a monotone circuit of polynomial size using or-nodes vi1,i2,t that represent that at least t of xi1 , . . . , xi2 are set to TRUE, and nodes conjoining pairs of these nodes to express that t′ of xi1 , . . . , xi′ and t - t′ of xi′+1, . . . , xi2 are set to TRUE.

With this lemma we can establish the complexity of Limited Belief Reasoning parameterized by the belief level:

Theorem 11 Limited Belief Reasoning with parameter k is AW[P]-complete.

Proof. Membership. We implement the decision procedure from Section 2.3 using an ARAM. Model checking at belief level 0 can clearly be done on a RAM in time p(m), where p is a polynomial and m = |KB| + |α|. At belief level k > 0 we select one of the function terms from F with EXISTS, and the corresponding name from N ∪ {ˆn} with FORALL. This amounts to 2 · k nondeterministic steps and a total runtime 2 · k · p(m), so the problem is in AW[P].

Hardness. We reduce from Quantified Monotone Circuit Satisfiability, which is AW[P]-complete by Lemma 10. Let C=(V, E) be a monotone circuit with inputs X1, . . . , Xl. We say Xi or x ∈ Xi is universal (existential) iff i is odd (even). Let F = {fv | v ∈ V } ∪ {fi,j | Xi universal, j ∈ [ki]} ∪ {fx,j | x ∈ Xi existential, j ∈ [ki]} be function terms. Let

N = {⊤,W} ∪ {nx | x ∈ Xi universal} be standard names. The idea is to represent that a node v is set to TRUE by fv = ⊤. The truth assignment is selected by splitting fi,1 , . . . , fi,ki one after another for universal Xi, and by splitting some ki of {fx,j | x ∈ Xi, j ∈ [ki]} for existential Xi. Truth of a universal input x ∈ Xi is represented by fi,j =nx for some j ∈ [ki], and truth of an existential input x ∈ Xi is represented by fx,j =⊤ for some j ∈ [ki], both of which trigger fx =⊤; these values are then propagated to the output node, so that fv0 =⊤ indicates that the circuit is satisfied.

This is encoded in a set of clauses s in the following way. For universal Xi let si be the least set that for all j ∈ [ki] and x ∈ Xi contains fi,j ̸= nx ∨ fx = ⊤, and ∨x∈Xi fi,j = nx ∨ fi,j =W. For existential let si be the least set that for all j ∈ [ki] and x ∈ Xi contains fx,j ̸=⊤ ∨ fx =⊤. Now let s be the least set such that s ⊇ si for all i ∈ [l], and that contains ∨w∈W fw ̸= ⊤ ∨ fv = ⊤ for every and-node v and its inputs W = {w | (w, v) ∈ E}, and fw ̸= ⊤ ∨ fv = ⊤ for all or-nodes v and all inputs w with (w, v) ∈ E.

It is then straightforward to show by induction on l and subinduction on the depth of C that for all S1 ⊆ X1 with |S1| ≤ k1, for some S2 ⊆ X2 with |S2| ≤ k2, . . . , the truth assignment S1 ∪ . . . ∪ Sl satisfies C iff for some t1,1 ∈ F1,1, for all n1,1 ∈ N1,1, . . . , for some tl,kl ∈ Fl,kl , for all nl,kl ∈ Nl,kl , s ∪ {t1,1 = n1,1, . . . , tl,kl = nl,kl } |≈ fv0 = ⊤, where Fi,j = {fi,j } and Ni,j = {nx | x ∈ Xi} for universal Xi, and Fi,j = {fx,j | x ∈ Xi} and Ni,j = {⊤} for existential Xi. The right-hand side can be rewritten to match Lemma 7 for Li,j = {fi,j ̸=W} for universal Xi and Li,j = {fx,j =⊤ | x ∈ Xi} for existential Xi, and thus fpt-reduces to Limited Belief Reasoning by Lemmas 7 and 4, which gives us AW[P]- hardness.

Membership in AW[P] is quite natural due to the alternation of existential and universal quantifications of case splits in Lemma 5. When the number of standard names |N| becomes a parameter as well, this gives us leverage to replace the nondeterministic FORALL steps that select the standard names with a simple loops. It is therefore not surprising that Limited Belief Reasoning parameterized by k and |N| is in W[P], the hardest NP-analogue of the W-hierarchy. The following result shows that the problem is in fact W[P]-complete:

Proposition 12 Limited Belief Reasoning with parameters k and |N| is W[P]-complete. The result also holds when |N| is constant.

Proof. Membership. We build an NRAM. For k = 0, it behaves like the ARAM in Theorem 11. For k > 0, we select a function term from F with EXISTS and loop over all names in N ∪ {ˆn}. This requires (|N| + k)k nondeterministic steps.

Hardness. We reduce fromWeighted Monotone Circuit Satisfiability, which is W[P]-complete [Abrahamson et al., 1995] and identical to the quantified problem with only a single block of existential variables, and the proof accordingly carries over from Theorem 11.

Next we consider the case where |F| becomes a parameter. The below theorem specifies co-W[P]-completeness:

Theorem 13 Limited Belief Reasoning with parameters k and |F| is co-W[P]-complete. The result also holds when k is input. Proof. Membership. We show that the co-problem is in W[P] using an NRAM that finds a falsifying assignment of names for all split terms. As in Theorem 11, the case k = 0 is straightforward. For k > 0 we loop over all function terms in F and for each we select a standard name from N ∪ {ˆn} with EXISTS. This requires |F||F| nondeterministic steps.

Hardness. We reduce from the complement of Weighted AntiMonotone Circuit Satisfiability, which is W[P]-complete [Flum and Grohe, 2006]. A circuit is anti-monotone when all inputs have out-degree 1 and feed into a not-node and there are no other not-nodes except those on top of some input. Let C = (V, E) be an anti-monotone circuit with inputs X. For every x ∈ X we denote the associated not-node by vx.

Let F = {fi | i ∈ [k]} ∪ {f} be function terms. Let N = {nv | v ∈ V \ X} ∪ {W} be standard names.

The idea is to represent that a node v is set to FALSE by f ̸=nv . The truth assignment is selected by splitting f1 , . . . , fk . Truth of an input x is represented by fi = nvx for some i ∈ [k], which triggers f ̸= nvx ; these values are propagated to the output node, so that f ̸= nv0 indicates that the circuit is falsified.

This is encoded in a set of clauses s as follows. For every i ∈ [k], let si be the least set that contains fi ̸=nvx ∨f ̸=nvx for every x ∈ X, and ∨x∈X fi = nvx ∨ fi =W. Let s be the least set such that s ⊇ si for all i ∈ [k], and fi ̸=nvx ∨fj ̸=nvx for every i, j ∈ [k] with i ̸= j and x ∈ X, and an encoding of the and- and or-nodes analogous to the one from the proof of Theorem 11.

We then prove that every S ⊆ X with |S| = k falsifies C iff for all n1, . . . , nk ∈ {nvx | x ∈ X}, s ∪ {f1 = n1, . . . , fk = nk} |≈ f ̸=nv0 by induction on the depth of C. The right-hand side can be rewritten to match Lemma 7 using Li = {fi ̸=W}, and thus fpt-reduces to Limited Belief Reasoning by Lemmas 7 and 4, which gives us co-W[P]-hardness.

Finally, the only remaining case is when Limited Belief Reasoning is parameterized by both |F| and |N|:

Proposition 14 Limited Belief Reasoning with parameters |F| and |N| is in FPT. This also holds when |N| is constant. Proof. The decision procedure runs in time (|F| · (|N|+k))k · p(m). By Lemma 2 we can estimate k ≤ |F|.

6 Conclusion

We have analyzed the complexity of Limited Belief Reasoning. While tractable for constant belief levels, the complexity jumps to PSPACE-complete in the general case. Using parameterized complexity theory, we showed how parameterized versions of the problem populate the space between these two extremes.

We believe our findings are relevant to the future development of the theory of limited belief. In particular, the insight that the limited belief level can actually increase the computational cost should be considered in future versions.

In light of PSPACE-completeness, one might implement a reasoning system using an off-the-shelf QBF-solver. Also, limited belief may be suitable as a modeling language for other problems in PSPACE.

So far, we have only considered Limited Belief Reasoning without first-order quantification; lifting this restriction would be a natural next step. Moreover, additional parameters could be studied, for example, parameters exploiting the structure of the knowledge base and the query, like backdoors [Gaspers and Szeider, 2012].

Another interesting question is whether our findings carry over to other approaches to resource-bounded reasoning using a similar splitting technique [D'Agostino, 2015].