Seeing, knowing, doing: some modal logics for Articial Intelligence

For instance in role playing video games, ennemies are agents who perceive some
part of the virtual world and who can attack or launch a sortilege. Here, we try
to give formal tools to model knowledge reasoning about the perception of their
environment and about actions based, on modal logic.
First, we give combine the standard epistemic modal logic S5n with perception
constructions of the form aBb (agent a sees agent b). We give a semantics in terms
of position and orientation of the agents in the space that can be a line (Lineland)
or a plane (Flatland). Concerning Lineland, we provide a complete axiomatization
and an optimal procedure for model-checking and satisability problem. Concern-
ing Flatland, we show that both model-checking and satisability problem are
decidable but the exact complexities and the axiomatization remain open prob-
lems. Thus, the logics of Lineland and Flatland are completely a new approach:
their syntax is epistemic but their semantics concern spatial reasoning.
Secondly, we study on the logic of agency see-to-it-that STIT. In classical
logics like Coalition Logic CL or Alternating-time Temporal Logic ATL the de
re and de dicto problem is dicult and technical whereas if we combine STIT-
operators with epistemic operators, we can solve it in a natural way. However
this strong expressivity has a prize: the general version of STIT is undecidable.
That is why we focus on some syntactic fragments of STIT: either we restrict
the allowed coalitions J in constructions [J]' or we restrict the nesting of modal
STIT-operators. We provide axiomatizations and complexity results.
Finally, we give avour to epistemic modal logic by adding STIT-operators.
The logic STIT is suitable to express counterfactual statements like agent a could
have choosen an action such that ' have been true. Thus we show how to model
counterfactual emotions like regret, rejoicing, disappointment and elation in this
framework.