A Tractable, Expressive, and Eventually Complete First-Order Logic of Limited Belief

1 Introduction

The whole idea of a knowledge-based system, going all the way back to [McCarthy, 1963], is to provide a system with a knowledge base (KB) of facts expressed in a logical language that the system would then draw conclusions from. But in trying to characterize just what conclusions the system should be able to draw, it has been difficult to come up with a notion of belief that allows for full-first order logic on the one hand, and is not overly demanding computationally on the other.

There has been considerable research on this topic (since our first efforts 35 years ago in [Levesque, 1984]), and we will review this research in a later section. In this paper, we present a new model of belief that is the culmination of our thoughts on this subject. Following [Liu et al., 2004], it is based on a notion of mental effort, characterized by a single parameter k. The idea is that when k = 0, the only sentences believed are those that are in the given KB (or "easy" logical consequences of them). At higher values of k, more and more logical consequences of the KB are revealed. The main properties we are claiming for this new model are the following:

Expressiveness: Any sentence of a first-order logic with equality and standard names can be a sentence in the KB and therefore believed at k = 0. In particular, it will be possible to believe (at k = 0) a disjunction without having to believe either disjunct, and to believe an existential without having to believe any of its instances.

Eventual completeness: Every sentence believed (at any level k) will be a logical consequence of the KB. In addition, if a sentence is a logical consequence of the KB, there will be a level k at which the sentence will be believed. So with enough mental effort it will be possible to do sound and complete first-order logical reasoning.

Tractability: The reasoning required to determine what is believed will be tractable in the following specific sense. Imagine that the KB consists of a potentially large number N of sentences each of which is bounded in size by a constant c. Suppose that we are interested in determining whether some other sentence (of size also bounded by c) is believed at some fixed level k. We will show that there is procedure that is polynomial in N for doing this.

(Note that although the elements of the KB can be of arbitrary logical form, belief is guaranteed to be tractable only when each individual sentence in the KB is small.) As far as we know, no existing model of belief, including our own earlier proposals, satisfy these properties. For example, cases where belief is guaranteed to be tractable might end up being less expressive than full first-order logic with equality, as in [Crawford and Etherington, 1998; Liu and Levesque, 2003; Liu et al., 2004], for example. Cases where all of first-order logic is allowed may fail to be eventually complete, that is, there may be logical consequences of the KB that are outside the reach of what can be believed [Patel-Schneider, 1985; Lakemeyer, 1996; Lakemeyer and Levesque, 2016].

The organization of the paper is as follows. In Section 2 we sketch the main ideas of our approach. Section 3 introduces the first-order logic with equality that our work is based on, and other logical preliminaries. Section 4 formalizes the notions of belief and only-believing that we are after, followed by a description of the full logic. In Section 6 we show that the logic indeed has all the desired properties and more. The paper ends with a discussion of related work and conclusions.

2 The Approach

In order to talk about what the system is considered to believe at any point, it will be convenient to use a logic of belief, where formulas Bkφ for k = 0, 1, 2 . . . are used to say that the system believes a first-order sentence φ at level k. (When we say that a logic of belief is tractable, expressive, and eventually complete, we mean that the notion of belief it characterizes has these properties.) In order to talk about the use of a knowledge base, we also use a form of only-believing by way of another modal operator Owhere Oφ means that φ is believed (at level 0), but nothing stronger [Levesque, 1990]. This will allow us to write sentences like (OKB ⊃ Bkφ), which can be read as "if the given knowledge base is KB, then φ is believed at level k." (When KB is used in a formula, we mean the conjunction of its elements.) The limited beliefs of a knowledge base can then be studied in terms of the valid sentences of this form.

With this logic of belief in mind, the properties of limited reasoning we are looking for are these:

• expressiveness: for any first-order φ, the sentence Oφ will be satisfiable, and moreover |= (Oφ ⊃ B0φ).
• cumulativity: for any k and any φ, |= (Bkφ ⊃ Bk+1φ).
• soundness: for any k, any KB and φ, if |= (OKB ⊃ Bkφ), then |= (KB ⊃ φ).
• eventual completeness: for any KB and φ, if |= (KB ⊃ φ), then there will be some k such that |= (OKB ⊃ Bkφ).
• tractability: for any KB and φ, the question as to whether |= (OKB ⊃ Bkφ) for fixed k will be decidable with polynomial data complexity as described above.

So while it will be computationally feasible to determine if Bkφ is true (with an effort that depends on the k), if an agent really needs to determine whether or not φ is true, it may have to look at higher and higher values of k. Because of the undecidability of first-order logic, it will be undecidable to determine whether there exists a k such that Bkφ is true.

2.1 Reduction to Clauses

