First-Order Logical Filtering

1 Introduction

Many everyday scenarios are dynamic and partially observable: a robot in one room cannot see the state of another room, a camera overlooking a bookshelf cannot detect the title of a book that is obscured, and one cannot readily observe the amount of money an agent has. Many applications in such domains compute information about the current world state (belief state, i.e., set of possible states or a distribution over such a set) after actions and observations. This computation is called filtering (also, state estimation, belief update, and database progression). They use this information to make decisions, answer questions, and explore.

Filtering is intractable in general for discrete domains [Eiter and Gottlob, 1992], and much research is dedicated to its approximation in stochastic domains (e.g., [Boyen and Koller, 1998]). Still, these approximations introduce unbounded errors many times, take unbounded computation time in others, and are not usable in most deterministic domains. Recent progress on logical methods for filtering of propositional belief states (sets of states) [Amir and Russell, 2003] with actions and observations has shown that exact filtering is tractable when belief states are represented as propositional formulae, and certain natural assumptions are met. Still, many domains have propositional encodings that are too large or are not possible (e.g., large numbers of objects, unknown number of objects, and observations with partial knowledge about identity of objects).

In this paper we present tractable algorithms and theoretical results for updating belief states that are represented in First-Order Logic (FOL). These representations permit belief states of infinite sizes, uncertainty about the number of objects and their identity, and observations that do not distinguish between some objects. It also enables more compact representations than those of propositional logic.

We show that when actions map states 1:1, then we can update FOL belief-state formulae efficiently (linear time in the representation size), after prior compilation. We also show that the representation remains of bounded polynomial size for two classes of actions, including those for which actions have simple case preconditions and actions with STRIPS-like preconditions (non-conditional, and observed success/failure). For those we also present filtering algorithms that do not require precompilation for efficient update. This is in surprising contrast to the common belief that FOL cannot be used efficiently for representing and updating partial knowledge [Winslett, 1990; Lin and Reiter, 1997].

On the way to these contributions we form the foundations and provide a theory for FOL belief update. We relate deterministic Situation Calculus [Reiter, 2001] with a first-order transition model [Blass and Gurevich, 2000]. There, every belief state is a set of FOL models over the FOL language of a state. We show that filtering such belief states can be captured exactly by deduction in FOL, if the result of the filtering is definable in FOL (this is the best we can hope for [Lin and Reiter, 1997]). Also, we show that deduction can be carried out one time step at a time.

Most work related to ours is limited to the propositional case (e.g., [Amir and Russell, 2003; Boyen and Koller, 1998]). Important exceptions are [Cravo et al., 2001; Dixon and Wobcke, 1993] (First-Order AGM belief revision), [Winslett, 1990] (belief update and revision in simple subclasses of FOL), and [Lin and Reiter, 1997] (progression in Situation Calculus). The important difference that we draw with these works is that ours provides efficient inference procedures, while others focus on the use of general-purpose theorem provers, and intractability results.

2 Semantics of First-Order Filtering

In this section, we study logical filtering with first-order structures. A first-order language has as nonlogical symbols, the variables, the function symbols and the predicate symbols. A 0-ary function symbol is called constant. Note that among the binary predicate symbols must be the equality symbol =. We define the terms and formulas by the generalized inductive definition. Variables and functions are terms. Predicates are atomic formulas.

A first-order language is a language in which the symbols and formulas are as described above. We now turn to a description of the semantics of first-order languages. A structure S for a first-order language consists of:

1. |S|, the nonempty universe or domain of the structure S. The elements of |S| are called the individuals of S.
2. For each n-ary predicate symbol p, pS ⊆ |S|n. These tuples of the universe are those tuples on which p is true.
3. For each n-ary function symbol f, f S : |S|n → |S|. (In particular, for each constant e, eS is an individual of S)

When a sentence ψ is true in a structure S, we denote it by |=S ψ. For example, suppose that in structure S, |S| = {B, R}, for predicate in, inS = {〈B, R〉}, for constant CS-R, CS-RS = {R}, and for constant CS-B, CS-BS = {B}. This world has a CS room (CS-R), a CS book (CS-B), and a predicate in which indicates whether a book is in a room. By this definition, sentence in(CS-B, CS-R) is true in S.

