On Progression and Query Evaluation in First-Order Knowledge Bases with Function Symbols

Introduction

A fundamental problem in reasoning about action is projection, which is to determine if a formula holds after a number of named actions have occurred, given a logical axiomatization of how the world behaves. In the situation calculus [Reiter, 2001], a regression operator solves the problem by reducing entailments about the future to a query about the initial knowledge base (KB). However, it is generally agreed that the use of regression is only reasonable on a small number of actions. In a seminal paper, Lin and Reiter (LR) [1997] developed the theory of progression, where the idea is to update the initial KB. There are two clear advantages with progression: no duplication of effort is needed to answer multiple queries about the resulting state, and second, one imagines that an agent, during its idle time, can compute progression while doing other physical activities.

In practice, progression has three main computational requirements: the new KB must be efficiently computable, its size must at most be linear in the size of initial KB (to allow progression to iterate), and lastly, the query evaluation problemmust at least be decidable. Unfortunately, LR's definition comes at the cost of second-order (SO) sentences in the progressed KB. And even if it is first-order (FO), the new theory may be an infinite one. Recently, Liu and Lakemeyer [2009] improve on earlier results and show that for a large class of action theories, called local-effect and normal actions, progression is FO definable and computable, but may lead to an exponential blow-up. Nevertheless, they also show that for certain kinds of FO disjunctive information, called proper+KBs, progression is efficiently computable. Briefly, since databases, which are equivalent (under certain assumptions) to a maximally consistent set of function-free ground literals, are too restrictive for KR purposes, proper+KBs were introduced [Lakemeyer and Levesque, 2002], which generalize databases and are equivalent to a (possibly) infinite set of consistent (not necessarily maximal) function-free ground clauses. For example, one can include things like Graduate(john) ∨ Graduate(mary) or ∀x.(Graduate(x) ⊃ Student(x)). So while the first two requirements of progression are accounted for (at least under some restrictions) the third, unfortunately, is not easy to satisfy. Unrestricted firstorder initial theories is clearly asking too much, but deductive reasoning with proper+KBs, which can be seen as a language restriction via syntactic normalization, remains undecidable.

There is a well-known tradeoff between the expressiveness of the representation language and its computational behavior. Over the decades, two main techniques have emerged. In the first, small domain FO theories are translated into propositional ones, often augmented with domain dependent information [Kautz and Selman, 1992]. In the second, FO features are not compromised but entailment is weakened, by way of non-traditional semantics e.g. [Liu et al., 2004] 1 . That said, both methods have limited appeal as they are function-free. This does not always coincide with practice, where in many standard applications such as moving robots [Levesque and Lakemeyer, 2001], game playing agents and planners [Reiter, 2001], functions are either essential or in the least allow for succinct representations. The apparent difficulty is that even simple clauses such as grade = 4 ∨ grade ̸= 2 result in non-trivial encodings: first, there is the semantic property that ground functions obtain unique values, and second, grade ̸= 2 says that there are an infinite number of possible values other than 2.

In this paper, we continue this line of research, where we investigate cases of progression that remain practical yet expressive. We extend proper+KBs to include functions, and show that progression wrt local-effect and normal actions is FO definable and efficiently computable. But they do not cover range-restricted actions [Vassos et al., 2009] which include non-local actions such as an exploding bomb that destroys everything in the vicinity. We obtain computability results for this class as well. Then for a large class of FO queries we provide a new methodology for sound and complete reasoning; one that is inspired by Boolean satisfiability.

1 Liu et al. propose a decidable but incomplete reasoning procedure for (function-free) proper+KBs. However, the conditions under which reasoning becomes complete is left open.

In the next section, we introduce the formalism, and then present results in the order indicated. For space reasons, the paper contains no proofs. They are presented in [Belle, 2011].

The Logic ESo

