A Reasoning System for a First-Order Logic of Limited Belief

1 Introduction

Dealing with incomplete knowledge is one of the longstanding aims of research in Knowledge Representation and Reasoning. Incompleteness often demands highly expressive languages to be represented accurately. For instance, the statement

"I don't know who Sally's father is, but I know he's rich"

involves an individual (Sally's father) and both knowns (he's rich) and unknowns (his identity) about him. From the representational point of view, first-order and modal logics are excellent tools to formalise such statements. However, reasoning in classical first-order logic very quickly gets undecidable: an existential quantifier and two unary functions with equality can be enough to make validity an undecidable problem [B¨orger et al., 1997].

One way to get around undecidability of first-order reasoning is through models of limited belief. 1 Inspired by natural agents, the idea behind limited belief is to give up the property of logical omniscience [Hintikka, 1975]. This separates limited belief from other approaches to decidable reasoning like the classical prefix-vocabulary classes [B¨orger et al., 1997] or description logics [Baader, 2003], but is similar to approaches of approximate reasoning like [D'Agostino, 2015]. While a number of models of limited belief have been proposed in the past [Konolige, 1986; Vardi, 1986; Fagin and Halpern, 1987; Levesque, 1984b; Patel-Schneider, 1990; Lakemeyer, 1994; Delgrande, 1995], these approaches can be criticised for either being too fine-grained or overly weakening the entailment relation and thus even ruling out the most basic cases of modus ponens.

1 We use the terms knowledge and belief interchangeably.

A more recent proposal for limited belief is due to Liu, Lakemeyer, and Levesque [2004]. Their logic is equipped with a perspicuous semantics based on clause subsumption, unit propagation, and case splitting, 2 and keeps the computational complexity under control by stratifying beliefs in levels: level 0 comprises only the explicit beliefs; every following level draws additional inferences by doing another case split. Every query specifies at which belief level it shall be evaluated, and thus controls how much effort should be spent on proving it. The rationale behind this technique of limiting belief by case splits is the hypothesis that in many practical reasoning tasks few case splits - perhaps no more than one or two - suffice.

Let us consider a brief example to illustrate the idea. Suppose we have the following knowledge base (KB):

At level 0 the agent believes these clauses, but does not draw any meaningful inferences from them yet. For instance, Rich(Frank)∨Rich(Fred), while entailed in classical logic, is not believed at level 0. It can however be inferred by splitting the cases for Sally's potential fathers:

• if fatherOf(Sally) = Frank, then we obtain Rich(Frank) by unit propagation with the second clause from the KB;
• if fatherOf(Sally) =Fred, then analogously Rich(Fred);
• if fatherOf(Sally) is anyone else, then unit propagation with the first clause in the KB yields the empty clause.

Either of the three cases subsumes Rich(Frank) ∨ Rich(Fred). Hence, Rich(Frank) ∨ Rich(Fred) is believed at level 1.

2 A clause is a disjunction of literals. Subsumption refers to inferring a clause c2 from a clause c1 when every literal in c1 subsumes a literal in c2. Unit propagation of a clause c with a literal ℓ means to remove all literals from c that are complementary to ℓ. A case split means to branch on all possible values a literal or term can take.

Several variants of Liu, Lakemeyer, and Levesque's original theory have been developed [Lakemeyer and Levesque, 2013; 2014; 2016; Klassen et al., 2015; Schwering and Lakemeyer, 2016]; they include concepts like introspection, actions, functions, or conditional beliefs. Despite this progress, the framework has remained a purely theoretical one without practical applications.

In this paper, we want to bring their approach to limited belief to practice. We make two contributions to this end:

• Firstly, we devise a logic of limited belief that unifies some concepts from the earlier proposals and adds several features to make it more attractive for practical use. The result is a sorted first-order logic with functions and equality and two introspective belief operators, one for knowledge and one for what is considered possible. While closely related to the earlier proposals, many technical details in this new language have been changed with practical considerations in mind.
• Secondly, we present a reasoning system that uses this logic as representation language. Our evaluation is twofold. Besides modelling toy domains to showcase the language's expressivity, we have also tested the system's performance with two popular puzzle games, Sudoku and Minesweeper. The results confirm the hypothesis that small belief levels often suffice to achieve good results.

The paper is organised as follows. In Section 2 we introduce an (omniscient) logic of knowledge. Based on this logic, we then develop a logic of limited belief in Section 3. In Section 4 we sketch a decision procedure for limited belief, discuss an implementation of this system, and present experiment results. Proofs of the results presented in this paper can be found in [Schwering, 2017].

2 A Logic of Knowledge

The logic we present in this section is a variant of Levesque's logic of only-knowing [Levesque, 1990] and will serve as a reference for the logic of limited belief in the next section. We refer to the logic from this section as L.

2.1 The Language

The language of L is a sorted first-order dialect with functions, equality, standard names, and three epistemic modalities. With minor modifications, this language will also be the language used for the logic of limited belief LL.

We assume an infinite supply of sorts, and for each sort we assume an infinite number of variables, function symbols of every arity j ≥ 0, and standard names (or names for short). Standard names serve as special constants that satisfy the unique name assumption and an infinitary version of domain closure. The set of terms (of a sort s) contains all variables (of sort s) and names (of sort s) as well as all functions f(t1, . . . , tj) where f is a j-ary function symbol (of sort s) and every ti is a variable or a name (not necessarily of sort s). A literal is an expression of the form t1 = t2 or ¬t1 = t2 where t1 is a variable, name, or function, and t2 is a variable or a name. The set of formulas is the least set that contains all literals and all expressions ¬α, (α ∨ β), ∃xα, Kα, Mα, and Oα where α and β are formulas and x is a variable.

Intuitively, Kα reads as "α is known," Mα as "α is considered possible," and Oα as "α is all that is known." We say a formula is objective when it mentions no belief operator, and subjective when it mentions no function outside of a belief operator. Only-knowing is particularly useful to capture the meaning of a knowledge base. As we only consider objective knowledge bases in this paper, we restrict ourselves from now on to objective φ in Oφ.

For convenience, we use the usual abbreviations ̸=, ∧, ∀, ⊃, and ≡, and we sometimes omit brackets to ease readability.

Some differences between our language and traditional firstorder languages are apparent: our language features no predicates; functions cannot be nested; only the left-hand side of a literal may be a function. These restrictions will prove helpful for the implementation of a reasoning system. We remark that none of these restrictions means a limitation of expressivity: a predicate P(t1, . . . , tj) can be simulated by a literal p(t1, . . . , tj) = ⊤ where ⊤ is some standard name chosen to represent truth, and nested functions and literals with a function on the right-hand side can be flattened by introducing a new variable - these transformations preserve equivalence.

As an example, we formalise the introductory statement about Sally's father, who is rich but unknown to the agent:

where Sally is a standard name of the same sort (say, 'human') as x and fatherOf, and ⊤ is a name of the same sort (say, 'Boolean') as rich. Quantifying x into the modal context M expresses that the father's identity is unknown. The next subsection gives a semantic justification to this interpretation.

2.2 The Semantics

The semantics is based on possible worlds. We call a term f(t1, . . . , tj) primitive when all ti are standard names. Let N and T be the sets of all names and primitive terms, respectively. To denote the names or primitive terms that occur in a formula α, we write N(α) and T (α), respectively, and analogously for sets of formulas. To include only terms of the same sort as t, we write Nt and Tt. A world w : T → N is a sortpreserving mapping from primitive terms to standard names, that is, w(t) ∈ Nt for every primitive term t. A sentence is a formula without free variables. We denote by αx t the result of substituting t for all free occurrences of the variable x in α.

Truth of a sentence α is defined w.r.t. a world w and a set of possible worlds e as follows:

1. e,w |= t =n iff
2. t and n are identical names if t is a name;
3. w(t) and n are identical names otherwise;
4. e,w |= ¬α iff e,w ̸|= α;
5. e,w |= (α∨ β) iff e,w |= α or e,w |= β;
6. e, w |= ∃xα iff e, w |= αxn for some n ∈ Nx;
7. e,w |=Kα iff e,w′ |= α for all w′ ∈ e;
8. e,w |=Mα iff e,w′ |= α for some w′ ∈ e;
9. e,w |=Oφ iff e = {w′ | e,w′ |= φ}.

Unlike classical first-order logic, this semantics handles quantification by substitution of names. Standard names thus effectively serve as a fixed, countably infinite universe of discourse. See [Levesque, 1984a] for a discussion why this is no effective limitation for our purposes.

Oφ maximises the set of possible worlds e such that Kφ still holds. Hence the agent knows φ, but considers possible everything else provided it is consistent with φ. In other words, everything that is not a consequence of φ is unknown, for its negation is consistent with φ and hence considered possible. Thus Oφ captures only φ and its consequences are known.

As usual, a sentence α entails another sentence β, written α |= β, when e,w |= α implies e,w |= β for all e,w. A sentence α is valid, written |= α, when e, w |= α for all e, w.

We omit a deeper analysis except to note that K is a K45 operator [Fagin et al., 1995] and the following equivalences:

Proposition 1

• (i) |=Kα ≡ ¬M¬α;
• (ii) |= ∀xKα ≡K∀xα and |=Kα∧Kβ ≡K(α∧ β);
• (iii) |= ∃xMα ≡M∃xα and |=Mα∨Mβ ≡M(α∨β);
• (iv) |=Oφ ⊃Kφ.

To familiarise ourselves with the logic, we show that the query formalised at the end of Section 2.1 is entailed by

where Frank and Fred are names of sort 'human.' Let φ denote the sentence within O. By Rule 7, e = {w | e,w |= φ} is the only set of worlds that satisfies Oφ, so proving the entailment reduces to model checking for e. By assumption, for every w ∈ e, w(fatherOf(Sally)) ∈ {Frank, Fred}. Suppose w(fatherOf(Sally)) = Frank; the case for Fred is analogous. By assumption, w(rich(Frank)) = ⊤, so it only remains to be shown that e, w |= MfatherOf(Sally) ̸= Frank, which holds because there are w′ ∈ e with w′ (fatherOf(Sally)) = Fred.

3 A Logic of Limited Belief

We now introduce the logic LL, the limited counterpart of L.

3.1 The Language

The language of LL follows the rules from L with the following modifications: the expressions Kα and Mα are replaced with Kkα and Mkα where k ≥ 0 is a natural number, and the expression Gα is added to the language. We read Kkα and Mkα as "α is believed at level k" and "α is considered possible at level k," respectively, and the new expression Gα intuitively means "assuming the knowledge base is consistent, α is true." Guaranteeing consistency is motivated by practical applications where it often may reduce the computational cost of reasoning.

3.2 The Semantics

In LL, sets of clauses take over from sets of possible worlds as the semantic primitive that models belief. Intuitively, these clauses will represent the agent's explicit knowledge, like fatherOf(Sally) = Frank ∨ fatherOf(Sally) = Fred and

∀x(fatherOf(Sally) ̸= x ∨ rich(x) = ⊤) in our running example. By means of case splitting and unit propagation then further inferences can be drawn from these clauses. Before we can formalise this, we need to introduce some terminology.

We call a literal ground when it contains no variables. Recall that a primitive term is one of the form f(n1, . . . , nj) where the ni are names. Therefore every ground literal is of form n=n′ or n ̸=n′ or f(n1, . . . , nj) =n or f(n1, . . . , nj) ̸=n for names ni, n, n′ .

A literal is valid when it is of the form t = t, or n ̸= n′ for distinct names n, n′ , or t ̸= t′ for terms t, t′ of distinct sorts. A literal ℓ1 subsumes a literal ℓ2 when ℓ1, ℓ2 are identical or ℓ1, ℓ2 are of the form t = n1 and t ̸= n2 for distinct names n1, n2. Two literals ℓ1, ℓ2 are complementary when ℓ1, ℓ2 are of the form t=t′ and t ̸=t′ (or vice versa), or ℓ1, ℓ2 are of the form t = n1 and t = n2 for distinct names n1, n2.

A clause is a finite set of literals. A clause with a single literal is a unit clause. We abuse notation and identify nonempty clauses {ℓ1, . . . , ℓj} with formulas (ℓ1 ∨ . . . ∨ ℓj). The above terminology for literals carries over to clauses as follows. A clause is valid when it contains a valid literal, or a literal t = t′ and its negation t ̸= t′ , or two literals t ̸= n1 and t ̸= n2 for distinct names n1, n2. A clause c1 subsumes a clause c2 if every literal ℓ1 ∈ c1 subsumes a literal ℓ2 ∈ c2. The unit propagation of a clause c with a literal ℓ is the clause obtained by removing from c all literals that are complementary to ℓ.

A setup is a set of ground clauses. We write UP(s) to denote the closure of s with all valid literals under unit propagation:

• if c ∈ s, then c ∈ UP(s);
• if ℓ is a valid literal, then ℓ ∈ UP(s);
• if c, ℓ ∈ UP(s) and c′ is the unit propagation of c with ℓ, then c′ ∈ UP(s).

We write UP + (s) to denote the result of adding to UP(s) all valid clauses and all clauses that are subsumed by some clause in UP(s). Similarly, UP - (s) shall denote the setup obtained by removing from UP(s) all valid clauses and all clauses subsumed by some other clause in UP(s).

Truth of a sentence α in LL, written s0, s, v |≈ α, is defined w.r.t. two setups s0, s and a set of unit clauses v. The purpose of having these three parameters is to deal with nested beliefs. For the objective part of the semantics, only s is relevant:

1. s0, s, v |≈ ℓ iff ℓ ∈ UP + (s) if ℓ is a literal;
2. s0, s, v |≈ (α∨ β) iff
3. (α∨ β) ∈ UP + (s) if (α ∨ β) is a clause;
4. s0, s, v |≈ α or s0, s, v |≈ β otherwise;
5. s0, s, v |≈ ¬(α∨β) iff s0, s, v |≈ ¬α and s0, s, v |≈ ¬β;
6. s0, s, v |≈ ∃xα iff s0, s, v |≈ αxn for some n ∈ Nx;
7. s0, s, v |≈ ¬∃xα iff s0, s, v |≈ ¬αxn for every n ∈ Nx;
8. s0, s, v |≈ ¬¬α iff s0, s, v |≈ α.

Note how negation is handled by rules for (t1 ̸= t2), ¬(α∨β), ¬∃xα, ¬¬α. A rule s0, s, v |≈ ¬α iff s0, s, v ̸|≈ α would be unsound, as LL is incomplete w.r.t. L (as we shall see).

We proceed with the semantics of Kkα. The idea is that k case splits can be made first, before α is evaluated. A case split means to select some term (say, fatherOf(Sally)) and branch (conjunctively) on the values it could take (namely all standard names of the right sort, such as Frank and Fred). To preserve soundness of introspection, the effect of case splits must not spread into nested beliefs. This is why we need to carefully manage three parameters s0, s, v. Intuitively, s0 is the "original" setup without split literals, and v "stores" the split literals. Once the number of case splits is exhausted, s0∪v takes the place of s, so that the objective subformulas of α are interpreted by s0 ∪ v, whereas the subjective subformulas of α are interpreted by s0 (plus future splits from the nested belief operators). We say a setup s is obviously inconsistent when UP(s) contains the empty clause. In this special case, which corresponds to the empty set of worlds in the possible-worlds semantics, everything is known. The semantics of knowledge formalises this idea as follows:

1. s0, s, v |≈K0α iff
2. s0 ∪ v is obviously inconsistent, or
3. s0, s0 ∪ v, ∅ |≈ α;
4. s0, s, v |≈Kk+1α iff

Similarly, the idea behindMkα is to fix the value of certain terms in order to show that the setup is consistent with α. Intuitively this means that we want to approximate a possible world, that is, an assignment of terms to names, that satisfies α. Often we want to fix not just a single term, but a series of terms with a common pattern, for instance, f(n) = n for all n. To this end, we say two literals ℓ1, ℓ2 are isomorphic when there is a bijection ∗ : N →N that swaps standard names in a sort-preserving way so that ℓ1 and ℓ∗2 are identical, and define v⊎sℓ1=v∪{ℓ2 | ℓ1, ℓ2 are isomorphic and ¬ℓ2 /∈UP + (s∪v)}. In English: v ⊎s ℓ1 adds to v every literal that is isomorphic to ℓ1 and not obviously inconsistent with the setup s ∪ v. Furthermore, we need to take care that after fixing these values the setup is not potentially inconsistent. We say a setup s is potentially inconsistent when it is obviously inconsistent or when the set {ℓ | ℓ ∈ c ∈ UP - (s)} of all literals in UP - (s) contains two complementary literals, or a literal t = n for n /∈ Nt, or all literals t ̸= n for n ∈ Nt for some primitive term t. Note that this consistency test is intentionally naive, for the complexity of Mkα shall be bounded by k alone. The semantics of the consistency operator is then:

1. s0, s, v |≈M0α iff
2. s0 ∪ v is not potentially inconsistent, and
3. s0, s0 ∪ v, ∅ |≈ α;
4. s0, s, v |≈Mk+1α iff

To capture that Oφ means that φ is all the agent knows, we need to minimise the setup (modulo unit propagation and subsumption), which corresponds to the maximisation of the set of possible worlds in L. We hence define:

Lastly, we define the semantics of the Gα operator, which represents a guarantee that s is consistent and therefore can reduce the size of s to clauses potentially relevant to α. We denote the grounding of α by gnd(α) = {βx1...xj n1...nj | ni ∈ Nxi } where β is the result of rectifying α and removing all quantifiers, and x1, . . . , xj are the free variables in β. Finally, s|T is the least set such that if c ∈ UP - (s) and c either mentions a term from T , is empty, or shares a term with another clause in s|T , then c ∈ s|T . Then Gα works as follows:

This completes the semantics. We write s0, s |≈ α to abbreviate s0, s, ∅ |≈ α. Note that for subjective formulas σ, s is irrelevant, so we may just write s0 |≈ σ. Analogous to |= in L, we overload |≈ for entailment and validity.

In this paper we are mostly concerned with reasoning tasks of the form Oφ |≈ σ where σ is a subjective query and φ is a knowledge base of a special form called proper + : φ is of the form ∧i ∀x1 . . . ∀xj ci for clauses ci.

Observe that a proper + KB directly corresponds to the setup gnd(φ) = ⋃i gnd(ci). Also note that while existential quantifiers are disallowed in proper + KBs, they can be simulated as usual by way of Skolemisation.

Reasoning in proper + KBs is sound in LL w.r.t. L, provided that the query does not mention belief modalities Kk ,Mk in a negated context. While the first-order case is incomplete, a restricted completeness result for the propositional case will be given below. We denote by σL the result of replacing in σ every Kk ,Mk with K,M. The soundness theorem follows:

Theorem 2 Let φ be proper + and σ be subjective, without O, G, and without negated Kk , Mk .

Then Oφ |≈ σ implies Oφ |= σL.

Negated beliefs break soundness because of their incompleteness. For example, Kk(t = n ∨ ¬¬t ̸= n) in general only holds for k ≥ 1. Hence ¬K0 (t = n ∨ ¬¬t ̸= n) comes out true, which is unsound w.r.t. L. As a consequence of this incompleteness, Kkα ≡ ¬Mk¬α is not a theorem in LL.

For propositional formulas, that is, formulas without quantifiers, high-enough belief levels are complete:

Theorem 3 Let φ, σ be propositional, φ be proper + , σ be subjective and without O,G. Let σk be like σ with every Kl ,Ml replaced with Kk,Mk .

Then Oφ |= σL implies that there is a k such that Oφ |≈ σk.

To conclude this section, let us revisit our running example. The KB is the same as in Section 2.2, and the modalities in the query are now indexed with belief levels:

By Rule 13, s0 = {fatherOf(Sally) = Frank ∨ fatherOf(Sally) =Fred, fatherOf(Sally) ̸= n ∨ rich(n) = ⊤ | n ∈ Nx} is the unique (modulo UP + ) setup that satisfies the KB. To prove the query, by applying Rule 8 we can split the term fatherOf(Sally). Consider s0 ∪ {fatherOf(Sally) = Frank}. By unit propagation we obtain rich(Frank) =⊤, so we can choose Frank for x in Rule 4, and all that remains to be shown is that s0 |≈M1fatherOf(Sally) ̸=Frank. This is done by assigning fatherOf(Sally) = Fred in Rule 11, and as the resulting setup s0 ∪ {fatherOf(Sally) = Fred} is not potentially inconsistent and subsumes fatherOf(Sally) ̸=Frank, the query holds. Returning to the splitting in Rule 8, the case s0 ∪ {fatherOf(Sally) = Fred} is analogous, and for all other n, the setups s0 ∪ {fatherOf(Sally) = n} are obviously inconsistent and therefore satisfy the query by Rule 7.

4 AReasoning System

We now proceed to describe a decision procedure for reasoning in proper + knowledge bases, and then discuss an implementation as well as experimental results.

4.1 Decidability

Reasoning in proper + knowledge bases is decidable in LL:

Theorem 4 Let φ be proper + , σ be subjective and without O. Then Oφ |≈ σ is decidable.

While space precludes a detailed treatment of the proof and decision procedure, we sketch the idea. For the rest of this section, we use Lk as a placeholder for Kk and Mk .

Let us first consider the case where σ is of the form Lkψ for objective ψ; we will turn to nested modalities later. As φ is proper + , gnd(φ) gives us the unique (modulo UP + ) setup that satisfies Oφ, so the reasoning task reduces to model checking of gnd(φ). An important characteristic of standard names is that, intuitively, a formula cannot distinguish the names it does not mention. As a consequence, we can limit the grounding gnd(φ) and quantification during the model checking to a finite number of names. For every variable x in φ or ψ, let px be the maximal number of variables occurring in any subformula of φ or ψ of the same sort as x. It is then sufficient for the grounding and for quantification of x to consider only the names Nx(φ) ∪ Nx(ψ) plus px + 1 additional new names. Given the finite grounding and quantification, splitting in Rules 8 and 11 can also be confined to finitely many literals.

That way, the rules of the semantics of LL can be reduced to only deal with finite structures, which immediately yields a decision procedure for Oφ |≈ Lkψ.

In the propositional case, this procedure is tractable:

Theorem 5 Let φ, ψ be propositional, φ be proper + , ψ be objective. Then Oφ |≈ Lkψ is decidable in O(2k (|φ|+|ψ|)k+2 ).

Now we turn to nested beliefs, which are handled using Levesque's representation theorem [Levesque, 1984a]. When ψ mentions a free variable x, the idea is to replace a nested belief Lkψ with all instances n for which Lkψxn holds. Given a proper + φ, a set of primitive terms T , and a formula Lkψ for objective ψ, we define RES[φ, T, Lkψ] as

• if ψ mentions a free variable x: ∨n∈Nx(φ)∪Nx(ψ) (x = n ∧ RES[φ, T , Lk ψxn ]) ∨ ( ∧n∈Nx(φ)∪Nx(ψ) x ̸= n ∧ RES[φ, T , Lk ψxˆn ] ˆnx ) where ˆn ∈ Nx \ (Nx(φ) ∪ Nx(ψ)) is a some new name;
• if ψ mentions no free variables: TRUE if gnd(φ)|T |≈ Lkψ, and ¬TRUE otherwise, where TRUE stands for ∃xx=x.

In our running example, RES[φ, T ,M1 fatherOf(Sally) ̸= x] is (x = Frank ∧ TRUE) ∨ (x = Fred ∧ TRUE) ∨ (x = Sally ∧ TRUE) ∨ (x ̸= Frank ∧ x ̸= Fred ∧ x ̸= Sally ∧ TRUE), which says that everybody is potentially not Sally's father.

The RES operator can now be applied recursively to eliminate nested beliefs from the inside to the outside. For proper + φ, a set of terms T , and α without O, we define

• ‖t = t′ ‖φ,T as t = t′ ;
• ‖¬α‖φ,T as ¬‖α‖φ,T ;
• ‖(α∨ β)‖φ,T as (‖α‖φ,T ∨ ‖β‖φ,T );
• ‖∃xα‖φ,T as ∃x‖α‖φ,T ;
• ‖Lkα‖φ,T as RES[φ, T,Lk‖α‖φ,T ];
• ‖Gα‖φ,T as ‖α‖φ,T∩T (gnd(α)).

Note that ‖ · ‖ works from the inside to the outside and always returns an objective formula. In our example, ‖K1 . . . ‖φ,T first determines RES[φ, T ,M1fatherOf(Sally) ̸= x], and then RES[φ, T , K1 ∃x(fatherOf(Sally) = x ∧ rich(x) = ⊤ ∧ RES[φ, T ,M1 fatherOf(Sally) ̸= x)]] evaluates to TRUE.

Levesque's representation theorem (transferred to LL) states that this reduction is correct:

Theorem 6 Let φ be proper + , σ be subjective and without O. Then Oφ |≈ σ iff |≈ ‖σ‖φ,T .

It follows that propositional reasoning is tractable:

Corollary 7 Let φ, σ be propositional, φ be proper + , σ be subjective, and k ≥ l for every Kl ,Ml in σ. Then Oφ |≈ σ is decidable in O(2k (|φ| + |σ|)k+3 ).

4.2 Implementation

The reasoning system LIMBO implements the decision procedure sketched in the previous subsection. LIMBO is written in C++ and available as open source. 3

Compared to literals in propositional logic, literals in our first-order language are relatively complex objects. As we want to adopt SAT solving technology, care was taken to keep literal objects lightweight and efficient. Firstly, for every term we create only a single full copy and from then on uniquely identify the term with a 30-bit pointer to this full copy. With this compact representation of terms, a literal fits into a 64-bit integer: 60 bits for the left- and right-hand terms, and one bit to encode whether the literal is negated. Two of the remaining bits are used to encode whether the terms are standard names, which allows us to implement the subsumption and complementarity tests for literals (as defined in Section 3.2) using just bitwise operations on the literals' 64-bit representation, without dereferencing the term pointers. An experiment showed this representation to be 24 times faster than a naive encoding.

Subsumption and complementarity tests for literals are mostly used in the context of setups for determining unit propagation and subsumption. To avoid unnecessary blowup, invalid literals in clauses as well as valid clauses in setups are not represented explicitly. To facilitate fast unit propagation and cheap backtracking during splitting, the setup data structure uses the watched-literals scheme [Gomes et al., 2008]. Other SAT technologies like backjumping or clause learning are not used at the current stage. The setup data structure also provides an operation to query the value of a primitive term, which is used to optimise subformulas of the form Kk t = x in queries.

3 Source code: www.github.com/schwering/limbo

When the KB is known to be consistent, the query may be wrapped in a G operator to allow the reasoner to remove irrelevant clauses and thus reduce the branching factor for splitting. With an inconsistent KB, G is not sound, though.

LIMBO also rewrites formulas, exploiting equivalences that hold in L but not in LL like Proposition 1 (ii-iii), and provides syntactic sugar for nested functions and the like.

4.3 Evaluation

Three sample applications were developed to evaluate the reasoning system. 4 For one thing, a textual user interface allows for specification of reasoning problems and has been used to model several small-scale examples, including this paper's running example, to test the system's full expressivity. In this section, however, we focus on the application of limited belief to the games of Sudoku and Minesweeper.

Sudoku is played on a 9×9 grid which is additionally divided into nine 3×3 blocks. The goal is to find a valuation of the cells such that every row, column, and 3×3 block contains every value [1, 9] exactly once. The difficulty depends on how many and which numbers are given as clues from the start.

In Minesweeper the goal is to explore a grid by uncovering all and only those cells that contain no mine. When such a safe cell is uncovered, the player learns howmany adjacent cells are safe, but when a mined cell is uncovered, the game is lost. The difficulty depends on the number of mines and grid size.

Both games were played by simple agents that use the reasoning system to represent and infer knowledge about the current game state. For Sudoku, we use a function value(x, y) ∈ [1, 9] and translate the game rules to constraints such as y1 = y2 ∨ value(x, y1) ̸= value(x, y2). For Minesweeper a Boolean function isMine(x, y) is used, and when a cell (x, y) is uncovered, clauses are added to represent the possible valuations of isMine(x ± 1, y ± 1). Both agents use iterative deepening to find their next move: first, they look for a cell

4 Demos: www.cse.unsw.edu.au/~cschwering/limbo

(x, y) for which value(x, y) or isMine(x, y) is known at belief level 0; if none exists, they repeat the same for belief level 1; and so on, until a specified maximum level is reached. Once a known cell is found, the corresponding information is added to the knowledge base. In the case of Minesweeper, it is sometimes necessary to guess; we then use a naive strategy that prefers cells that are not next to an uncovered field.

While both games do not require much expressivity to be modelled, they are nevertheless interesting applications of limited belief because they are known to be computationally hard - Sudoku on N×N grids is NP-complete [Takayuki and Takahiro, 2003], Minesweeper is co-NP-complete [Scott et al., 2011] - yet often easily solved by humans. According to the motivating hypothesis behind limited belief, a small belief level should often suffice to reach human-level performance. Indeed we find this hypothesis confirmed for both games. The results for Sudoku in Table 1 show that most 'easy' instances are solved just by unit propagation, and the number of necessary case splits increases for 'medium' and 'hard.' Significantly more effort is needed to solve games from the "Top 1465" list, a repository of extremely difficult Sudokus. For Minesweeper, Table 2 shows that strong results are achieved at level 1 already, and while belief level 2 increases the chance of winning by 0.5%, there is no improvement at level 3.

The experiments were conducted with custom implementations of both games, compiled with clang -O3, and run on an Intel Core i7-4600U CPU at 3.3GHz.

5 Conclusion

We developed a practical variant of Liu, Lakemeyer, and Levesque's [2004] theory of limited belief and introduced and evaluated LIMBO, a reasoning system that implements our logic. The system features a sorted first-order language of introspective belief with functions and equality; the complexity of reasoning is controlled through the number of case splits. The idea behind limited belief is that often a small number of case splits suffice to bring about useful reasoning results; this hypothesis was confirmed in our experimental evaluation.

A natural next step is to incorporate theories of action, belief change, and multiple agents, which could open up applications in epistemic planning and high-level robot control. Another task is to improve the runtime performance, perhaps using SAT technology like clause learning and backjumping.