Inconsistencies between different information sources may arise because of statements that are inaccurate, albeit not completely false. In such scenarios, the most natural way to restore consistency is often to interpret assertions in a more flexible way, i.e. to enlarge (or relax) their meaning. As this process inherently requires extra-logical information about the meaning of atoms, extensions of classical merging operators are needed. In this paper, we introduce syntactic merging operators, based on possibilistic logic, which employ background knowledge about the similarity of atomic propositions to appropriately relax propositional statements.

Dominance testing, the problem of determining whether an outcome is preferred over another, is of fundamental importance in many applications. Hence, there is a need for algorithms and tools for dominance testing. CP-nets and TCP-nets are some of the widely studied languages for representing and reasoning with preferences. We reduce dominance testing in TCP-nets to reachability analysis in a graph of outcomes. We provide an encoding of TCP-nets in the form of a Kripke structure for CTL. We show how to compute dominance using NuSMV, a model checker for CTL. We present results of experiments that demonstrate the feasibility of our approach to dominance testing.

Large scale ontology applications require efficient and robust description logic (DL) reasoning services. Expressive DLs usually have very high worst case complexity while tractable DLs are restricted in terms of expressive power. This brings a new challenge: can users use expressive DLs to build their ontologies and still enjoy the efficient services as in tractable languages. In this paper, we present a soundness preserving approximate reasoning framework for TBox reasoning in OWL2-DL. The ontologies are encoded into EL++ with additional data structures. A tractable algorithm is presented to classify such approximation by realizing more and more inference patterns. Preliminary evaluation shows that our approach can classify existing benchmarks in large scale efficiently with a high recall.

When merging belief sets from different agents, the result is normally a consistent belief set in which the inconsistency between the original sources is not represented. As probability theory is widely used to represent uncertainty, an interesting question therefore is whether it is possible to induce a probability distribution when merging belief sets. To this end, we first propose two approaches to inducing a probability distribution on a set of possible worlds, by extending the principle of indifference on possible worlds. We then study how the (in)dependence relations between atoms can influence the probability distribution. We also propose a set of properties to regulate the merging of belief sets when a probability distribution is output. Furthermore, our merging operators satisfy the well known Konieczny and Pino-Perez postulates if we use the set of possible worlds which have the maximal induced probability values. Our study shows that taking an induced probability distribution as a merging result can better reflect uncertainty and inconsistency among the original knowledge bases.

Topological relations between spatial objects are the most important kind of qualitative spatial information. Dozens of relation models have been proposed in the past two decades. These models usually make a small number of distinctions and therefore can only cope with spatial information at a fixed granularity of spatial knowledge. In this paper, we propose a topological relation model in which the topological relation between two convex plane regions can be uniquely represented as a circular string over the alphabet {u; v; x; y}. A linear algorithm is given to compute the topological relation between two convex polygons. The infinite relation calculus could be used in hierarchical spatial reasoning as well as in qualitative shape description.

We show how the situation calculus can be reformulated in terms of the first-order stable model semantics. A further transformation into answer set programs allows us to use an answer set solver to perform propositional reasoning about the situation calculus. We also provide an ASP style encoding method for Reiter's basic action theories, which tells us how the solution to the frame problem in ASP is related to the solution in the situation calculus.

In this paper, we review a series of agent behavior synthesis problems under full observability and nondeterminism (partial controllability), ranging from conditional planning, to recently introduced agent planning programs, and to sophisticated forms of agent behavior compositions, and show that all of them can be solved by model checking two-player game structures. These structures are akin to transition systems/Kripke structures, usually adopted in model checking, except that they distinguish (and hence allow to separately quantify) between the actions/moves of two antagonistic players. We show that using them we can implement solvers for several agent behavior synthesis problems.

The study of node-selection query languages for (finite) trees has been a major topic in the recent research on query lan- guages for Web documents. On one hand, there has been an extensive study of XPath and its various extensions. On the other hand, query languages based on classical logics, such as first-order logic (FO) or monadic second-order logic (MSO), have been considered. Results in this area typically relate an Xpath-based language to a classical logic. What has yet to emerge is an XPath-related language that is expressive as MSO, and at the same time enjoys the computational proper- ties of XPath, which are linear query evaluation and exponen- tial query-containment test. In this paper we propose μXPath, which is the alternation-free fragment of XPath extended with fixpoint operators. Using two-way alternating automata, we show that this language does combine desired expressiveness and computational properties, placing it as an attractive can- didate as the definite query language for trees.

We study methods to specify preferences among subsets of a set (a universe ). The methods we focus on are of two types. The first one assumes the universe comes with a preference relation on its elements and attempts to lift that relation to subsets of the universe. That approach has limited expressivity but results in orderings that capture interesting general preference principles. The second method consists of developing formalisms allowing the user to specify "atomic" improvements, and generating from them preferences on the powerset of the universe. We show that the particular formalism we propose is expressive enough to capture the lifted preference relations of the first approach, and generalizes propositional CP-nets. We discuss the importance of domain-independent methods for specifying preferences on sets for knowledge representation formalisms, selecting the formalism of argumentation frameworks as an illustrative example.

In this paper, we propose a translation from normal first-order logic programs under the answer set semantics to first-order theories on finite structures. Specifically, we introduce ordered completions which are modifications of Clark's completions with some extra predicates added to keep track of the derivation order, and show that on finite structures, classical models of the ordered-completion of a normal logic program correspond exactly to the answer sets (stable models) of the logic program.