We consider a modal reconstruction of the situation calculus called ESo, with epistemic features, including onlyknowing [Levesque and Lakemeyer, 2001], which refers to all that an agent knows in the sense of having a KB. In recent work, Lakemeyer and Levesque [2009] show how the semantics below is fully compatible with LR's idea of progression. So what we obtain in this paper is a definition of FO progression in an epistemic setting with regards to actions with nontrivial sensing results, and where one can analyze beliefs and non-beliefs as valid sentences. 2 We review the main features:

1. Language: It includes fluent functions and rigid functions (for actions only) of every arity, 3 rigid SO functions of every arity, FO variables, SO function variables, distinguished fluents Poss and SF (for sensing), and closed under connectives: ∧, ¬, =, ∀, [t], ✷, B, O. 4 We assume there is a countably infinite set of object names N; e.g. obj5, desk. Let A be the (infinite) set {A(m1, . . . ,mk) | A is a rigid function, mj ∈ N}, and these denote action names; e.g. move(obj5, desk). N ∪A serves as the domain of discourse. 5 We also assume that variables come in both the object and the action sort.
2. Terms: Every FO variable and name is a term. We use t to denote a vector of terms, and tj to denote a term in t. If f is a function and R is a SO function variable, then f(t) and R(t) are terms. By primitive term and primitive SO term, we mean ones of the form f(m) and R(m) resp. , where mj ∈ N.
3. Formulas: Let t and t′ be terms. If α and β are formulas, then so are: t = t′ , α∧β, ¬α, ∀xα, ∀Rα, [t]α, Bα, Oα, ✷α. Primitive equalities are formulas of the form f(m) = n, where mj, n ∈ N. Fluent literals are of the form f(r) = s, where f is neither Poss nor SF, and rj and s are either variables or names. A clause is a disjunction of such literals. Fluent formulas are those that only mention fluent literals. 6

2 While our results also apply to the non-epistemic fragment, we believe the ability to deal with sensing is an important feature. See [Lakemeyer and Levesque, 2009] for examples.

3 Predicates are not included for simplicity, and can be thought of as special functions whose values are either (say) name 0 or name 1.

4 Symbols such as ∨, ∃, ≡ and ⊃ are understood as usual.

5 This allows a substitutional interpretation of quantifiers (respecting sorts).

6 Formulas with nested functions can be expressed wlog as a fluent formula. For instance, f(g(x)) = h(x) is written equivalently as ∃z, z′ f (z) = z′ ∧ g(x) = z ∧ h(x) = z′ .

We let Z denote all finite sequences of names in A, including 〈〉 i.e., empty sequence. We define worlds as functions from (fluent) primitive terms and Z to N, and from primitive SO terms to N. An epistemic state e ⊆ W is any set of worlds. While names act as rigid designators, the co-referring name for an arbitrary term is obtained wrt w and z ∈ Z as: (a) |t|zw = t if t ∈ N ∪A;

• (b) |A(t)|zw = A(m), where mj = |tj|zw and A is an action function;
• (c) |f(t)|zw = w[f(m), z], where f is a fluent, mj = |tj|zw ;
• (d) |R(t)|zw = w[R(m)], where mj = |tj |zw .

For sensing, we consider a relation w′ ≃z w s.t. w′ ≃〈〉 w for all w′ and w, and w′ ≃z·t w iff w′ ≃z w, w′ [Poss(t), z] = 1 and w′ [SF(t), z] = w[SF(t), z].

To interpret SO variables, we write w′ ∼R w to mean that w′ and w agree on everything except assignments involving R. Now, given e, w, z, a semantics is (connectives are understood as usual):

• e, w, z |= t1 = t2 iff n1 and n2 are identical, nj = |tj |zw ;
• e, w, z |= [t]α iff e, w, z · σ |= α, where σ = |t|zw ;
• e,w, z |= ✷α iff e,w, z · z′ |= α for all z′ ∈ Z;
• e,w, z |= ∀xα iff e,w, z |= αxn for every name n of the right sort;
• e, w, z |= ∀Rα iff e, w′ , z |= α for every w′ ∼R w;