We define logical filtering using situation calculus. The one that we use is compatible with the basic action theory of [Reiter, 2001]. The basic action theory has the formD = Σ ∪ Dss ∪ Dap ∪ Duna ∪ Ds0 where:

• Σ are the foundational axioms for situations.
• Dss is a set of successor state axioms.
• Dap is a set of action precondition axioms.
• Duna is a set of unique name axioms for actions. A(-→x ) ̸= A′ (-→y ) , A(-→x ) = A(-→y ) ⇒ -→x = -→y where A and A′ are action symbols.
• Ds0 (the initial database) is a finite set of first-order sentences that are uniform in s0

Definition 2.1 (Uniform Formula). A formula is uniform in s if s is the only term of sort situation mentioned by that formula.

We define precondition axioms and successor state axioms as a part of basic action theory as follows.

Definition 2.2 (Action Precondition Axioms). An action precondition axiom is a sentence of the form: 1

P oss(a(x1:n), s) ⇔ preconda(x1:n, s) where a is an n-ary action symbol, and preconda(x1:n, s) is a formula that is uniform in s and whose free variables are among x1, . . . , xn, s.

1x1:n is the abbreviation for x1, . . . , xn

Generally, the values of relations and functions in a dynamic world will vary from one situation to the next. Relations whose truth values vary from situation to situation are called relational fluents. They are denoted by predicate symbols taking a situation term as their last argument. Same argument is true about functions.

Definition 2.3 (Successor State Axioms). Successor state axioms is defined for either a relational fluent or a functional fluent. A successor state axiom for an n-ary relational fluent p is a sentence of the form:

where a is an action symbol, and succp,a(x1:n, y1:m, s) is a formula that is uniform in s and whose free variables are among x1, . . . , xn, y1, . . . , ym, s. We define a successor state axiom for a functional fluent in a similar way.

All changes to the world are the result of named actions. An action may be parameterized. For example, move(b, r1, r2) stands for the action of moving object b from room r1 to room r2. The intended interpretation is that situations are finite sequences of actions, and do(a, s) denotes the sequence formed by adding action a to the sequences s. In other words, do(a, s) is the successor situation resulting from performing the action a. We use situation calculus as foundations and semantics. Later (section 3 onwards) we do not mention it because we always focus on belief states. However, it is used in the proofs of theorems and our results are applicable to it.

Example Consider a book keeper robot who lives in a world consisting of rooms. When the robot is in a room, it can make observations about the books in that room. It can move a book between rooms, it can return a book to the library from an arbitrary room or it can put a borrowed book in a room. So possible actions are move(b, r1, r2), return(b, r) or borrow(b, r). The actions which are executable in a world state can change the value of different predicates or functions. Predicates are room(r), book(b) or in(b, r). There are no functional fluents except constants.

We define a precondition axiom and a successor state axiom for action move and skip the others.

• Precondition Axiom: P oss(move(b, r1, r2), s) ⇔ book(b, s) ∧ room(r1, s) ∧ room(r2, s) ∧ in(b, r1, s)
• Successor State Axioms:

P oss(move(b, r1, r2), s) ⇒ ∀b′ , r′ (in(b′ , r′ , do(move(b, r1, r2), s)) ⇔ (((b′ = b) ∧ (r′ = r1)) ⇒ false ∧((b′ = b) ∧ (r′ = r2)) ⇒ true ∧(¬((b′ = b) ∧ (r′ = r1)) ∧¬((b′ = b) ∧ (r′ = r2))) ⇒ in(b′ , r′ , s)))

The definition of progression and filtering semantics are as follows.

Definition 2.4 (Transition Relation of Structures). For an action theory D and a structure S, we define a transition relation RD(S, a, S′ ) as follows.

We use [x/v] as a notion of substitution in which x is a vector of variables and v is a vector of variables and constants. [x/v] is a shorthand for [x1/v1, . . .] in which [x1/v1] means replacing all instances of symbol x1 by symbol v1.

Definition 2.5 (Logical Filtering Semantics). Let σ be a set of first-order structures. We refer to it as belief state. The filtering of a sequence of actions (ground or not) and observations 〈a1, o1, . . . , at, ot〉 is defined as follows (ǫ refers to the empty sequence).

1. Filter[ǫ](σ) = σ;
2. Filter[a](σ) = {S ′ | S ∈ σ, 〈S, ˆa, S′ 〉 ∈ RD, ˆa = a[x/v]}
3. Filter[o](σ) = {S ∈ σ | |=S o};

