We propose a theory for reasoning about actions based on order-sorted predicate
logic where one can consider an elaborate taxonomy of objects. We are
interested in the projection problem: whether a statement is true after
executing a sequence of actions. To solve it we design a regression operator that takes advantage of
well-sorted unification between terms. We show that answering projection queries in
our logical theories is sound and complete with respect to that of in Reiter’s basic action
theories. Moreover, we demonstrate that our regression operator
based on order-sorted logic can provide significant computational
advantages in comparison to Reiter’s regression operator.
My research focuses on advanced reasoning about dynamical systems. We propose a modified fragment of the situation calculus that can assure decidable reasoning and has potential applications to Semantic Web services. Recently, we also develop a framework to handle large taxonomies of actions compactly, which allow us to gain computational advantages. Now, we consider another improvement to the situation calculus using order-sorted logic. In the future, we will further consider their possible applications to other AI research areas.
We design a
representation based on the situation calculus to facilitate development,
maintenance and elaboration of very large taxonomies of actions. This
representation leads to more compact and modular basic action theories (BATs)
for reasoning about actions than currently possible. We compare our
representation with Reiter’s BATs and prove that our representation inherits
all useful properties of his BATs. Moreover, we show that our axioms can be
more succinct, but extended Reiter’s regression can still be used to solve the
projection problem (this is the problem of whether a given logical expression
will hold after executing a sequence of actions). We also show that our representation
has significant computational advantages. For taxonomies of actions that can be
represented as finitely branching trees, the regression operator can work
exponentially faster with our theories than it works with Reiter’s BATs.
Finally, we propose general guidelines on how a taxonomy of actions can be
constructed from the given set of effect axioms in a domain.
We consider a modified version of
the situation calculus built using a two-variable fragment of the first-order
logic extended with counting quantifiers. We mention several additional groups
of axioms that can be introduced to capture taxonomic reasoning. We show that
the regression operator in this framework can be defined similarly to
regression in the Reiter's version of the situation calculus. Using this new
regression operator, we show that the projection and executability problems are
decidable in the modified version even if an initial knowledge base is
incomplete and open. For an incomplete knowledge base and for context-dependent
actions, we consider a type of progression that is sound with respect to the
classical progression. We show that the new knowledge base resulting after our
progression is definable in our modified situation calculus if one allows
actions with local effects only. We mention possible applications to
formalization of Semantic Web services.
To reason about
properties of reactive programs, one may usually follow either an operational
or a deductive approach. In this paper, we propose representing the classical
model checking approach of Clarke and Emerson in the situation calculus. Doing
so, we propose an approach that merges the operational and the deductive
approaches into one single framework by translating Kripke models that
represent system specifications into theories formulated in the situation
calculus and by recasting CTL as a
sublanguage of the calculus.
In this paper,
we focus on the problem of modeling autonomous agents that perform similar
strategies repeatedly in the same local situations in a stochastic system. We
introduce the concept of macroaction into the situation calculus, extend the
basic action theories and the regression operator, and develop a knowledge base
for macro-actions so that the agent can remember certain details and later
“recall” them when the agent performs the macroactions in the same local
situations again, thereby saving computational time.