A new feature of ESo is that belief is handled by progressing epistemic states wrt actions. That is, let wz be a world such that wz[p, z′ ] = w[p, z ·z′ ] for all primitive terms p and action sequences z′ . Further, let ewz = {w′z | w′ ∈ e and w′ ≃z w}.

• e,w, z |=Bα iff for all w′ ∈ ewz , ewz ,w′ , 〈〉 |= α;
• e,w, z |=Oα iff for all w′ , w′ ∈ ewz iff ewz ,w′ , 〈〉 |= α.

Models satisfy well-known introspective properties, i.e. that of weak S5 [Hughes and Cresswell, 1972; Lakemeyer and Levesque, 2009]. Given a set of sentences Σ, we write Σ |= α to mean that for every e, w, z if e, w, z |= α′ for all α′ ∈ Σ then e, w, z |= α. Finally, |= α denotes {} |= α.

The Computability of Progression

We begin by considering the equivalent of basic action theories (BATs) of the situation calculus [Reiter, 2001].

Definition 1: Given a set of fluents F, a set Σ ⊆ ESo is called the basic action theory over F iff Σ is the union of: 7

1. The initial theory Σ0 is any set of fluent sentences. Σpre is a sentence of the form ✷Poss(v) = 1 ≡ π and Σsense is a sentence of the form ✷SF(v) = y ≡ ψ, where π, ψ are fluent formulas and Poss represents a predicate.
2. Successor-state axioms (SSAs) Σpost is a set of sentences of the form ✷[v]f(x) = y ≡ γ ∗ f , where γ ∗ f = γf (x, y, v) ∨ f (x) = y ∧ ¬∃h γf (x, h, v) one for each fluent f and γf is a fluent formula.

Denote the initial theory as φ and the rest as ✷β. Hereafter, let t denote a name from A, say A(e). We remark that the unique name assumption for actions is built into the logic.

Lakemeyer and Levesque [2009] obtain a characterization of progression in the logic in terms of only-knowing:

7 Free variables are (implicitly) universally quantified.

Theorem 1: [Lakemeyer and Levesque, 2009] Let t be a standard action name, then

where, Ψ is the new initial theory defined as

We note that, different from LR, progression takes both the action executed (πv t ) and the sensing result (ψv t ) into account.

In the sequel, we are interested in efficient progression, and we realize this by restricting the initial theory to so-called proper+KBs (but appropriately generalized to functions) and considering certain classes of syntactically restricted BATs.

Proper+KBs

Let e denote Boolean combinations of formulas of the form r = s, where r and s are either variables or names, and d denote clauses. Let ∀α denote the universal closure of α. Moreover, we call a formula of the form ∀(e ⊃ d) a ∀-clause.

Definition 2: A proper+KB is any finite and satisfiable set of ∀-clauses.

Restrictions on BATs

Local-effects. Actions in many domains have local-effects in the sense that if a primitive action A(e) affects a fluent atom f(m), then m is contained in e. They generalize the strictly context-free class of BATs considered by LR [1997].

Definition 3: A SSA is local-effect if γf (x, y, v) is a disjunction of formulas of the form ∃u [v = A(z) ∧ μ(z)], where z contains x ∪ {y}, u are the remaining variables in z and μ(z) is the context formula.

Given a primitive action A(e), local-effect SSAs can be simplified. That is, it can be shown that γf(x, y,A(e)) is equivalent to disjunctions of the form x = m∧ y = n ∧ μ(e), where mj and n are names mentioned in e.

Normal Actions. Certain types of naturally occurring actions are not local-effect, e.g. moving a briefcase containing objects. Liu and Lakemeyer [2009] observe that these actions do not depend on the fluents on which they have non-local effects. That is, they have local-effects on all fluents mentioned in γf . For example, moving the briefcase also moves the contained objects without affecting the fluent in.