We call Step 2 progression with a and Step 3 filtering with o.

3 Filtering of FOL Formulae

In the above definition, filtering is applied to a set of firstorder structures. In this section we use FOL to represent belief states and we update this representation without explicit reference to the structures in a belief state.

3.1 FOL Theories and Belief States

A belief state formula is a first-order theory (possibly infinite) that represents belief state. A structure is in belief state if and only if it satisfies the belief state formula. The use of a theory instead of a formula is required because the set of first-order consequences of a first-order formula is infinite and may not be representable by a FOL formula.

For simplicity, we use the same logical connectives that we have for FOL formulas. The meaning of those connectives on first-order theories is as follows:

If ϕ, ψ are theories of infinite size, then

• ϕ ∧ ψ will mean ϕ ∪ ψ.
• ϕ ∨ ψ will mean {α ∨ β| α ∈ ϕ, β ∈ ψ} (similar to de-morgan law).
• Whenever applying negation (¬) we will assume that ϕ is a finite theory (thus, a logical formula)
• Same for ∃ (can replace ∃ with a new constant symbol)

Thus, in the rest of the paper, whenever we say "belief state formula", we refer to a FOL theory, unless sanctioned otherwise as above. From now on, we assume that our first-order language has no function symbols except constants.

3.2 Basic Algorithm

In this section, we show how we can progress an initial database represented by a logical formula after applying a single action or observation. The result of progression is a new database that progression algorithm can use afterwards.

We define a predicate corresponding to each relational fluent whose truth value does not depend on the situation. The snapshot of system at time t only shows the truth values of predicates. The truth values of predicates would change while moving from one situation to the next. We represent predicates with the same symbol as relational fluents but with different arity.

Suppose that P = {g1, . . . , gr} is the set of all constants and predicates. We define a new set of symbols P ′ = {g′1 , . . . , g′r } such that g′i (y1:n) = gi(y1:n)[P/P ′ ] where [P/P ′ ] is a shorthand for [g1/g′1 , ..., gr/g′r ]. We view P as the set of predicates in situation s, and P ′ as the set of predicates in situation do(a, s).

We filter a belief-state formula as follows. (We reuse Filter[·](·) for filtering a belief-state formula.) Let ψ be a belief state formula, a(u1:n) be a grounded action, Cn(Ψ) be the set of logical consequences of Ψ (i.e. formulae φ such that Ψ |= φ), and CnL(Ψ) be the set of logical consequences of Ψ in the language L. We write CnL(Ψ), when L is a set of symbols, to mean CnL(L) (Ψ).

When we filter with action a we assert implicitly that its precondition held in the last world state. If the action is not executable on the belief state, the new belief state would be false which indicates an empty set. We prove in the following theorem that this definition of filtering approximates the semantics of definition 2.5.

Theorem 3.1. Let ψ be a belief state formula and a be an action, then

[Lin and Reiter, 1997] showed that progression is not always first-order definable. However, they proved that progression always exists as a set of second order sentences for finite initial databases. Therefore, the two sides in theorem 3.1 are not equivalent since formula (1) is in FOL. In other words, FOL is not strong enough to model the progression of the initial database. However, the following corollary shows that the two sides of theorem 3.1 would be equal if the progression of a database is FOL definable.

Corollary 3.2. Let ψ be a first-order belief state formula. If FOL can represent the progression of ψ after performing action a, then

From this point, we assume that progression is first-order definable. Our basic algorithm computes F ilter[〈a1, o1, ..., at, ot〉](ψ) by iteratively applying filtering of a belief-state formula with an action and an observation. It sets ψ0 = ψ and ψi = Filter[oi](Filter[ai](ψi-1))

recursively for i > 0 using the equations defined above. This algorithm is correct, as shown by corollary 3.2. It can be implemented using a first-order consequence finder.

3.3 Sequences of Actions and Observations

This section shows that iterative applications of progression steps lose no information. Thus, we can throw away the previous database and start working with the new one after performing each action.

We break our action theory D into two parts, the initial database Ds0 and the rest Dg. Therefore, D = Dg ∪ Ds0 . Now we define the language of an action theory as follows.

Definition 3.3. The language of D, L(D), is a set of firstorder formulae whose predicate and function symbols occur in D.