One possible approach to satisfying the above requirements is to start with a sound and complete logical reasoning procedure (like Resolution, say), but cut it off after k steps. In other words, we might have arranged the semantics so that Bkφ is true iff φ can be derived from the KB by the reasoning procedure in k or fewer steps.

However, such a straightforward interpretation of belief levels is problematic, as it would likely mean that many desirable properties of belief are lost. For example, Bk(α ∧ β) and Bk(β ∧α) may not be logically equivalent, since the reasoning procedure might need some extra steps to go from one conjunction to the other. As we will see in Section 6, our notion of belief will preserve these and other equivalences.

In the semantics of O and Bk to follow starting in the next section, we obtain these desirable equivalences by reducing the general definition of belief over arbitrary sentences to belief over ground clauses, that is, disjunctions of literals. We will be making use of reductions of the following forms:

1. Bkφ will hold iff Bk∃⃗x.ψ holds, where the formula ψ is a Skolemized version of φ with no quantifiers;
2. Bk∃x.ψ will hold iff there are terms t0, . . . , tk such that Bk(ψx t0 ∨ · · · ∨ ψx tk ) holds;
3. finally, when φ is quantifier-free, Bkφ will hold iff for every ground clause c in the CNF of φ, Bk(c) holds.

The reduction in item (1) involves a conversion to prenex form and the dual form of Skolemization (sometimes called Herbrandization) where universally quantified variables are eliminated using Skolem functions; item (2) is what amounts to an application of a bounded version of Herbrand's Theorem [Buss, 1998]; finally, item (3) involves the usual conversion to CNF.

This of course still leaves us with the problem of specifying which ground clauses c are to be believed given a KB. We need to be careful here, since the problem of determining whether KB logically entails a ground clause c (even without equality) is already undecidable. In fact, it is undecidable even when the KB is a single universally quantified clause.

2.2 Epistemic States

In possible-world semantics [Kripke, 1959; Hintikka, 1962; Chellas, 1980], perhaps the simplest model of the epistemic state of a KB is the set of all worlds satisfying the KB, given a fixed universe of discourse [Levesque and Lakemeyer, 2001]. For tractable reasoning however, this notion of epistemic state is too coarse, as it lumps together all logically equivalent knowledge bases. For example, for KB = {p, (p ⊃ q)}, we might want an epistemic state where B0(q) is false, but for the logically equivalent KB = {p, (p ⊃ q), q}, we want a different epistemic state where B0(q) would be true.

So in this paper, we will be using a much finer-grained notion of epistemic state. There may be many ways of doing this (and see future work), but we will show here that it is sufficient to think of an epistemic state not as a set of worlds, but as a finite set of clauses (which may contain variables). Intuitively, these clauses are the ones obtained by Skolemizing the KB and converting it to CNF. This solves the problem above since logically equivalent knowledge bases need not correspond to the same epistemic state when they do not have the same CNF (like the two examples above). (However, if two of them have exactly the same CNF, only believing one will end up being equivalent to only believing the other.)

The use of clauses as epistemic primitive is not new and dates back to [Liu et al., 2004], where epistemic states were possibly infinite sets of ground clauses (see also Section 7). While we consider finite sets of clauses with variables, these can be thought of as representing the (infinite) set of all ground instances.

2.3 When Are Clauses Believed?

What we will be proposing for the belief of clauses is easiest to understand in the propositional case (without the complications of quantifiers or equality). First, define a clause to be trivial iff it contains complementary literals. Then define

So RP(C) performs one step of Resolution on the elements of C, RP(RP(C)) performs two steps, and so on. Then finally, define a clause b to be believed at level k in an epistemic state defined by a set of clauses C iff b is trivial or there is a clause a ∈ RPk (C) such that a ⊆ b. For example, if the epistemic state is defined by {(p∨q), (¬p∨r), (¬q∨r)}, then the clauses (p ∨ q) and (s ∨ ¬s) and their supersets are believed at levels 0 and above, the clause (p ∨ r) and its supersets are believed at level 1 and above, and the clause r and its supersets are believed at level 2 and above. The rest of the paper will make all these ideas precise for a full first-order logic with equality and standard names.

3 First-Order Preliminaries

We begin by introducing the logic L from [Levesque and Lakemeyer, 2001] as our base logic, followed by various other notions we need from first-order logic.

3.1 The Base Logic L

The language of L is a first-order dialect with = and an infinite supply of function and predicate symbols of every arity. In addition, the language also features a set N of standard names #1, #2, #3, . . . , which are syntactically treated like constants but which are intended to be isomorphic to the (fixed) domain of discourse. In other words, standard names can be thought of as constants that satisfy the unique name assumption and an infinitary version of domain closure. Among other things, standard names allow for a very simple, substitutional account of quantifiers. See [Levesque and Lakemeyer, 2001] for more discussion on why standard names are useful. In the following we often simply write "name" instead of "standard name." Terms and atomic formulas are defined in the usual way, and so are formulas using the connectives ¬ and ∧ and the quantifier ∀. Other connectives like ∨,⊃,≡ and the quantifier ∃ are freely used as syntactic abbreviations. Any formula from L is also called an objective formula. A sentence is a formula without free variables.