Definition 3 (cont.): A primitive action A(e) is said to have a local-effect on a fluent f if γf(x, y,A(e)) simplifies to a disjunction of formulas of the form x = m∧ y = n ∧ μ(e). Let LE(A) ⊆ F be the functions on which A(z) has localeffect. We call A(z) normal if for each f, all fluents appearing γf (x, y, v) are also in LE(A).

We consider another class of actions, called range-restricted theories, the treatment of which is deferred to later.

Example 1: To first illustrate the idea of a proper+KB, imagine the following incomplete facts about (stacks of) cards. We have cards 8 c1, c2, . . ., stacks s1, s2, . . . and ranks J,Q, . . . Each card has a rank and is associated with a value.

8 We assume that cards, ranks, values and stacks are names from N .

Now let φ1 be a proper+KB defined as a conjunction of rank(c1) = J (rank of c1 is J), rank(c2) = Q∨ rank(c2) ̸= K, in(c1) = s1 (c1 is inside the stack s1) and ∀.in(x) = s1 ⊃ value(x) = 5 (all cards in s1 are valued at 5).

To illustrate BATs, let Σ0 = {payoff = 0} ∪ φ1, Σpre = {✷Poss(v) = 1} (for simplicity), Σsense = {✷SF(readc1) = y ≡ value(c1) = y}. Consider SSAs:

That is, if the agent guesses the value of a card accurately, he receives a matching payoff. The agent may read card values (shown for c1) and move stacks between locations. (Note that the payoff SSA is local-effect and move is a normal action.)

In this paper, we show that under the reasonable assumption that BATs are quantifier free, the progression of a proper+KB wrt the defined classes of BATs is efficient.

Definition 4 : A BAT is quantifier free if πv t , ψv t and γf (x, y, v)vt can be simplified to quantifier free formulas.

For instance, Example 1 is clearly quantifier free.

We begin by extending the FO definability results in [Liu and Lakemeyer, 2009] to a language with function symbols. 9 First, we show that progression of local-effect SSAs is obtained by forgetting [Lin and Reiter, 1994] a finite set of primitive equalities. However, different from [Liu and Lakemeyer, 2009], and perhaps of independent technical interest, we will need to handle the modal operators appearing in the instantiated SSAs. In addition, progression will be characterized as what the agent comes to only-know after the action, as an extension to Theorem 1. We then discuss computational costs. For normal actions, Liu and Lakemeyer [2009] formalize progression as a special case of Ackermann's Lemma, which is a predicate elimination result [Doherty et al., 2001]. We obtain an analogous theorem for function symbols and discuss the complexity. Lastly, progression wrt range-restricted theories is also shown to be definable as forgetting a finite set of equalities. For reasons of space, we only go over the main aspects. See [Belle, 2011] for more details.

Forgetting

LR [1994] define a notion of forgetting from finite theories, which we adapt below for a language with functions. 10 Following their ideas, it can be shown that while forgetting primitive equalities is FO definable, forgetting functions is SO.

In what follows, let S denote a finite set of primitive equalities. We writeM(S) to mean the set of all truth assignments to S. Slightly abusing notation, given an equality ρ and function f , we write w′ ∼ρ w and w′ ∼f w to mean that w′ and w agree on everything initially, except maybe ρ and (resp.) the values for equalities mentioning f .

9 FO definability results for functional fluents are also mentioned (but not published) as an extension in [Liu and Lakemeyer, 2009]. Moreover, we differ in the ways discussed above.

10 While their definitions are given for standard first-order logic and Tarskian models, we consider analogous notions for the ESo semantical framework.

Definition 5: Let λ denote an equality or a function. Given a fluent formula φ, we say any fluent formula φ′ is the result of forgetting λ, denoted forget(φ, λ), if for any world w, w |= φ′ iff there is a w′ s.t. w′ |= φ and w ∼λ w′ . Inductively define forget(φ, {λ1, . . . , λk}) as forget(forget(φ, λ1), . . . , λk).

