A major challenge of query language design is the combination of expressivity with effective static analyses such as query containment. In the setting of XML, documents are seen as finite trees, whose structure may additionally be constrained by type constraints such as those described by an XML schema. We consider the problem of query containment in the presence of type constraints for a class of regular path queries extended with counting and interleaving operators. The counting operator restricts the number of occurrences of children nodes satisfying a given logical property. The interleaving operator provides a succinct notation for describing the absence of order between nodes satisfying a logical property. We provide a logic-based framework supporting these operators, which can be used to solve common query reasoning problems such as satisfiability and containment of queries in exponential time.

Many AI applications are based on some underlying logic that tolerates inconsistent information in a non-trivial way. However, it is not always clear what should be the exact nature of such a logic, and how to choose one for a specific application. In this paper, we formulate a list of desirable properties of `ideal' logics for reasoning with inconsistency, identify a variety of logics that have these properties, and provide a systematic way of constructing, for every n>2, a family of such n-valued logics.

This paper proposes the integration of the resolution rule for Max-SAT with unsatisfiability-based Max-SAT solvers. First, we show that the resolution rule for Max-SAT can be safely applied as dictated by the resolution proof associated with an unsatisfiable core when such proof is read-once, that is, each clause is used at most once in the resolution process. Second, we study how this property can be integrated in an unsatisfiability-based solver. In particular, the resolution rule for Max-SAT is applied to read-once proofs or to read-once subparts of a general proof. Finally, we perform an empirical investigation on structured instances from recent Max-SAT evaluations. Preliminary results show that the use of read-once resolution substantially improves the performance of the solver.

The minimization problem for propositional formulas is an important optimization problem in the second level of the polynomial hierarchy. In general, the problem is Sigma-2-complete under Turing reductions, but restricted versions are tractable. We study the complexity of minimization for formulas in two established frameworks for restricted propositional logic: The Post framework allowing arbitrarily nested formulas over a set of Boolean connectors, and the constraint setting, allowing generalizations of CNF formulas. In the Post case, we obtain a dichotomy result: Minimization is solvable in polynomial time or coNP-hard. This result also applies to Boolean circuits. For CNF formulas, we obtain new minimization algorithms for a large class of formulas, and give strong evidence that we have covered all polynomial-time cases.

A systematic study on the abstract level is the first step towards algorithms that solve the problem. We show that different semantics of ability in ATL Ultimately, we show that what agents can achieve is more give rise to different validity sets. As a consequence, sensitive to the strategic model of an agent (and a precise notion different notions of ability induce different of achievement) than it was generally realized. No less strategic logics and different general properties importantly, our study reveals that some natural properties - of games. Moreover, the study can be seen as the usually taken for granted when reasoning about action - may first systematic step towards satisfiability-checking cease to be universally true if we change the strategic setting.

In a pursuit-evasion game, one or more pursuers aim to discover the existence of, and then capture, an evader. The paper studies pursuit-evasion games in which players may have incomplete information concerning the game state. A methodology is presented for the application of a model checker for the logic of knowledge and time to verify epistemic properties in such games. Experimental results are provided from a number of case studies that validate the feasibility of the approach.

Binary aggregation studies problems in which individuals express yes/no choices over a number of possibly correlated issues, and these individual choices need to be aggregated into a collective choice. We show how several classical frameworks of Social Choice Theory, particularly preference and judgment aggregation, can be viewed as binary aggregation problems by designing an appropriate set of integrity constraints for each specific setting. We explore the generality of this framework, showing that it makes available useful techniques both to prove theoretical results, such as a new impossibility theorem in preference aggregation, and to analyse practical problems, such as the characterisation of safe agendas in judgment aggregation in a syntactic way. The framework also allows us to formulate a general definition of paradox that is independent of the domain under consideration, which gives rise to the study of the class of aggregation procedures of generalised dictatorships.

Research in AI has built upon the tools and techniques of many different disciplines, including formal logic, probability theory, decision theory, management science, linguistics and philosophy. However, the application of these disciplines in AI has necessitated the development of many enhancements and extensions. Among the most powerful of these are the methods of computational logic. I will argue that computational logic, embedded in an agent cycle, combines and improves upon both traditional logic and classical decision theory. I will also argue that many of its methods can be used, not only in AI, but also in ordinary life, to help people improve their own human intelligence without the assistance of computers.

Constraint propagation is one of the basic forms of inference in many logic-based reasoning systems. In this paper, we investigate constraint propagation for first-order logic (FO), a suitable language to express a wide variety of constraints. We present an algorithm with polynomial-time data complexity for constraint propagation in the context of an FO theory and a finite structure. We show that constraint propagation in this manner can be represented by a datalog program and that the algorithm can be executed symbolically, i.e., independently of a structure. Next, we extend the algorithm to FO(ID), the extension of FO with inductive definitions. Finally, we discuss several applications.

We introduce an abductive method for a coherent integration of independent data-sources. The idea is to compute a list of data-facts that should be inserted to the amalgamated database or retracted from it in order to restore its consistency. This method is implemented by an abductive solver, called Asystem, that applies SLDNFA-resolution on a meta-theory that relates different, possibly contradicting, input databases. We also give a pure model-theoretic analysis of the possible ways to `recover' consistent data from an inconsistent database in terms of those models of the database that exhibit as minimal inconsistent information as reasonably possible. This allows us to characterize the `recovered databases' in terms of the `preferred' (i.e., most consistent) models of the theory. The outcome is an abductive-based application that is sound and complete with respect to a corresponding model-based, preferential semantics, and -- to the best of our knowledge -- is more expressive (thus more general) than any other implementation of coherent integration of databases.