Function symbols with names as arguments are called primitive terms, and predicate symbols with names as arguments are called primitive atoms.

The semantics is defined in terms of worlds, which are mappings from the primitive terms into N and from the primitive atoms into {0, 1}.

The meaning of an arbitrary ground term is given in terms of its coreferring standard name. Formally, given a ground term t and a world w we define |t|w (read: the coreferring standard name for t given w) by:

1. If t ∈ N, then |t|w = t;

The truth of a sentence wrt world w (written as w |= φ) is defined inductively as follows:

1. w |= (t1 = t2) iff |t1|w and |t2|w are the same names;
2. w |= ¬φ iff w ̸|= φ;
3. w |= (φ ∧ψ) iff w |= φ and w |= ψ;
4. w |= ∀x. φ iff w |= φxn for all names n;

Here φxn stands for φ with every free occurrence of x replaced by n. A sentence φ is valid (|= φ) iff for all worlds w, w |= φ.

Apart from standard names and equality, L behaves exactly like classical first-order logic: it is shown in [Levesque and Lakemeyer, 2001] that a sentence without standard names and equality is valid iff it is valid in classical logic. Standard names are, of course, special in that sentences like (#6 ̸= #7) are valid, for example. Also, since the domain of discourse is infinite, sentences like ∃x∀y(x = y) are unsatisfiable in L.

3.2 Other Preliminaries

The logic of belief here uses the language L but incorporates some ideas from standard first-order logic that we review here. First some notation. We use the following metavariables throughout: x, y for variables, t, u, v for terms, n for standard names, f, g for function symbols, p, q for predicate symbols, a, b, c, d for clauses (defined below), θ for substitutions, ρ, τ, µ for literals, ¯ ρ for the complement of a literal, φ, ψ, χ for objective formulas, i, j, k,m, r, s for nonnegative integers. A capitalized version of any of these will be used for sets. We assume throughout that all formulas are rectified, that is, that no variable appears bound by two quantifiers, one within the scope the other, as in something like ∃x(φ ∧ ∀xψ)))). For any substitution θ, and any literal, clause, formula, or set of clauses z, zθ is like z but with free variables x in z replaced by θ(x). Two literals ρ and τ with distinct variables unify if there is a θ such that ρθ = τθ. A most general unifier of two literals is one where any other unifier can be obtained by applying further substitutions.

A clause is a finite set of literals (including equalities and inequalities) which we understand intuitively as a disjunction. (The empty clause is understood as a formula that is always false.) For any formula φ ∈ L without quantifiers, CNF(φ) is the finite set of clauses that results from putting φ into conjunctive normal form, defined as follows:

Definition 1 Assume that φ has no quantifiers and has been rewritten so that it does not use ∨, ⊃, or ≡. Then CNF(φ) is defined inductively by:

1. CNF(φ) = {{φ}}, when φ is a literal;
2. CNF(φ ∧ψ) = CNF(φ) ∪CNF(ψ);
3. CNF(¬¬φ) = CNF(φ);
4. CNF(¬(φ ∧ψ)) = {a ∪ b | a ∈ CNF(¬φ), b ∈ CNF(¬ψ)}.

We obtain the following property of CNF:

Proposition 1 Let φ be any formula with no quantifiers.

If CNF(φ) = {c1, . . . , ck},

For any formula φ ∈ L, SKO(φ) is the formula without quantifiers that results from Skolemizing φ, defined as follows:

Definition 2 Assume that φ has been rewritten so that it does not use ∃, ∨, ⊃, or ≡. Then let SKO(φ) = SKO′ (φ, {}), which is defined inductively by:

1. SKO′ (φ,X) = φ, when φ is a literal;
2. SKO′ ((φ ∧ψ),X) = (SKO′ (φ,X) ∧ SKO′ (ψ,X));
3. SKO′ (¬¬φ),X) = SKO′ (φ,X);
4. SKO′ (¬(φ∧ψ),X) = (SKO′ (¬φ,X)∨SKO′ (¬ψ,X));

1. SKO′ (∀xφ,X) = SKO′ (φ,X ∪ {x});
2. SKO′ (¬∀xφ,X) = SKO′ (¬φxt ,X), where t = f(x1, . . . , xn), where X = {x1, . . . , xn} and f is a function symbol (a so-called Skolem function) that occurs nowhere else.