Definition 6: Suppose θ ∈M(S). Let φ[θ] denote replacing every occurrence of f(t) = t′ in φ with:

where, f(mj) = nj appears in S and is replaced by the truth assignment BOOLj according to θ. 11

Progression of Local-Effect Theories

We now turn to local-effects. Suppose that we have simplified γf (x, y, A(e)) to disjunctions of x = m∧ y = n ∧ μ(e) as discussed. Then define the argument set (wrt f) and characteristic set resp. as follows [Liu and Lakemeyer, 2009]:

Essentially, local-effects affect a finite number of primitive terms, which are those in Ω, conditioned on context formulas. Let us denote the instantiated SSAs ([v]f(x) = y ≡ γ ∗ f )vt as Fssa. So roughly speaking, progression is the addition of Fssa to the initial theory, while forgetting the initial values of all primitive terms specified in Ω.

However, as Fssa mentions modalities, we first convert it to a fluent formula. Let G be fresh functions s.t. gj has the same arity as fj . Now, let Fssa[G] denote (f(x) = y ≡ γ ∗ f FG)vt , that is, we use G to characterize formulas that hold initially.

Example 1 continued. If t denotes guess(c2, 3) then Fssa is {value(c2) = 3 ⊃ [t]payoff = 3, value(c2) ̸= 3 ⊃ [t]payoff = 0}. Thus, the progressed proper+KB φ′ is φ1 ∪ {payoff = y ≡ (value(c2) = 3 ∧ y = 3) ∨ y = 0}. Due to incomplete information O(φ′ ∧✷β) ̸|= ∃xBpayoff = x. 12

Note that Theorem 3 holds for any finite theory but it may not be efficient while the case of proper+KBs is very efficient.

Theorem 4: Forgetting an equality f(m) = n from a proper+KB φ takes O(h + (4w l)2 ) time, where h is the size of φ, l is the size of ∀-clauses in φ where f appears, and w is the maximum number of mentions of f in a ∀-clause in φ.

It is reasonable to assume that l, w and Ω are O(1). Then, progression is linear in the size of φ.

11 It is interesting to note, for example, that forgetting f = 1 from f = 4 is simply true, since f = 4 implies that f ̸= 1. That is, forgetting primitive equalities also results in forgetting primitive terms.

12 To see where only-knowing pays off, we can reduce formulas mentioning B to non-modal ones by means of the representation theorem [Levesque and Lakemeyer, 2001], which we do not go over for space reasons.

Progression of Normal Actions

When f ∈ LE(A) for a normal action A(z), then forgetting is as above. So what is really needed is a method of forgetting f ∈ F - LE(A).

A predicate elimination (i.e., forgetting) result by Ackermann [Doherty et al., 2001] states that given two formulas ∀.P(x) ⊃ α(x) and ∀.β(x), where α does not mention P and β only mentions P positively i.e. ¬P does not occur in the NNF of β, eliminating P from the conjunction is equivalent to βP(x) α(x) . An analogous result holds for functions:

Theorem 5: Let βi, αj and δ denote fluent formulas not mentioning f. Forgetting f from

That is, in any theory where the occurrence of f is semi-Horn [Doherty et al., 2001], i.e. either as β ⊃ f or f ⊃ α, forgetting the function is FO definable. Suppose that functions appear in a proper+KB in the semi-Horn form. Under the syntactic restrictions of normal actions, instantiated SSAs for f ∈ F - LE(A) can be simplified to the semi-Horn form. Therefore, forgetting f from the conjunction of the initial proper+KB and the instantiated SSA is FO definable. It can be shown that computing the result is linear in the size of theory. We skip the only-knowing theorem for space reasons.