For instance, if Ds0 = put(A,B) ∧ ∀x box(x), then put(A, A) and ∀x∃y put(x, y) are in L(Ds0 ) but box(A, B) is not.

In progression we assume that a ground action a is performed, and we are looking for a set of sentences Dsa that can serve as a new initial database (sa denotes the situation term do(a, s)). Unfortunately [Lin and Reiter, 1997] showed that Dsa is not always first-order definable.

We define Fsa as the set of first-order sentences uniform in sa entailed by D. If we use Fsa instead of Dsa , for every first-order sentence ψ about the future of sa, Fsa ∪Dg |= ψ iff D |= ψ. The following theorem states this result.

Note that the intersection of all consequences of the action theory with L(Dg ∪ {sa}) is uniform in sa.

Theorem 3.4. Let D0 be an action theory, and define D1,D2,D′2 as follows.

D1 = Cn(D0 ∪ {s1 = do(a1, s0)}) ∩L(Dg ∪ {s1}) D2 = Cn(D1 ∪ {s2 = do(a2, s1)}) ∩L(Dg ∪ {s2}) D′2 = Cn(D0 ∪ {s1 = do(a1, s0), s2 = do(a2, s1)}) ∩L(Dg ∪ {s2})

(a1 and a2 are two actions in D0, not necessarily different. s0, s1 and s2 do not occur in Dg.) Then , D2 = D′2 .

PROOF See section A.2

For instance in our book keeper example, if Ds0 is {book(B, s0), room(R, s0), in(B, R, s0)} and the first action is return(B, R), Ds1 would be {book(B, s1), room(R, s1), ¬in(B, R, s1)}.

4 Factored Inference

Several distribution properties hold for logical filtering. We can decompose the filtering of a formula ϕ along logical connectives ∧, ∨, ¬, ∀, ∃.

Theorem 4.1. Let a be an action, and let ϕ, ψ be first-order formulae. Then,

1. Filter[a](ϕ∨ψ) ≡ Filter[a](ϕ) ∨Filter[a](ψ) 2. |= Filter[a](ϕ∧ψ) ⇒Filter[a](ϕ) ∧Filter[a](ψ) 3. |= Filter[a](¬ϕ) ⇐¬Filter[a](ϕ)∧Filter[a](TRUE) 4. Filter[a](∃x ϕ(x)) ≡ ∃x Filter[a](ϕ(L))[L/x]

(L is a fresh constant symbol.) 3, 4 hold only when Filter[a](ϕ) is finite.

We can say something stronger for actions that act as permutations on the structures in which they are executable.

Definition 4.2 (Permuting Actions). Action a is permuting (1:1) if for every structure S ′ there is at most one S such that RD(S, a, S′ ).

Domains that only include permuting actions are called permutation domains.

Theorem4.3 (Distribution for PermutationDomains). Let a be a permuting action, and let ϕ, ψ be formulae. Then,

1. Filter[a](ϕ∨ψ) ≡ Filter[a](ϕ) ∨Filter[a](ψ) 2. Filter[a](ϕ∧ψ) ≡ Filter[a](ϕ) ∧Filter[a](ψ) 3. Filter[a](¬ϕ) ≡ ¬Filter[a](ϕ) ∧Filter[a](TRUE) 4. Filter[a](∃x ϕ(x)) ≡ ∃x Filter[a](ϕ(L))[L/x]

We can decompose every first-order formula into a set of single literals by using distribution properties proved above. For instance, ∀x (ϕ(x) ∧ ψ(x)) is equivalent to ∀x ϕ(x) ∧ ∀x ψ(x) so rule 2 can break it into two parts. Also ∀x ¬ϕ(x) is equivalent to ¬∃x ϕ(x) so rule 3 and rule 4 can be used, and ∀x (ϕ(x)∨ψ(x)) is equivalent to ¬∃x (¬ϕ(x)∧¬ψ(x)) so rule 3, rule 4, and rule 2 can be used.

In permutation domains, we decompose the formula down to a set of grounded first-order single literals, and for filtering a single literal we use formula (1).

Our factored filtering (FF) algorithm for permutation domains is presented in Figure 1. It relies on theorems 3.2, 4.1, and 4.3. The number of different grounded single literals would be finite, if the number of objects is finite. Therefore, we can calculate filtering of all single literals as a preprocessing step and retrieve it later in finite domains.