In a nutshell, Skolemization involves replacing each existentially quantified variable in a formula by a new function applied to all the universally quantified variables that it appears within the scope of. We can get a version of Skolemization that replaces universally quantified variables instead of existential ones by using ¬SKO(¬φ), which is sometimes referred to as Herbrandization. This is made precise in the following proposition:

Proposition 2 For any objective φ, let ψ be the formula that results from removing all quantifiers from φ. Then there are substitutions θ and θ′ such that SKO(φ) = ψθ and SKO(¬φ) = ¬ψθ′ . Moreover, θ and θ′ can be unified: there is a θ∗ such that θθ∗ = θ′ θ∗ .

Definition 3 For any two literals ρ and τ, MGU[ρ, τ] is the set of most general unifiers of ρ and τ (empty if the two literals do not unify).

Definition 4 UNA = {{¬(n = n′ )} | n and n′ are distinct standard names }.

Definition 5 For function symbols F and predicate symbols P, EQF,P is the union of the following sets of clauses:

1. {(x = x)},
2. {¬(x = y), (y = x)},
3. {¬(x = y), ¬(y = z), (x = z)},
4. {¬(x1 = y1), . . . , ¬(xk = yk), (f(x1, . . . , xk) = f(y1, . . . , yk))}, for every k-ary function symbol f ∈ F ,

for every k-ary predicate symbol p ∈ P.

Note that these clauses are equivalent to the standard axioms of equality restricted to the symbols in F and P. When the context is clear, we omit the F and P subscripts.

Finally, we say that a set of clauses (possibly with variables) is first-order satisfiable (or fo-satisfiable) if it is satisfiable in classical first-order logic. There is a close connection between these notions and L: a sentence φ is valid in L, that is, |= φ iff the set of clauses EQ∪UNA∪CNF(SKO(¬φ)) is fo-unsatisfiable.

4 Believing and Only-Believing

To define the logic of belief in the next section, we begin by defining what it means to believe a clause and a sentence, following the approach outlined above in Section 2.

Definition 6 An epistemic state is any finite set of clauses, where the variables in each clause are distinct.

Definition 7 A clause c is trivial iff it contains complementary literals or an element of UNA.

Note that (n = n) is not a trivial clause, but will be handled as a consequence of the first item of EQ defined above.

In these definitions, we assume the clauses in C use distinct variables, and that just one θ is chosen (if one exists) so that the new clauses cθ and (a ∪ b)θ also have distinct variables. Definition 8 realizes what is known as Factoring, that is, the unification of literals within the same clause, which is needed for Resolution to be complete. For example, if [P(x), P(a),Q(x)] is in C, then [P(a),Q(a)] is in F(C). Note that F(C), while recursive, is well defined, as in each step newly added clauses have fewer literals than those from which they were generated. Definition 9 then performs one step of resolution on all clauses in C extended by those obtainable by Factoring.

Definition 10 For any integer k ≥ 0, clause b, and set of clauses C, we say that b is believed at level k in epistemic state C (written C, k |= b) iff b is trivial or there exist θ and a ∈ RPk (C ∪ EQF,P ) such that for every ρ ∈ aθ, ¯ ρ ∈ UNA or ρ ∈ b. (The F and P here are sets that contain the function and predicate symbols in C or b.)