Example 1 continued. Suppose stacks are located on desk1 or desk2 and let φ2 = {at(s1) = desk1} ∪φ1. Then, progression wrt move(s1, desk2) is φ1 with the following instantiated SSAs: { y = desk2 ∧ (x = s1 ∨ in(x) = s1) ⊃ [t]at(x) = y, y ̸= desk2 ∧ (x = s1 ∨ in(x) = s1) ⊃ ¬[t]at(x) = y }. Finally, replace all occurrences of [t]f(x) = y with f(x) = y.

Progression of Range-restricted Theories

Non-local actions such as an exploding bomb destroy everything in the vicinity, i.e., these actions do not specify the objects that they affect. Global effects such as these are believed to be one of the reasons why progression is SO. But when the range of nearby objects is restricted, Vassos et al. [2009] prove FO definability and computability results for certain types of initial theories which they refer to as a database of possible closures (DBPC). Roughly speaking, a DBPC corresponds to disjunctions of maximally consistent sets of literals.

To restrict the range of nearby objects, they consider SSAs where γf(x, y, v) is a disjunction of formulas of the form ∃u[v = A(z) ∧ μ(z,w)], where z contains y, u are the remaining variables in z but not in x, w are variables in x but not in z, and μ(z,w) is the context formula. 13 For every primitive action A(e), they further assume that the initial theory entails only a finite number of substitutions for the free variables w in the context formula μ(e,w). It then follows that only a finite set of fluent atoms are affected after doing an action. So progression can again be formulated in terms of forgetting.

However, the account in Vassos et al. is very involved because progression must be also definable as a DBPC (to allow for iterated progression). We improve on this by proving FO definability results for proper+KBs, which differs from their KBs in the sense that it can express notions like ∀.x ̸= c3 ⊃ st(x) ̸= broken which says that an infinite number of objects other than c3 are not broken (but leaving the status of c3 open). Second, the definition is a simple one via the concept of forgetting. Therefore, computability results from above are applicable.

13 Strictly speaking, Vassos et al. only consider predicates in their language. We present a functional fluent version of their notions in order to remain consistent with the rest of the paper.

We leave out the formal details, including the assumptions placed on context formulas, for space reasons (see [Belle, 2011]). We give an example instead:

