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.

Bisimulation provides structural conditions to characterize indistinguishability between nodes on graph-like structures from an external observer. It is a fundamental notion used in many areas. However, many applications use graphs where nodes have data, and where observers can test for equality or inequality of data values (e.g., asking the attribute "name" of a node to be different from that of all its neighbors). The present work constitutes a first investigation of "data aware"' bisimulations on data graphs. We study the problem of computing such bisimulations, based on the observational indistinguishability for XPath — a language that extends modal logic with tests for data equality. We show that in general the problem is pspace-complete, but identify several restrictions that yield better complexity bounds (coNP, ptime) by controlling suitable parameters of the problem; namely, the amount of em non-locality allowed, and the class of models considered (graph, DAG, tree). In particular, this analysis yields a hierarchy of tractable fragments.

A principled way to study limited forms of reasoning for expressive knowledge bases is to specify the reasoning problem within a suitable logic of limited belief. Ideally such a logic comes equipped with a perspicuous semantics, which provides insights into the nature of the belief model and facilitates the study of the reasoning problem. While a number of such logics were proposed in the past, none of them is able to deal with function symbols except perhaps for the special case of logical constants. In this paper we propose a logic of limited belief with arbitrary function symbols. Among other things, we demonstrate that this form of limited belief has desirable properties such as eventual completeness for a large class of formulas and that it serves as a specification of a form of decidable reasoning for very expressive knowledge bases.

We study anti-unification for the description logic EL and introduce thenotion of least general generalisation, which generalises simultaneously leastcommon subsumer and concept matching. The idea of generalisation of twoconcepts is to detect maximal similarities between them, and to abstract overtheir differences uniformly. We demonstrate that a finite minimal complete setof generalisations for ELconcepts always exists and establish complexitybounds for computing them. Wepresent an anti-unification algorithm that computes generalisations with afixed skeleton, study its properties and report on preliminary experimental evaluation.

We review several different languages for collective decision making problems, in which agents express their judgments, opinions, or beliefs over elements of a logically structured domain. Several such languages have been proposed in the literature to compactly represent the questions on which the agents are asked to give their views. In particular, the framework of judgment aggregation allows agents to vote directly on complex, logically related formulas, whereas the setting of binary aggregation asks agents to vote on propositional variables, over which dependencies are expressed by means of an integrity constraint. We compare these two languages and some of their variants according to their relative succinctness and according to the computational complexity of aggregating several individual views expressed in such languages into a collective judgment. Our main finding is that the formula-based language of judgment aggregation is more succinct than the constraint-based language of binary aggregation. In many (but not all) practically relevant situations, this increase in succinctness does not entail an increase in complexity of the corresponding problem of computing the outcome of an aggregation rule.

Preference models lie at the core of the formalization for several related notions, such as non-monotonic reasoning,obligations, goals, beliefs, etc. Recently, the interest in integrating dynamic operators in the logics of belief, preference and obligation has gained momentum.This integration sheds light on similarities among several change operations traditionally studied independently of each other. While a prolific approach, important operations, such as the well-known contraction of beliefs or derogation of norms studied in the AGM tradition,have not received proper attention in this framework.In this work, we study codifications of contraction operations, stemming from the work on iterate dbelief change, in the logic of preferences, by means of both semantically defined operations and their counterpart in syntactical priority structures.

Lifting a recent proposal by Moreno-Centeno and Karp, we propose a general framework for so-called implicit hitting set algorithms for reasoning beyond NP. The framework is motivated by empirically successful specific instantiations of the approach---based on interactions between a Boolean satisfiability (SAT) solver and an integer programming (IP) solver---in the context of maximum satisfiability (MaxSAT). The framework opens up opportunities for developing implicit hitting set algorithms for various important reasoning problems in KR by implementing domain-specific reasoning modules with SAT and IP solvers. We detail instantiations of the framework for the minimum satisfiability problem---as a natural dual of MaxSAT---and, as a central KR problem, for propositional abduction, covering the second level of the polynomial hierarchy. We show empirically that an implementation of the instantiation for propositional abduction surpasses the efficiency of an approach based on encoding and solving propositional abduction instances as disjunctive logic programming under answer set semantics.We also study key properties of the general framework.

The ability to infer intentions, emotions, and other unobservable psychological states from people's behavior is a hallmark of human social cognition, and an essential capability for future Artificial Intelligence systems. The commonsense theories of psychology and sociology necessary for such inferences have been a focus of logic-based knowledge representation research, but have been difficult to employ in robust automated reasoning architectures. In this paper we model behavior interpretation as a process of logical abduction, where the reasoning task is to identify the most probable set of assumptions that logically entail the observable behavior of others, given commonsense theories of psychology and sociology. We evaluate our approach using Triangle-COPA, a benchmark suite of 100 challenge problems based on an early social psychology experiment by Fritz Heider and Marianne Simmel. Commonsense knowledge of actions, social relationships, intentions, and emotions are encoded as defeasible axioms in first-order logic. We identify sets of assumptions that logically entail observed behaviors by backchaining with these axioms to a given depth, and order these sets by their joint probability assuming conditional independence. Our approach solves almost all (91) of the 100 questions in Triangle-COPA, and demonstrates a promising approach to robust behavior interpretation that integrates both logical and probabilistic reasoning.

The Temporal Network with Uncertainty (TNU) modeling framework is used to represent temporal knowledge in presence of qualitative temporal uncertainty. Dynamic Controllability (DC) is the problem of deciding the existence of a strategy for scheduling the controllable time points of the network observing past happenings only. In this paper, we address the DC problem for a very general class of TNU, namely Disjunctive Temporal Network with Uncertainty. We make the following contributions. First, we define strategies in the form of an executable language; second, we propose the first decision procedure to check whether a given strategy is a solution for the DC problem; third we present an efficient algorithm for strategy synthesis based on techniques derived from Timed Games and Satisfiability Modulo Theory. The experimental evaluation shows that the approach is superior to the state-of-the-art.

Many papers describe the use of Fuzzy Cognitive Maps as a modeling/representation technique for real-life scenarios’ simulation or prediction. However, not many real software implementations are described neither found. In this proposal the authors describe a modeling and experimentation framework where realistic problems can be recreated using Fuzzy Cognitive Maps as a knowledge representation form. Design elements, and descriptions of the algorithms that have been incorporated into the software, and hybridized with Fuzzy Cognitive Maps, are presented in this paper. Case studies were conducted and are illustrated with the intention of demonstrating the success and practical value of the general approach together with the implementation tool.