Note that the arguments of these literals are either the constants associated to existential quantifiers or the constants which are mentioned in the initial belief state, the set of axioms or the observations.

PROCEDURE FF(〈ai, oi〉0<i≤t ,ψ) ∀i, ai an action, oi an observation, ψ a belief-state formula. 1. if t = 0, return ψ. 2. return ot∧ FF-Step(at, precondat ∧ FF(〈ai , oi〉0<i≤(t-1) ,ψ)).

PROCEDURE FF-Step(a,ψ) a an action. ψ a belief-state formula.

1. if ψ is a single literal, then return Single-Literal-Filtering(a, ψ).
2. else, use distribution properties, call FF-Step recursively on sub-formulas of ψ.

Figure 1: Filtering of a FOL formula when all the actions are permuting actions.

Theorem 4.4. The algorithm FF is correct, and if the filtering of all single literals are given, the algorithm FF would run in time O(|preconda ∧ ψ|), where ψ is a belief state formula.

Our factored filtering algorithm uses consequence finding tools. Since it is part of preprocessing, it does not affect the runtime of the system. In open systems the time is different since new objects may be added during the operation of the system. In these systems filtering of new single literals should be computed while system is running.

5 Filtering Algorithms for Different Domains

Our naive filtering algorithm uses consequence finding tools which do not scale to large domains. The following theorem suggests a different reasoning procedure.

Theorem 5.1. Let a be an action, ψ be a belief state formula, and Φ(ϕ1:n) be a first-order logical formula whose atomic subformulas are among ϕ1, . . . , ϕn. Then,

In this formula, all possible Φs should be considered. In general, generating all Φs is impossible because there are infinitely many such Φs. In the following sections, we provide simpler closed-form solutions for two special cases of dynamic domains. These give rise to practical(polynomial) algorithms.

5.1 Unit-Case Successor State Axioms

By definition of successor state axioms, for every pair of actions and predicates exactly one successor state axiom is provided. The successor state axiom for action a and predicate pi can be rewritten as:

where caseji is of the form (yj1 = xj1 ) ∧ . . . ∧ (yjk = xjk ) (variable xj1 is an argument of action a and variable yj1 is an argument of predicate p) and each variable assignment satisfies at most one of the cases. A successor state axiom is called unit-case successor state axiom if it can be rewritten in a form where every φji (1 ≤ j ≤ li + 1) is a unit clause.

We break a unit-case successor state axiom into multiple instantiated axioms. Instantiated successor state axioms for predicate pi are:

• P oss(a(x1:n), s) ⇒ (pi(y1:m, do(a, s)) ⇔ φji )[yj i /xji ] for all 1 ≤ j ≤ li
• Poss(a(x1:n), s) ⇒ ∀y1:m (¬case1i ∧. . .∧¬caseli i ) ⇒ (pi(y1:m, do(a, s)) ⇔ φli+1)

[yj i /xji ] is the substitution corresponding to caseji (yj i and xji are sequences of variables). This process is called breaking into cases. Note that all instantiated successor state axioms are in the form Poss(a) ⇒ (condi ⇒ (pi ⇔ φi)) where in some of them condi is true (i is an enumeration of all instantiated successor state axioms of action a).

