=Paper= {{Paper |id=Vol-2052/paper18 |storemode=property |title=Reasoning in the Situation Calculus with Limited Belief |pdfUrl=https://ceur-ws.org/Vol-2052/paper18.pdf |volume=Vol-2052 |authors=Christoph Schwering |dblpUrl=https://dblp.org/rec/conf/commonsense/Schwering17 }} ==Reasoning in the Situation Calculus with Limited Belief== https://ceur-ws.org/Vol-2052/paper18.pdf
                     Reasoning in the Situation Calculus with Limited Belief
                                       Extended Abstract
                                                Christoph Schwering
                                     School of Computer Science and Engineering
                                         The University of New South Wales
                                            Sydney NSW 2052, Australia
                                              c.schwering@unsw.edu.au

1   Introduction                                                       An epistemic state is not modelled as a set of possible
Action formalisms like the situation calculus [McCarthy, 1963;      worlds but as a set of ground clauses, that is, a set of disjunc-
Reiter, 2001] are powerful tools for modelling dynamic do-          tions of atomic formulas or their negation with an additional
mains. However, these formalisms, typically based on first-         sequence of actions. This set is not closed under full logi-
order logic, are also notorious for having little practical rele-   cal consequence but merely under unit propagation and sub-
vance due to their computational complexity.                        sumption. These clauses represent the agent’s explicit beliefs.
   This paper introduces an expressive yet computationally          Implicit beliefs are successively reached through case splits,
feasible variant of the situation calculus. To this end, we amal-   which means to select a term and branch on all its possible
gamate the situation calculus with a first-order logic of limited   values individually. The belief level determines the number
belief [Schwering, 2017]. Queries are evaluated at a specific       of allowed nested case splits. The complexity of reasoning
belief level, which intuitively limits the maximum allowed rea-     lies in finding the right terms to split and in the combinatorial
soning effort. Reasoning in this logic is sound and decidable.      explosion of nested splits at the higher belief levels.
An implementation has been made available.                             We restrict our attention to so-called proper+ knowledge
                                                                    bases, which are formulas in conjunctive normal form with-
                                                                    out existential quantifiers (existentials can be captured using
2   The Epistemic Situation Calculus                                Skolemization). We make no syntactic restrictions to the query.
The epistemic situation calculus [Lakemeyer and Levesque,              Reasoning about limited belief is sound with respect to its
2011] is a modal variant of Reiter’s situation calculus [2001].     unlimited ancestor with the possible-worlds semantics. In the
The language is a first-order logic with functions and equality     absence of quantifiers and at sufficiently high belief level, it is
and modal operators for knowledge and actions.                      complete as well. Moreover, reasoning is decidable, essentially
   The semantics is defined in terms of possible worlds. Ac-        because the number of individuals that need to be considered
tions can have two sorts of effects: physical or epistemic. A       for quantification is finite. An implementation of the reasoning
physical effect means that an action modifies the value of          system using the regression procedure is freely available.1
some function or predicate, whereas an epistemic effect pro-           The next steps are to further expand the system’s expres-
duces new knowledge through sensing, which is modelled by           sivity, improve runtime performance, and to evaluate it in
eliminating certain possible worlds.                                practical applications.
   The usual format of modelling a domain in the situation
calculus uses successor-state axioms, which relate the value        References
of a predicate or fluent after an action to what was true before.
                                                                    [Lakemeyer and Levesque, 2011] Gerhard Lakemeyer and
The fundamental task in the situation calculus is the projec-
tion problem, which refers to determining whether a certain            Hector J. Levesque. A semantic characterization of a useful
formula is true after a sequence of actions. The regression            fragment of the situation calculus with knowledge. Artifi-
procedure exploits the structure of successor-state axioms to          cial Intelligence, 175(1), 2011.
rewrite query formulas to eliminate the actions and thus reduce     [McCarthy, 1963] John McCarthy. Situations, actions, and
projection to ordinary static reasoning.                               causal laws. Technical report, Stanford University, 1963.
                                                                    [Reiter, 2001] Ray Reiter. Knowledge in Action: Logical
3   The Limited Epistemic Situation Calculus                          Foundations for Specifying and Implementing Dynamical
The limited epistemic situation calculus amalgamates the epis-         Systems. The MIT Press, 2001.
temic situation calculus [Lakemeyer and Levesque, 2011] with        [Schwering, 2017] Christoph Schwering. A reasoning system
a logic of limited belief which stratifies beliefs into levels,        for a first-order logic of limited belief. In Proceedings of the
starting with the explicit beliefs at level 0 and continuing the      Twenty-Sixth International Joint Conference on Artificial
implicit beliefs at levels > 0. The language is adopted from           Intelligence, 2017.
the (unlimited) epistemic situation calculus, except that knowl-
                                                                       1
edge operators are parameterised with a belief level.                      www.github.com/schwering/limbo