Alternative Semantics for Normative Reasoning with an Application to Regret and Responsibility

We provide a fine-grained analysis of notions of regret and responsibility (such as agent-regret and individual responsibility) in terms of a language of multimodal logic. This language undergoes a detailed semantic analysis via two sorts of models: (i) relating models, which are equipped with a relation of propositional pertinence, and (ii) synonymy models, which are equipped with a relation of propositional synonymy. We specify a class of strictly relating models and show that each synonymy model can be transformed into an equivalent strictly relating model. Moreover, we define an axiomatic system that captures the notion of validity in the class of all strictly relating models.

Cut elimination for knowledge logic with interaction

In the article the multimodal logic Tn with central agent interaction axiom is analysed. The Hilbert type calculi is presented, then Gentzen type calculi with cut is derived and the proof of cutelimination theorem is outlined. The work shows that it is possible to construct a Gentzen type calculi without cut for this logic.

A flexible logic-based approach to closeness using order of magnitude qualitative reasoning

In this paper, we focus on a logical approach to the important notion of closeness, which has not received much attention in the literature. Our notion of closeness is based on the so-called proximity intervals, which will be used to decide the elements that are close to each other. Some of the intuitions of this definition are explained on the basis of examples. We prove the decidability of the recently introduced multimodal logic for closeness and, then, we show some capabilities of the logic with respect to expressivity in order to denote particular positions of the proximity intervals.

KSP: A Resolution-based Prover for Multimodal K, Abridged Report

In this paper, we briefly describe an implementation of a hyper-resolution-based calculus for the propositional basic multimodal logic, Kn. The prover, KSP, is designed to support experimentation with different combinations of refinements for its basic calculus. The prover allows for both local and global reasoning. We present an experimental evaluation that compares KSP with a range of existing reasoners for Kn.

On Action Theory Change

As historically acknowledged in the Reasoning about Actions and Change community, intuitiveness of a logical domain description cannot be fully automated. Moreover, like any other logical theory, action theories may also evolve, and thus knowledge engineers need revision methods to help in accommodating new incoming information about the behavior of actions in an adequate manner. The present work is about changing action domain descriptions in multimodal logic. Its contribution is threefold: first we revisit the semantics of action theory contraction proposed in previous work, giving more robust operators that express minimal change based on a notion of distance between Kripke-models. Second we give algorithms for syntactical action theory contraction and establish their correctness with respect to our semantics for those action theories that satisfy a principle of modularity investigated in previous work. Since modularity can be ensured for every action theory and, as we show here, needs to be computed at most once during the evolution of a domain description, it does not represent a limitation at all to the method here studied. Finally we state AGM-like postulates for action theory contraction and assess the behavior of our operators with respect to them. Moreover, we also address the revision counterpart of action theory change, showing that it benefits from our semantics for contraction.

TEAMLOG in action: A case study in teamwork

This article presents a case study of a theoretical multi-agent system designed to clean up ecological disasters. It focuses on the interactions within a heterogeneous team of agents, outlines their goals and plans, and establishes the necessary distribution of information and commitment throughout the team, including its sub-teams. These aspects of teamwork are presented in the TEAMLOG formalism [20], based on multimodal logic, in which collective informational and motivational attitudes are first-class citizens. Complex team attitudes are justified to be necessary in the course of teamwork. The article shows how to make a bridge between theoretical foundations of TEAMLOG and an application and illustrates how to tune TEAMLOG to the case study by establishing sufficient, but still minimal levels for the team attitudes.