Figure 2 shows the unit-case filtering (UCFilter) algorithm. This algorithm is applicable on permutation domains whose successor state axioms are unit-case. The algorithm UCFilter is actually a way to compute every Φ(subsucc1a , . . . , subsuccka ) in formula (2). In permutation domains, the head of entailment in formula (2) is a single literal (action precondition can be considered as a conjunct to PROCEDURE UCFilter(〈ai, oi〉0<i≤t ,ψ)

∀i, ai an action, oi an observation, ψ a belief-state formula.

1. if t = 0, return ψ.
2. ψt-1 =UCFilter(〈ai, oi〉0<i≤(t-1) ,ψ).
3. return ot∧Filter-True(at) ∧UCStep(at, precondat ∧ψt-1).

PROCEDURE Filter-True(a)

a an action.

1. poss(a) ⇒ (condi ⇒ (pi ⇔ φi)) an instantiated successor state axiom (1 ≤ i ≤ k).
2. S = ∅
3. for all 1 ≤ i, j ≤ k,
4. (a) if φi = true, add casei ⇒ pi to S
5. (b) elseif φi = false, add casei ⇒¬pi to S
6. (c) elseif unifiable(φi, φj), add ((condi ∧ condj) ⇒ (pi ⇔ pj))mgu(φi,φj) to S

(d) elseif unifiable(φi, ¬φj), add

((condi ∧ condj) ⇒ (pi ⇔ ¬pj))mgu(φi,φj) to S

• (e) elseif φi = ∀x q(x), φj = q(t), add (condi ∧ condj) ⇒ (¬pi ∨ pj) to S
• (f) elseif φi = ∃x q(x), φj = q(t), add (condi ∧ condj) ⇒ (pi ∨ ¬pj) to S
• return ∧ϕ∈S ϕ.

PROCEDURE UCStep(a,ψ)

a an action. ψ a belief-state formula.

1. if ψ is a single literal, then
2. (a) poss(a) ⇒ (condi ⇒ (pi ⇔ φi)) an instantiated successor state axiom (1 ≤ i ≤ k).
3. (b) S = ∅
4. (c) for all 1 ≤ i ≤ k,
5. if unifiable(φi, ψ), add (casei ⇒ pi)mgu(φi,ψ) to S
6. elseif unifiable(φi, ¬ψ), add (casei ⇒¬pi)mgu(φi,ψ) to S
7. else, use distribution properties, call UCStep recursively on sub-formulae of ψ.
8. (d) return ∧ϕ∈S ϕ.

Figure 2: Unit-Case Filtering.

the belief state formula, and the distribution properties can be used). Consequently, Φ(subsucc1a , . . . , subsuccka ) is either equivalent to that literal or a tautology. A tautology is at most of size two when unit-case successor state axioms are used. Therefore, we can compute all desired Φs in a finite number of steps.

Theorem 5.2. Let k be the number of successor state axioms after breaking into cases, and ψ be the belief state formula. If each predicate has arity at most R, then algorithm UCFilter returns the filtering of ψ with action a in time O(R · k2 +R · k · |ψ ∧ preconda|). The length of new belief state formula is O(R · k2 + R · k · |ψ ∧ preconda|).

Corollary 5.3. Given a sequence of t actions and observations, algorithm UCFilter returns the filtering of ψ0 in time O(t2 · Rt · kt+1 + t · Rt · kt · |ψ0|). The length of belief state formula after t step is ψt = O(t · Rt · kt+1 +Rt · kt · |ψ0|). (If the length of all observations and preconditions of actions are negligible compared to the length of belief state formula)

5.2 STRIPS Domains

In STRIPS domains every action has no conditional effects. It means that the value of each predicate either changes to true, changes to false, or remains the same. STRIPS actions are not necessarily permuting. Consequently STRIPS successor state axioms can not be treated by algorithm UCFilter even though they are unit-case. Successor state axioms in STRIPS domains are of the form:

where φji (j ≤ li) is either true or false.

A STRIPS action affects some of the instantiated predicates and keeps the value of the others. We refer to the set of affected instantiated predicates as Eff(a).

where v is a sequence of variables and constant symbols.

The first-order STRIPS filtering (FOSF) algorithm is presented in figure 3. The belief state formula which is an input to this algorithm should be in the form ∃∗∀∗φ (EAFOL) (EAFOL is a first-order formula in which there is no existential quantifier inside a universal one). A clause in the clausal form of φ would be splitted into multiple instantiated clauses if one of its literals has some instances in Eff(a) and some out of Eff(a). This step is called splitting into pure literal clauses. We split every clause p(x) ∨ ϕ in which some instantiations of p(x) are affected and some are not, into:

where p(v1), . . . , p(vr) are in Eff(a). Note that we treat ((x ̸= v1 ∧ . . . ∧ x ̸= vr) ⇒ p(x)) as a single literal.

The new clausal form of φ is divided into two parts, clauses with no literal in Eff(a) and clauses that have at least one literal in Eff(a). The first part directly goes to the new belief state formula. The algorithm adds all the consequences of the second part in which no affected literals exist, to the new belief state formula. All literals in Eff(a) are also added to new belief state formula as their values can be determined unconditionally after applying the action.

Theorem 5.4. Given action a, observation o, and belief state formula ψ in EAFOL, algorithm FOSF returns the filtering of ψ with a and o in time O(R · |E| · min(( |E| 2 )2|Eff(a)| , |Eff(a)|2|E|·R ) + |ψ|) where E is the set of all clauses with any literal in Eff(a) after splitting into pure literal clauses and each clause has length at most R.

