Action formalisms like the situation calculus [McCarthy, 1963;Reiter, 2001] are powerful tools for modelling dynamic domains. However, these formalisms, typically based on firstorder logic, are also notorious for having little practical relevance due to their computational complexity.
This paper introduces an expressive yet computationally feasible variant of the situation calculus. To this end, we amalgamate the situation calculus with a first-order logic of limited belief [Schwering, 2017]. Queries are evaluated at a specific belief level, which intuitively limits the maximum allowed reasoning effort. Reasoning in this logic is sound and decidable. An implementation has been made available.
The epistemic situation calculus [Lakemeyer and Levesque, 2011] is a modal variant of Reiter's situation calculus [2001]. The language is a first-order logic with functions and equality and modal operators for knowledge and actions.
The semantics is defined in terms of possible worlds. Actions can have two sorts of effects: physical or epistemic. A physical effect means that an action modifies the value of some function or predicate, whereas an epistemic effect produces new knowledge through sensing, which is modelled by eliminating certain possible worlds.
The usual format of modelling a domain in the situation calculus uses successor-state axioms, which relate the value of a predicate or fluent after an action to what was true before. The fundamental task in the situation calculus is the projection problem, which refers to determining whether a certain formula is true after a sequence of actions. The regression procedure exploits the structure of successor-state axioms to rewrite query formulas to eliminate the actions and thus reduce projection to ordinary static reasoning.
The limited epistemic situation calculus amalgamates the epistemic situation calculus [Lakemeyer and Levesque, 2011] with a logic of limited belief which stratifies beliefs into levels, starting with the explicit beliefs at level 0 and continuing the implicit beliefs at levels > 0. The language is adopted from the (unlimited) epistemic situation calculus, except that knowledge operators are parameterised with a belief level.
An epistemic state is not modelled as a set of possible worlds but as a set of ground clauses, that is, a set of disjunctions of atomic formulas or their negation with an additional sequence of actions. This set is not closed under full logical consequence but merely under unit propagation and subsumption. These clauses represent the agent's explicit beliefs. Implicit beliefs are successively reached through case splits, which means to select a term and branch on all its possible values individually. The belief level determines the number of allowed nested case splits. The complexity of reasoning lies in finding the right terms to split and in the combinatorial explosion of nested splits at the higher belief levels.
We restrict our attention to so-called proper + knowledge bases, which are formulas in conjunctive normal form without existential quantifiers (existentials can be captured using Skolemization). We make no syntactic restrictions to the query.
Reasoning about limited belief is sound with respect to its unlimited ancestor with the possible-worlds semantics. In the absence of quantifiers and at sufficiently high belief level, it is complete as well. Moreover, reasoning is decidable, essentially because the number of individuals that need to be considered for quantification is finite. An implementation of the reasoning system using the regression procedure is freely available. 1The next steps are to further expand the system's expressivity, improve runtime performance, and to evaluate it in practical applications.