We propose a declarative framework for representing and reasoning about truthfulness of agents using answer set programming. We show how statements by agents can be evaluated against a set of observations over time equipped with our knowledge about the actions of the agents and the normal behavior of agents. We illustrate the framework using examples and discuss possible extensions that need to be considered.

In many scenarios where the integration of information into a knowledge base (KB) leads to inconsistencies there is a need to change the KB minimally. In belief revision, relevance postulates meet the minimality requirement by restricting the elimination of KB elements to those that are relevant for the incoming information. This paper focuses on two minimality postulates in an ontology revision scenario in which conflicts are caused by ambiguous use of symbols: a relevance postulate and a generalized inclusion postulate which limits the creativity of the operators. Both postulates exploit the (satisfiably) equivalent representation of a first-order logic KB by its prime implicates, which, intuitively, represent the most atomic logical components of the KB. The paper shows that reinterpretation operators (which are ontology revision operators) fulfill both postulates.

The situation calculus has proved to be a very popular formalism for modeling and reasoning about dynamic systems. This otherwise elegant and refined language however lacks a natural way of dealing with "infinite future histories". To this end, in this paper we introduce a new sort ranging over infinite paths in the situation calculus and propose an axiomatization for infinite paths. We thus obtain a convenient way of specifying several kinds of notions that involve infinite futures such as temporal properties of non-terminating executions of agents or programs and mental attitudes such as desires and intentions. We prove the correctness of the axiomatization and show that our formalization has some intuitively desirable properties.

We study the logical properties of the (parametric) well-founded fixed point operation. We show that the operation satisfies several, but not all of the equational properties of fixed point operations described by the axioms of iteration theories.

Probabilistic logic programs without negation can have cycles (with a preference for false), but cannot represent all conditional distributions. Probabilistic logic programs with negation can represent arbitrary conditional probabilities, but with cycles they create logical inconsistencies. We show how allowing negative noise probabilities allows us to represent arbitrary conditional probabilities without negations. Noise probabilities for non-exclusive rules are difficult to interpret and unintuitive to manipulate; to alleviate this we define ``probability-strengths'' which provide an intuitive additive algebra for combining rules. For acyclic programs we prove what constraints on the strengths allow for proper distributions on the non-noise variables and allow for all non-extreme distributions to be represented. We show how arbitrary CPDs can be converted into this form in a canonical way. Furthermore, if a joint distribution can be compactly represented by a cyclic program with negations, we show how it can also be compactly represented with negative noise probabilities and no negations. This allows algorithms for exact inference that do not support negations to be applicable to probabilistic logic programs with negations.

We consider knowledge representation (KR) formalisms as collections of finite knowledge bases with a model-theoretic semantics. In this setting, we show that for every KR formalism there is a formalism that characterizes strong equivalence in the original formalism, that is unique up to isomorphism and that has a model theory similar to classical logic.

Agent supervision is a form of control/customization where a supervisor restricts the behavior of an agent to enforce certain requirements, while leaving the agent as much autonomy as possible. In this work, we investigate supervision of an agent that may acquire new knowledge about her environment during execution, for example, by sensing. Thus we consider an agent's online executions, where, as she executes the program, at each time point she must make decisions on what to do next based on what her current knowledge is. This is done in a setting based on the situation calculus and a variant of the ConGolog programming language. To reason about such agents, we first define a notion of online situation-determined agent which ensures that for any sequence of actions that the agent can perform online, the resulting agent configuration is unique. We then present our formalization of the online maximally permissive supervisor.

Model checking is one of the most powerful and widespread tools for system verification with applications in many areas of computer science and artificial intelligence. The large majority of model checkers deal with properties expressed in point-based temporal logics, such as LTL and CTL. However, there exist relevant properties of systems which are inherently interval-based. Model checking algorithms for interval temporal logics (ITLs) have recently been proposed to check interval properties of computations. As the model checking problem for full Halpern and Shoham's ITL (HS for short) turns out to be decidable, but computationally heavy, research has focused on its well-behaved fragments. In this paper, we provide an almost final picture of the computational complexity of model checking for HS fragments with modalities for (a subset of) Allen's relations meets , met by , starts , and ends .

In this paper we study verification of situation calculus action theories against first-order mu-calculus with quantification across situations. Specifically, we consider mu-La and mu-Lp, the two variants of mu-calculus introduced in the literature for verification of data-aware processes. The former requires that quantification ranges over objects in the current active domain, while the latter additionally requires that objects assigned to variables persist across situations. Each of these two logics has a distinct corresponding notion of bisimulation. In spite of the differences we show that the two notions of bisimulation collapse for dynamic systems that are generic, which include all those systems specified through a situation calculus action theory. Then, by exploiting this result, we show that for bounded situation calculus action theories, mu-La and mu-Lp have exactly the same expressive power. Finally, we prove decidability of verification of mu-La properties over bounded action theories, using finite faithful abstractions. Differently from the mu-Lp case, these abstractions must depend on the number of quantified variables in the mu-La formula.

We will explore the use of disjunctive causal rules for representing indeterminate causation. We provide first a logical formalization of such rules in the form of a disjunctive inference relation, and describe its logical semantics. Then we consider a nonmonotonic semantics for such rules, described in (Turner 1999). It will be shown, however, that, under this semantics, disjunctive causal rules admit a stronger logic in which these rules are reducible to ordinary, singular causal rules. This semantics also tends to give an exclusive interpretation of disjunctive causal effects, and so excludes some reasonable models in particular cases. To overcome these shortcomings, we will introduce an alternative nonmonotonic semantics for disjunctive causal rules, called a covering semantics, that permits an inclusive interpretation of indeterminate causal information. Still, it will be shown that even in this case there exists a systematic procedure, that we will call a normalization, that allows us to capture precisely the covering semantics using only singular causal rules. This normalization procedure can be viewed as a kind of nonmonotonic completion, and it generalizes established ways of representing indeterminate effects in current theories of action.