Theorem5.5. If ψ is in 2-FO-CNF 2 then the time complexity of FOSF after filtering one action is O(|Eff(a)| · |E|2 + |ψ|). The formula length is O(|Eff(a)| + |E|2 + |ψ|).

Extended Example

Consider our previous book-keeping robot. Suppose that we have two rooms, a CS room and an ECE room, and two books, PROCEDURE FOSF(〈ai, oi〉0<i≤t ,ψ)

2 A first-order formula is in k-FO-CNF if in clausal form the size of each clause is at most k.

∀i, ai an action, oi an observation and ψ a belief state formula. oi and ψ in EAFOL

1. if t = 0, return ψ.
2. returnMove-Quan a (ot∧ FO-STRIPS-Step(at, Move-Quan(precondat ∧ FOSF(〈ai , oi〉0<i≤(t-1) ,ψ))))

a Moves all the quantifiers to the front with fresh variable names

PROCEDURE FO-STRIPS-Step(a,ψ)

• a an action, ψ = ∃∗∀∗ ∧i ci a belief-state formula.
• if ψ = ∃x φ(x), return ∃x FO-STRIPS-Step(a,φ(L))[L/x] a

2. elseif ψ = ∀x φ(x), return ∀x FO-STRIPS-Step(a,φ(x))

1. else,
2. (a) ψ′ ← split every clause in ψ into pure literal clauses
3. (b) E ← all clauses in ψ′ with any literal in Eff(a)
4. (c) S ← all clauses in ψ′ with no literal in Eff(a)
5. (d) if E ̸= ∅ for all l ∈ Eff(a) E ← resolve-out(l, E)
6. (e) φ = ∧ci∈E∪S ci
7. (f) Eff+(a) ← literals affected to true
8. (g) Eff-(a) ← literals affected to false
9. (h) return φ∧ ∧p(v)∈Eff+(a) p(v) ∧ ∧p(v)∈Eff-(a) ¬p(v).

a L is a fresh constant that does not appear in the language

Figure 3: First-Order STRIPS Filtering.

a CS book and an ECE book, and our belief state formula is in(CS-B, CS-R) ∧ in(ECE-B, ECE-R). ECE department needs the CS book for a while, so the book keeper moves it to ECE room. The action is a = move(CS-B, CS-R, ECE-R). (This example has unit-case successor state axioms.)

First, we add precondition to belief state formula. The new belief state is in(CS-B, CS-R) ∧ in(ECE-B, ECE-R) ∧ book(CS-B) ∧ room(CS-R) ∧ room(ECE-R). We calculate the filtering of all the single literals of the belief state formula separately and compute the result by using distribution properties. What follows is the formula for one of these literals based on the algorithm presented before.

Now suppose that instead of applying an action we filter the belief state based on an observation. The robot enters the CS room and observes that there is only one book in the room. The perfect filtering algorithm guarantees that in such cases the book is the same book that the robot has put in the room before.

Assume that the belief state formula is in(CS-B, CS-R) ∧ in(ECE-B, ECE-R). The observation is ∀x in(x, CS-R) ⇒ x = TheBook. Filter[o](ψ) |= TheBook = CS-B, so we can replace every instance of TheBook in the new belief state formula by CS-B.

6 Conclusions

In this paper we presented semantics and methodology for filtering in domains that include many objects whose identity is not certain. We generalized this problem to filtering with FOL

formulae. We showed that this problem is solvable in polynomial time when actions map states 1:1, or the actions are STRIPS. We showed that 1:1 actions allow us to filter firstorder belief state formulae in linear time (in the size of representation), if we can perform a precompilation step. When actions are STRIPS or Unit-Case, we can filter these belief state formulae efficiently without precompilation. In some cases, we showed that the belief state formulae is guaranteed to remain compactly represented. Those cases permit filtering of actions and observations indefinitely in polynomial time (in the number of predicates and objects). As a result, we can use our algorithm for many interesting applications, such as semantic web, autonomous agents, robot motion control, and partial knowledge games.

7 Acknowledgements

We wish to thank Megan Nance for useful discussions on related topics. We also wish to acknowledge support from DAF Air Force Research Laboratory Award FA8750-04-20222 (DARPA REAL program).