Example 1 continued. Let φ3 = {∀.near(bomb, y) = 1 ≡

Then progression wrt explode is the removing of the ∀-clause mentioning st and the adding of {st(c1) = broken, st(c2) = broken, ∀.x ̸= c1 ∧ x ̸= c2 ∧ x ̸= c3 ⊃ st(x) ̸= broken}.

Theorem 6: Progression of a proper+KB wrt local-effect, normal and range-restricted theories is FO definable, efficiently computable (under discussed assumptions), and definable as a proper+KB.

Query Evaluation

The query evaluation procedure we have in mind is a logically sound and complete decision procedure for certain classes of queries on proper+KBs. To understand its basic principles, we begin with the (simpler) case where both the initial theory φ and query α are quantifier-free (QF) ground fluent formulas (i.e. no variables), and thus representable as ground clauses.

As hinted earlier, the computation mechanism is inspired by Boolean satisfiability where entailments are verified via refutation i.e. checking if S .= φ ∪ {¬α} is unsatisfiable. We essentially consider a variant of DPLL [Davis and Putnam, 1960], which first needs the notion of an assignment.

Definition 7: Let θ denote a consistent set of positive primitive equalities, and S is as above. Let [S]θ denote:

1. given f(m) = n ∈ θ, replace every occurrence of f(m) = n in S with true, and every occurrence of f(m) ̸= n or f(m) = n′ for some n′ ̸= n with false;
2. remove all clauses that contain at least one true literal, and delete all occurrences of false literals in clauses.

Intuitively, like partial assignments in Boolean reasoners [Gomes et al., 2008], [S]θ reduces S to a simpler formula which is satisfiable provided S ∧ θ is. The satisfiability procedure works as follows. It takes as input any set of ground clauses S and returns either SAT with a satisfying assignment θ i.e. one that makes [S]θ true, or with UNSAT.

A fundamental step in the classical DPLL is that of choosing a literal from the remaining clauses and considering partial assignments that either sets the literal to true everywhere, or sets it to false. In our case, the branches are possible assignments to primitive terms appearing in the remaining set of clauses. However, the universe is infinite, and so not all names can be considered. Instead, we show that it is sufficient to consider names in S, plus an (arbitrary) extra one.

Given a primitive term ρ, let H(S, ρ) be a set of names {n1, . . . , nk} s.t. ρ ◦ nj appears in S, where ◦ ∈ {=, ̸=}. If SAT is not returned for every assignment ρ = nj, then we consider ρ = n′ , for any n′ ∈ N - H(S, ρ). 14

Proposition 1: Let Θ denote the set {ρ = n1, . . . , ρ = nk, ρ = n′ } obtained as above. Then S is satisfiable iff ∨θ∈Θ[S]θ is satisfiable.

Easy arguments show that a DPLL proof has k+1 branches, in contrast to the binary tree in the Boolean case. Therefore, the worst-case complexity is O((k +1)q ), where q is the number of primitive terms in S and k is the size of H(S, ρ).

Theorem 7: Given any set of ground clauses S, S is unsatisfiable (satisfiable) iff DPLL(S, {}) returns UNSAT (SAT).

Algorithm 1: DPLL(S, θ)

Input: set of ground clauses S with θ = {} initially Output: UNSAT, or a set θ such that [S]θ is true (S, θ) .= UNIT-PROPOGATE(S, θ); if S contains false then return UNSAT; if S has no clauses left then output θ and return SAT; ρ .= any primitive term appearing in S and not mentioned in θ; foreach n ∈ H(S, ρ) do if DPLL([S]ρ=n, θ ∪ {ρ = n}) = SAT then return SAT; ret. DPLL([S]ρ=n′ , θ ∪ {ρ = n′ }) for any n′ ∈ N - H(S, ρ); where, UNIT-PROPOGATE(S, θ) is: while S does not contain false and has unit clause ρ = n do S .= [S]ρ = n and θ .= θ ∪ {ρ = n};

Beyond Ground Clauses. We extend the scope of the procedure to allow universally quantified queries wrt proper+KBs. We will need one reasonable assumption. But first, we prove a result about inferring the validity of a universal by means of a finite number of substitutions. Below, if H denotes a set of names, let H+b denote the union of H and b fresh names.

Theorem 8: Let φ be any set of closed fluent formulas s.t. there is an infinite number of names not appearing in φ. Let α be a fluent formula with a single free variable x and let H be the set of names mentioned in φ and α. Then, φ |= ∀xα iff φ |= αxm for all m ∈ H+1 .

Suppose φ is a proper+KB. The idea now will be to obtain a finite representation for gnd(φ) = {dxm | ∀(e ⊃ d) ∈ φ and |= exm}, which is the (possibly infinite) QF form of φ. We let gnd(φ)|H+b denote the restriction to names fromH+b .

Theorem 9: Let α be a closed QF fluent formula, φ be a proper+KB, and H be as above. Let φ also satisfy: for every primitive term f(m) with mj ∈ H, gnd(φ) mentions only finitely many inequalities of the form f(m) ̸= nj or gnd(φ)|H+1 entails ∨ f(m) = nj, where nj ∈ H. 15 Then, φ |= α iff gnd(φ)|H+1 |= α.

14 To see why the fresh name is needed, let φ be f (1) ̸= 1. Clearly, φ is satisfiable, but only for assignments to f(1) other than 1. Also, for functions representing relations, the procedure is modified to only consider 0 or 1 as possible assignments (see footnote 1).

Here, the "⇐" direction is immediate. Conversely, it is possible to show that any w that satisfies gnd(φ)|H+1 ∧ ¬α can be extended to a world that satisfies gnd(φ) ∧ ¬α which agrees with w on {f(m) | mj ∈ H+1 }. Now, by applying Theorem 8 and then Theorem 9, we are able to obtain:

Corollary 1: Let φ be a proper+KB (restricted as above), α be a QF fluent formula with a single free variable x and H is as above. Then φ |= ∀α iff gnd(φ)|C+ 1 |= αxm for all m ∈ C, where C = H+1 .

Example 2: (a.) If α and β denote ρ ̸= K and ρ = Q resp., α ̸|= ¬β since H(α ∧ β, ρ) = {K, Q}, [α ∧ β]ρ=Q = SAT. And since [α ∧ ¬β]ρ=n = SAT for any new name n, α ̸|= β.

(b.) Consider φ1 from Ex. 1 and let α = {in(c2) = s1}. To see how φ1 ̸|= α, let H+1 = {5, s1, c1, c2, J,Q,K, n} where n is new. Now consider δ = gnd(φ1)|H+1 ∧ ¬α. The only equality mentioning in(c2) in δ is ¬α. Since gnd(φ1)|H+1 is sat., let in(c2) = m, m ∈ N - {s1} and we obtain SAT.

(c.) Let α be in(x) = s1 ⊃ value(x) ̸= 4. Here, φ1 |= ∀α. To see this let C be H+1 from above. Then we obtain UNSAT with gnd(φ1)|C + 1 ∧¬(αxm) for all substitutions m ∈ C.

Conclusions

We have presented the following results. We consider the expressive proper+KBs, but this time extended to include functions. 16 With proper+KBs as initial theories, we show FO definability results for local-effect, normal and range-restricted theories. These cover all syntactically restricted action theories studied so far. Second, we prove efficient computability results for all three cases. Third, we consider the query evaluation problem, and show that despite the expressiveness, a sound and complete decision procedure exists for a large class of queries. The procedure shares structural properties with satisfiability solvers, and yet quantification is interpreted over an infinite universe. Given the success of Boolean reasoners, we believe these results show promise especially as far as progression is concerned in expressive settings. We remark that besides the LR definition, a number of alternate ones appears in the literature [Lakemeyer and Levesque, 2009].

While the chosen formalism in the paper is the situation calculus, we do believe our knowledge bases can be used with others. We think an important direction for future work lies in identifying classes of action theories for which the regressed formula [Reiter, 2001] remains in a form that is decidable.

As a concluding remark, reasoning about functions, equalities and constants is certainly not a new effort, and goes back to Ackermann [Badban et al., 2007]. Here too one finds variants of DPLL for certain QF fragments of FO logic, where often nesting of functions is allowed and the uniqueness of constants is not assumed. However, it is the latter property that allows us to handle quantifiers, both in the query and the KB, in a decidable manner. We believe the formalism provides a new insight in terms of finding satisfying assignments to ground functions. Nonetheless, it remains to be seen if it is the more practically viable option, and should be favored to say an encoding of the KB (plus, the uniqueness of names) input to the many solvers [Badban et al., 2007].

15 To see why such a restriction is needed, let φ = ∀.x ̸= n ⊃ f(n) ̸= x for some n. While φ entails f(n) = n, gnd(φ)|H+1 does not. If we add, say, f(n) = n ∨ f(n) = m to φ then gnd(φ)|H+1 does entail f(n) = n as required. However, if there are only finitely many inequalities, then they will also appear in gnd(φ)|H+1 .

16 Proper+KBs with functions are strictly more expressive. For instance, although formulas of the form ∀.x ̸= y ⊃ ¬P (x)∨¬P (y) simulate the uniqueness of function values, we can not capture the existence of values, i.e. ∃x.P(x), due to the infinite discourse.

Acknowledgements

We thank anonymous reviewers for helpful suggestions. The first author is supported by the B-IT Graduate School.