This definition goes well beyond the propositional version given in Section 2. It handles equality by making EQ be part of the argument to RP, and it handles standard names by first, incorporating UNA in the definition of trivial, and second, by allowing a ∈ RP to contain literals that are not in b as long they are guaranteed to be false (like #5 = #7).

We can now define what it means to believe an arbitrary objective sentence of L:

Definition 11 For any integer k ≥ 0, objective sentence ψ, and set of clauses C, we say that ψ is believed at level k in epistemic state C iff there are k + 1 substitutions, θ0, . . . , θk, such that for all clauses b ∈ CNF(ψ′ θ0 ∨ · · · ∨ ψ′ θk), where ψ′ = ¬SKO(¬ψ), we have that C, k |= b.

Note that believing ψ involves Skolemizing ¬ψ (and then negating the result) so that existentially quantified variables remain but universally quantified ones disappear. So, for example, ∀x.q(x) is believed at level k iff the clause {q(u)} is believed at level k, where u is a new Skolem constant appearing nowhere else. (Since the KB in question cannot mention u, the sentence will only be believed if the KB entails a suitable universal.) But ∃x.q(x) will be believed at level k iff there are terms t0, . . . , tk (not necessarily new ones) such that the clause {q(t0), . . . , q(tk)} is believed at level k. For a concrete example, consider the sentence ψ = ∃x∀y(¬P(y) ∨ P(x)), which is valid and equivalent to ∀y¬P(y) ∨ ∃xP(x). After Skolemizing the universal we obtain ψ′ = (¬P(f(x)) ∨ P(x)). Now consider two substitutions θ0 and θ1, where θ0 maps x to itself and θ1 maps x to f(x). Then CNF(ψ′ θ0 ∨ ψ′ θ1) is the trivial clause [¬P(f(x)), P(x), ¬P(f(f(x))), P(f(x))]. Hence, if C is empty then ψ is believed at level 1 but not at level 0.

Finally, let us now consider what it means to say that φ is all that is believed:

Definition 12 For any objective sentence φ and set of clauses C, we say that φ is only-believed in epistemic state C iff there is a relabelling of the variables and Skolem functions in C such that C = CNF(SKO(φ)).

As mentioned above, having φ logically equivalent to ψ does not make only-believing φ the same as only-believing ψ. For example, let φ = (p ∧ (¬p ∨ q)) and let ψ = (φ ∧ q). Then only-believing φ requires an epistemic state with exactly two clauses, while only-believing ψ requires an epistemic state with three clauses. These two epistemic states will have different beliefs: the sentence q will not be believed at level 0 in the first one, but it will in the second. (They will agree, however, on beliefs at level 1 and beyond.)

Note also that only-believing φ involves Skolemizing φ itself (and not its negation), so that universally quantified variables remain but existentially quantified ones now disappear. So, for example, ∀x.q(x) is only-believed in C iff C consists of the single clause {q(x)} (or a variant with some other variable). But ∃x.q(x) is only-believed in C iff C consists of the single clause {q(v)}, where v is a Skolem constant.

5 A Logic of Limited Reasoning

Our logic of belief extends L by adding belief operators. In particular, for any objective formula φ and any non-negative integer k, Bkφ and Oφ are also formulas. Note that we do not consider nested beliefs here. A formula is called subjective if all predicate and function symbols appear within the scope of a modal operator.

The semantics of sentences of the extended language is defined with respect to worlds and epistemic states, that is, sets of clauses. For the objective part, the semantics is identical to that of L.

Definition 13 For any set of clauses C, any world w, and any sentence α, we say that α is true wrt C and w (written C, w |= α) according to the following definition:

1. C,w |= p(t1, . . . , tm) iff w[p(|t1|w, . . . , |tm|w)] = 1;
2. C,w |= (t1 = t2) iff |t1|w and |t2|w are ident. names;
3. C,w |= ¬α iff C,w ̸|= α;
4. C,w |= (α∧ β) iff C,w |= α and C,w |= β;
5. C,w |= ∀x.α iff C,w |= αxn for all standard names n;
6. C,w |=Bkφ iff φ is believed at level k in ep. state C;
7. C,w |=Oφ iff φ is only-believed in epistemic state C.

When α is subjective, we leave out the w and write C |= α. We say that α is valid in this logic (written |= α) iff C, w |= α for every finite set of clauses C and world w.

Before looking at the general properties of this logic, let us consider a simple example:

We show that |= (O∀x(x ̸= #5 ⊃ p(x)) ⊃ B0p(#7)). Suppose that C |= O∀x(x ̸= #5 ⊃ p(x)). Then C consists of one clause, {x = #5, p(x)}, modulo renaming of x. So that clause is an element of RP0 (C∪EQ). Now let θ0 be the empty substitution. Let ψ′ = ¬SKO(¬p(#7)) = ¬¬p(#7), so that CNF(ψ′ θ0) = {{p(#7)}}. So for every b ∈ CNF(ψ′ θ0) there is indeed a clause a ∈ RP0 (C∪EQ) (namely {x = #5, p(x)}) and a θ (namely [x/#7]), such that for each literal ρ ∈ aθ, either ¯ ρ ∈ UNA (when ρ is #7 = #5) or ρ ∈ b (when ρ is p(#7)). Therefore, C |= B0p(#7).

6 Properties of the Logic

In this section, we confirm that the logic of belief defined above behaves appropriately. We prove that it has the desired properties listed in Section 2.

6.1 Satisfying the Desiderata

Theorem 1 (Cumulativity) |= (Bkψ ⊃ Bk+1ψ).

Proof: The theorem follows easily from the fact that for any a, k, and C, if C, k |= a then C, k + 1 |= a.

For expressiveness, we need this lemma:

Lemma 1 φ is believed at level 0 in the epistemic state CNF(SKO(φ)).

Proof: Let C = CNF(SKO(φ)) and D = CNF(¬SKO(¬φ)). We need to show that there is a θ0 such that for every b ∈ CNF(Dθ0), C, 0 |= b. Let θ, θ′ , and θ∗ be as in Proposition 2. So C = CNF(ψ)θ and D = CNF(ψ)θ′ . Let θ0 = θ∗ and suppose b is any element of Dθ0 = CNF(ψ)θ′ θ∗ . So there is a b′ ∈ CNF(ψ) such that b = b′ θ′ θ∗ . But b′ θ′ θ∗ = b′ θθ∗ . So b′ θ ∈ C and b′ θθ∗ = b. Therefore, C, 0 |= b.

Theorem 2 (Expressiveness)

For any objective sentence φ, the sentence Oφ is satisfiable, and moreover |= (Oφ ⊃ B0φ).

Proof: Let C = CNF(SKO(φ)). Then C |= Oφ. Now assume that C ′ is any finite set of clauses. If C ′ |= Oφ, then C ′ is like C except for a possible relabelling. By Lemma 1, φ is believed at level 0 in C, and so C ′ |=B0φ.

Turning now to tractability, we have the following:

Lemma 2 There is a procedure which given b, k and C can decide whether or not C, k |= b.

Proof: Here is a sketch of the procedure: First calculate C ′ = RPk (C ∪ EQ) in the obvious way. (This C ′ will be finite.) Then confirm that either b is trivial or there is a θ and a c ∈ C ′ such that for every ρ ∈ cθ, ¯ ρ ∈ UNA or ρ ∈ b. (This is a small tweak to a procedure known to be decidable called theta-subsumption.)

Theorem 3 (Tractability) Suppose that φ1, . . . , φN, ψ are sentences such that |φi| < c and |ψ| < c, where c is some constant. Let φ = (φ1 ∧ · · · ∧ φN). Then for any k ≥ 0, the validity of (Oφ ⊃ Bkψ) can be determined in time polynomial in N.

Proof: Here is a sketch of a decision procedure which runs in time polynomial in N: First, calculate C = CNF(SKO(φ)), ψ′ = ¬SKO(¬ψ), and guess at a Θ = {θ0, . . . , θk}. Then calculate B = CNF(ψ′ θ0 ∨ · · · ∨ ψ′ θk). Finally, use the procedure of Lemma 2 to confirm for each b ∈ B that C, k |= b. The θi in question will be substitutions that map the variables in ψ′ to the (finitely many) terms that appear in SKO(φ) or SKO(¬ψ).

Note that this procedure requires converting the entire knowledge base φ to CNF, which can be exponential in general. However, it is polynomial here since φ is assumed to be a conjunction of small sentences. For any fixed k, the calculation of C ′ = RPk (C ∪ EQ) required by Lemma 2 will be polynomial in |C|, but of course, this will grow exponentially as k increases. A similar argument applies when converting (ψ′ θ0 ∨· · ·∨ψ′ θk) into CNF, since the query is also assumed to be bounded in size. Note that, in the case of Factoring (F), which is part of RP, for each clause at most a polynomial number of new clauses is added. (Note also that the RPk calculation only needs to be done once, however, and can even be done offline before considering any queries.) The "guessing" of an appropriate Θ in the proof can be made determinate by trying all potential MGUs between terms in ψ′ and terms in C, of which there are only polynomially many. Overall, under the given assumptions and for any fixed k, the procedure will be polynomial in the size of the knowledge base.

To obtain soundness and eventual completeness, we need the following lemmas:

Lemma 3 Let C be a finite set of clauses, and φ an objective formula. If for all d ∈ CNF(φ), C, k |= d, then C ∪ EQ ∪ UNA ∪ {¬φ} is fo-unsatisfiable.

Proof: SupposeM is a first-order interpretation andM satisfies C ∪EQ∪UNA. Since M satisfies UNA, M satisfies any trivial clause and M also satisfies RPk (C∪EQ) (by induction on k). So for any d, if C, k |= d, then M satisfies d. Therefore, M satisfies all the clauses in CNF(φ). So M satisfies φ and does not satisfy ¬φ.

Lemma 4 Let C be a finite set of clauses, and φ a formula. (Both can have variables.) Then the set of clauses C∪EQ∪UNA∪CNF(φ) is fo-unsatisfiable iff there is a k and substitutions θ0, . . . , θk such that for all d ∈ CNF(¬φθ0 ∨ · · · ∨ ¬φθk), C, k |= d.

Proof: (Sketch) (⇐) Suppose that for all d ∈ CNF(¬φθ0 ∨ · · ·∨¬φθk), C, k |= d. By Lemma 3, C∪EQ∪UNA∪{φθ0∧ · · · ∧φθk} is fo-unsatisfiable, and so the set C ∪EQ∪UNA∪ CNF(φ) must be fo-unsatisfiable also.

(⇒) Now suppose C ∪ EQ ∪ UNA ∪ CNF(φ) is founsatisfiable. Let D = CNF(φ). By the refutation completeness of Resolution, there is a resolution derivation of the empty clause from the clauses in C ∪ EQ ∪ UNA ∪ D. Say the derivation is b0, . . . br where br = {}. We prove the following claim: For every 0 ≤ j ≤ r, there is a k such that for every θ, there are substitutions θ0, . . . , θk such that for all clauses d ∈ CNF(¬φθ0 ∨ · · · ∨ ¬φθk), C, k |= bjθ ∪ d. The theorem will then follow since br = {}.

The proof is by induction on j. For the base case (j = 0), we have b0 ∈ C∪EQ∪UNA∪D, and it can be shown that the lemma holds for k = 0. In the induction step, bj can be either the result of a resolution step or factoring. In both cases, there is a k such that C, k |= bjθ ∪ d.

Theorem 4 (Soundness and Eventual Completeness) Let φ and ψ be objective sentences. Then |= (φ ⊃ ψ) iff for some k, |= (Oφ ⊃ Bkψ).

Proof: We have |= (φ ⊃ ψ) iff EQ∪UNA∪CNF(SKO(φ∧ ¬ψ)) is fo-unsatisfiable iff CNF(SKO(φ)) ∪ EQ ∪ UNA ∪ CNF(SKO(¬ψ)) is fo-unsatisfiable iff (by Lemma 4) for some k, there are substitutions θ0, . . . , θk such that for all d ∈ CNF(ψ′ θ0 ∨ · · · ∨ ψ′ θk), C, k |= d, where ψ′ = ¬SKO(¬ψ) iff for some k, ψ is believed at level k in epistemic state CNF(SKO(φ)) iff for some k, |= (Oφ ⊃Bkψ).

6.2 The Logical Properties of Belief

Theorem 5 (Equivalent beliefs) For any k and any objective sentences φ, ψ, and χ, the following sentences are valid:

Bkφ ≡ Bk(φ ∧ φ), Bkφ ≡ Bk(φ ∨ φ), Bkφ ≡ Bk¬¬φ, Bk(φ ∧ ψ) ≡ Bk(ψ ∧ φ), Bk(φ ∨ ψ) ≡ Bk(ψ ∨ φ), Bk(¬(φ ∧ ψ)) ≡ Bk(¬φ ∨ ¬ψ), Bk(¬(φ ∨ ψ)) ≡ Bk(¬φ ∧ ¬ψ). Bk(φ ∧ (ψ ∧ χ)) ≡ Bk((φ ∧ ψ) ∧ χ)), Bk(φ ∨ (ψ ∨ χ)) ≡ Bk((φ ∨ ψ) ∨ χ)), Bk(φ ∧ (ψ ∨ χ)) ≡ Bk((φ ∧ ψ) ∨ (φ ∧ χ)),

Bk(φ ∨ (ψ ∧ χ)) ≡ Bk((φ ∨ ψ) ∧ (φ ∨ χ)),

These follow from the fact that CNF(¬SKO(¬φ)) = CNF(¬SKO(¬ψ)) implies |= (Bkφ ≡ Bkψ).

Theorem 6 (Non-equivalent beliefs) There are obj. sentences φ and ψ such that |= (φ ≡ ψ), but ̸|= (Bkφ ≡ Bkψ).

Proof: Let p and q be distinct atomic sentences. Let φ = (p ∧ (¬p ∨ q)) and ψ = (φ ∧ q). Then |= (φ ≡ ψ), but ̸|= (B0φ ≡ B0ψ).

The final thing to show is the relationship between beliefs and logical combinations of other beliefs.

Theorem 7 For any sentences φ and ψ and any formula χ with a single-free variable x:

1. |= (Bkφ ∨Bkψ) ⊃Bk(φ ∨ψ).
2. |= ∃xBkχ ⊃Bk∃xχ.
3. |= Bk(φ ∧ψ) ⊃ (Bkφ ∧Bkψ), but the converse fails.
4. |= Bk∀xχ ⊃ ∀xBkχ, but the converse fails.

Proof: Here we only prove (3.): The formula ¬SKO(¬(φ∧ ψ)) is (¬SKO(¬φ) ∧ ¬SKO(¬ψ)). So CNF(¬SKO(¬(φ ∧ ψ))) = CNF(¬SKO(¬φ)) ∪ CNF(¬SKO(¬ψ)). So if C |= Bk(φ ∧ ψ), then C |= Bkφ and C |= Bkψ. Regarding the converse, let φ = ∃x.p(x), ψ = ∃y.q(y), and C = {{p(#1), p(#2)}, {q(#1), q(#2)}}. Then C |= B1φ

We do however get "eventual" versions of the closure of belief under conjunction and universal generalization:

Theorem 8 For any φ, ψ, χ as above, any k and finite C:

7 RelatedWork

Perhaps the best understood formal models of belief are those based on possible-world semantics [Kripke, 1959; Hintikka, 1962; Halpern and Moses, 1992]. However, it was recognized early on that belief under this framework suffers from logical omniscience [Hintikka, 1975], that is, beliefs are closed under (classical) logical entailment and hence reasoning becomes intractable in the propositional and even undecidable in the first-order case.

Later, weaker logics of belief started to emerge with a focus on tractability, but initially restricted to the propositional case. These include [Levesque, 1984; Cadoli and Schaerf, 1996; Frisch, 1987; Fagin et al., 1990; Delgrande, 1995; Cadoli and Schaerf, 1996] and either provided an explicit model of limited belief or a limited entailment relation, often based on tautological entailment [Dunn, 1976], a fragment of relevance logic [Anderson and Belnap, 1975]. There were also proposals for tractable entailment relations of increasing complexity [Dalal, 1996; Crawford and Etherington, 1998; D'Agostino, 2015], again limited to the propositional case. In a first-order setting, tractable reasoning was investigated either in terms of limited inference [Levesque, 1998; Liu and Levesque, 2003] or in terms of belief levels as in this paper [Liu et al., 2004; Liu and Levesque, 2005; Lakemeyer and Levesque, 2013; 2014; 2016; Schwering, 2017]. In this line of work, epistemic states, which they call setups. are also sets of clauses, but in contrast to our approach they need to be ground. Belief levels are defined in terms of splitting, either on a clause in the epistemic state [Liu et al., 2004; Liu and Levesque, 2005; Lakemeyer and Levesque, 2013], an arbitrary ground literal [Lakemeyer and Levesque, 2014], or on the possible denotations of a term [Lakemeyer and Levesque, 2016; Schwering, 2017]. For example, splitting on a literal l at belief level k means adding l to the epistemic state and then checking whether the belief in question obtains at level k-1, and doing the same for the complement of l. These approaches, as well as [Crawford and Etherington, 1998; D'Agostino, 2015] discussed next, go further than us in allowing the use of unit propagation, that is, resolution with a clause containing a single literal, already at belief level 0. In all cases reasoning is tractable for every belief level k. While the knowledge base needs to be in CNF, query evaluation does not require a transformation into CNF. Schwering [2017] also provides an implementation for his logic with interesting results for games like Sudoku or Minesweeper.

Closely related to ours is the work by D'Agostino [2015], who proposes a three-valued nondeterministic semantics which was also considered in [Crawford and Etherington,

1998], together with a k-consequence relation, where splitting is allowed on arbitrary formulas at levels greater than 0. Again, tractability results are obtained for every level k, and here neither the KB nor the query need to be transformed into CNF. The author also provides a sound and complete prooftheoretic account of the k-consequence relation. But again, this is all for a propositional language only.

There are very few expressive models of limited reasoning handling full first-order logic such as [Patel-Schneider, 1985; Lakemeyer, 1996; Lakemeyer and Levesque, 2016]. None of the approaches are eventually complete for full first-order logic, although a few proposals, such as [Lakemeyer and Levesque, 2014; D'Agostino, 2015; Klassen et al., 2015; Lakemeyer and Levesque, 2016], do exhibit eventually completeness for the propositional case.

Finally, returning to Hintikka, he considered ideas related to ours a long time ago [Hintikka, 1973]. His proposal deals with full first-order logic and distinguishes notions such as trivial inconsistencies vs. those that need to be discovered. In contrast to us, he uses a special disjunctive normal form, where each disjunct represents possible worlds. There is no discussion of tractability, however. We leave it to future work to investigate what the exact connections are.

8 Conclusions

In this paper we proposed, for the first time, a first-order logic of limited belief which is at once tractable, expressive, and eventually complete. One possible direction for future work involves simplifying the semantics by replacing the use of clauses in the definition of belief by threevalued interpretations. (Interestingly, this seems to work fine in the propositional case, but in the first-order case, the use of Skolemization and what amounts to the Herbrand Theorem still appears to be needed.) There are at least two directions in which the logic could be extended. For one, we so far completely ignored nested beliefs, which are necessary when an agent needs to introspect on what is and is not believed. Previous approaches to limited belief that considered introspection include [Lakemeyer, 1996; Lakemeyer and Levesque, 2013]. For another, there are additional easy forms of reasoning one may want to include even at belief level 0. A simple example would be unit propagation which, as noted in the related-work section, was included in the proposals presented in [Crawford and Etherington, 1998] and later in [D'Agostino, 2015] as well as [Liu et al., 2004] and its descendants. In the case of a very expressive language like ours, one must be careful, however, as an unrestricted use of unit propagation is already undecidable. Possible restrictions could be to restrict unit propagation to when the arguments of the predicates are standard names, or to when the nesting of function symbols does not exceed a certain depth.

Acknowledgments

We thank the reviewers for their thoughtful comments, which helped improve the presentation of the paper. Gerhard Lakemeyer also acknowledges his affiliation with the University of Toronto while this work was conducted.