KR 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. Logic programs with ordered disjunction (LPODs) \cite{Brewka02} generalize normal logic programs by combining alternative and ranked options in the heads of rules. It has been showed that LPODs are useful in a number of areas including Game Theory, policy languages, planning and argumentations. In this paper, we extend propositional LPODs to the first-order case, where a classical second-order formula is defined to represent the stable model semantics of the underlying first-order LPODs. We then develop a progression semantics that is equivalent to the stable model semantics but naturally reflects the reasoning procedure of LPODs. We show that under finite structures, every LPOD can be translated into a first-order sentence, which provides a basis for computing stable models of LPODs. We further study the complexity and expressiveness of LPODs and prove that almost positive LPODs precisely capture normal logic programs, which indicates that ordered disjunction itself and constraints are sufficient to represent negation as failure.

ABSTRACT. Extensional higher-order logic programming has been recently proposed as an interesting extension of classical logic programming. An important characteristic of the new paradigm is that it preserves all the well-known properties of traditional logic programming. In this paper we enhance extensional higher-order logic programming with constructive negation. We argue that the main ideas underlying constructive negation are quite close to the existing proof procedure for extensional higher-order logic programming and for this reason the two notions amalgamate quite conveniently. We demonstrate the soundness of the resulting proof procedure and describe an actual implementation of a language that embodies the above ideas. In this way we obtain the first (to our knowledge) higher-order logic programming language supporting constructive negation and offering a new style of programming that genuinely extends that of traditional logic programming.

ABSTRACT. In the past, there have several attempts to explain logic programming under the well-founded semantics as a logic of inductive definitions. A weakness in all is the absence of an obvious connection between how we understand various types of informal inductive definitions in mathematical texts and the complex mathematics of the well-founded semantics. In this paper, we close this gap and show in a more definitive way that indeed, the well-founded semantics is a formalization of the principle of inductive definition.

ABSTRACT. Input languages of answer set solvers are based on the mathematically simple concept of a stable model. But many useful constructs available in these languages, including local variables, conditional literals, and aggregates, cannot be easily explained in terms of stable models in the sense of the original definition of this concept and its straightforward generalizations. Manuals written by designers of answer set solvers usually explain such constructs using examples and informal comments that appeal to the user's intuition, without references to any precise semantics. We propose to approach the problem of defining the semantics of gringo programs by translating them into the language of infinitary propositional formulas. This semantics allows us to study equivalent transformations of gringo programs using natural deduction in infinitary propositional logic, so that the properties of these programs can be more precisely characterized. In this way, we aim to create a foundation on which important issues such as the correctness of gringo programs and optimization methods may be more formally studied.

ABSTRACT. This paper presents a meta-algorithm, based on the general recursive schema for argumentation semantics called SCC-Recursiveness, for the computation of preferred labellings. The idea is to recursively decompose a framework so as to compute semantics labellings on restricted sub-frameworks, in order to reduce the computational effort. The meta-algorithm can be instantiated with a specific "base algorithm", applied to the base case of the recursion, which can be obtained by generalizing existing algorithms in order to compute labellings in restricted sub-frameworks. We devise to this purpose a generalization of a SAT-based state-of-the art algorithm, and provide an empirical investigation to show the significant improvement of performances obtained by exploiting the SCC-recursive schema.

ABSTRACT. In this paper, we investigate the revision of argumentation systems à la Dung. We focus on revision as minimal change of the arguments status. Contrarily to most of the previous works on the topic, the addition of new arguments is not allowed in the revision process, so that the revised system has to be obtained by modifying the attack relation only. We introduce a language of revision formulae which is expressive enough for enabling the representation of complex conditions on the acceptability of arguments in the revised system. We show how AGM belief revision postulates can be translated to the case of argumentation systems. We provide a corresponding representation theorem in terms of minimal change of the arguments statuses. Several distance-based revision operators satisfying the postulates are also pointed out, along with some methods to build revised argumentation systems. We also discuss some computational aspects of those methods.

ABSTRACT. We provide a logical analysis of abstract argumentation frameworks and their dynamics. Following previous work, we express attack relation and argument status by means of propositional variables and define acceptability criteria by formulas of propositional logic. We here study the dynamics of argumentation frameworks in terms of basic operations on these propositional variables, viz. change of their truth values. We describe these operations in a uniform way within a well-known variant of Propositional Dynamic Logic PDL: the Dynamic Logic of Propositional Assignments, DL-PA. The atomic programs of DL-PA are assignments of propositional variables to truth values, and complex programs can be built by means of the connectives of sequential and nondeterministic composition and test. We start by showing that in DL-PA, the construction of extensions can be performed by a DL-PA program that is parametrized by the definition of acceptance. We then mainly focus on how the acceptance of one or more arguments can be enforced and show that this can be achieved by changing the truth values of the propositional variables describing the attack relation in a minimal way.

ABSTRACT. The study of extension-based semantics within the seminal abstract argumentation model of Dung has largely focused on definitional, algorithmic and complexity issues. In contrast, matters relating to comparisons of representational limits, in particular, the extent to which given collections of extensions are expressible within the formalism, have been under-developed. As such, little is known concerning conditions under which a candidate set of subsets of arguments are “realistic” in the sense that they correspond to the extensions of some argumentation framework AF for a semantics of interest. In this paper we present a formal basis for examining extension-based semantics in terms of the sets of extensions that these may express within a single AF. We provide a number of characterization theorems which guarantee the existence of AFs whose set of extensions satisfy specific conditions and derive preliminary complexity results for decision problems that require such characterizations.

ABSTRACT. Today's propositional satisfiability (SAT) solvers are extremely powerful and can be used as an efficient back-end for NP-complete problems. However, many fundamental problems in knowledge representation and reasoning are located at the second level of the Polynomial Hierarchy or even higher, and hence polynomial-time transformations to SAT are not possible, unless the hierarchy collapses. Recent research shows that in certain cases one can break through these complexity barriers by fixed-parameter tractable (fpt) reductions which exploit structural aspects of problem instances in terms of problem parameters.

In this paper we develop a general theoretical framework that supports the classification of parameterized problems on whether they admit such an fpt-reduction to SAT or not.

We instantiate our theory by classifying the complexities of several case study problems, with respect to various natural parameters. These case studies include the consistency problem for disjunctive answer set programming and a robust version of constraint satisfaction.

ABSTRACT. Knowledge compilation is a rewriting approach to propositional knowledge representation. The `knowledge base' is initially represented as a CNF for which many important types of queries are NP-complete to answer. Therefore, the CNF is compiled into another representation for which the minimal requirement is that the clause entailment query (can the given partial assignment be extended to a complete satisfying assignment?) can be answered in a polynomial time. Such transformation can result in exponential blow up of the representation size. A possible way to circumvent this issue is to identify a structural parameter of the input CNF such that the resulting transformation is exponential in this parameter and polynomial in the number of variables. A notable result in this direction is an $O(2^kn)$ upper bound on the size of Decomposable Negation Normal Form (DNNF) proposed by (Darwiche, JACM 2001), where $n$ is the number of variables of the given CNF and $k$ is the treewidth of its primal graph. Quite recently this upper bound has been shown to hold for Sentential Decision Diagrams (Darwiche, IJCAI2011), a subclass of DNNF that can be considered as a generalization of the famous Ordered Binary Decision Diagrams (OBDD) and shares with the OBDD the key nice features (e.g. poly-time equivalence testing). Under this parameterization, the best known upper bound for an OBDD is $O(n^k)$ (Ferrara, Pan, Vardi; LPAR2005). A natural question is whether a fixed parameter upper bound holds for OBDD.

In this paper we answer this question negatively. In particular, we demonstrate an infinite class of CNFs of the primal graph treewidth at most $k$ for which the OBDD size is at least $O(n^{k/4})/o(n)$ thus providing a separation from SDD and essentially matching the upper bound of Ferrara, Pan, and Vardi. We also establish a more optimistic version of the $O(n^k)$ upper bound for the OBDD showing that it in fact holds when $k$ is the treewidth of the incidence graph of the given CNF and thus applies for `sparse' CNFs with large clauses.

ABSTRACT. Abstract dialectical frameworks (ADFs) have recently been proposed as a versatile generalization of Dung's abstract argumentation frameworks (AFs). In this paper, we present a comprehensive analysis of the computational complexity of ADFs. Our results show that while ADFs are one level up in the polynomial hierarchy compared to AFs, there is a useful subclass of ADFs which is as complex as AFs while arguably offering more modeling capacities. As a technical vehicle, we employ the approximation fixpoint theory of Denecker, Marek and Truszczyński, thus showing that it is also a useful tool for complexity analysis of operator-based semantics.

ABSTRACT. First-order model counting recently emerged as a novel reasoning task, at the core of efficient algorithms for probabilistic logics. We present a Skolemization algorithm for model counting problems that eliminates existential quantifiers from a first-order logic theory without changing its weighted model count. For subsets of first-order logic, lifted model counters were shown to run in time polynomial in the number of objects in the domain of discourse, where propositional model counters require exponential time. However, these guarantees only apply to Skolem normal form theories, and the presence of existential quantifiers reduces lifted model counters to propositional ones. Since textbook Skolemization is not sound for model counting, these restrictions precluded efficient model counting for directed models such as probabilistic logic programs. Our Skolemization procedure extends the applicability of first-order model counters to these representations. Moreover, it simplifies the design of lifted model counting algorithms.

ABSTRACT. Belief merging aims at defining the beliefs of a group from the beliefs of each member of the group. It is related to more general notions of aggregation from economy (social choice theory). Two main subclasses of belief merging operators exist: majority operators which are related to utilitarianism, and arbitration operators which are related to egalitarianism. Though utilitarian (majority) operators have been extensively studied so far, there is much less work on egalitarian operators. In order to fill the gap, we investigate possible translations in a belief merging framework of some egalitarian properties and concepts coming from social choice theory, such as Sen-Hammond equity, Pigou-Dalton property, median, and Lorenz curves. We study how these properties interact with the standard rationality conditions considered in belief merging. Among other results, we show that the distance-based merging operators satisfying Sen-Hammond equity are mainly those for which leximax is used as the aggregation function.

ABSTRACT. The paper addresses how the information state of an agent relates to the arguments that the agent endorses. Information states are modeled in doxastic logic and arguments by recasting abstract argumentation theory in a modal logic format. The two perspectives are combined by an application of the theory of product logics, delivering sound and complete systems in which the interaction of arguments and beliefs is investigated.

ABSTRACT. We examine several belief change operations in the light of Dynamic Logic of Propositional Assignments DL-PA. We show that we can encode in a systematic way update operations (such as Winslett's `Possible Models Approach') and revision operations (such as Dalal's) as particular DL-PA programs. Every DL-PA formula being equivalent to a boolean formula, one obtains syntactical counterparts for all these belief change operations.

ABSTRACT. A strong intuition for AGM belief change operations, Gärdenfors suggests, is that formulas that are independent of a change should remain intact. Based on this intuition, Fariñas and Herzig axiomatize a dependence relation w.r.t. a belief set, and formalize the connection between dependence and belief change. In this paper, we introduce base dependence as a relation between formulas w.r.t. a belief base. After an axiomatization of base dependence, we formalize the connection between base dependence and a particular belief base change operation, saturated kernel contraction. Moreover, we prove that base dependence is a reversible generalization of Fariñas and Herzig’s dependence. That is, in the special case when the underlying belief base is deductively closed (i.e., it is a belief set), base dependence reduces to dependence. Finally, an intriguing feature of Fariñas and Herzig’s formalism is that it meets other criteria for dependence, namely, Keynes’ conjunction criterion for dependence (CCD) and Gärdenfors’ conjunction criterion for independence (CCI). We show that our base dependence formalism also meets these criteria. More interestingly, we offer a more specific criterion that implies both CCD and CCI, and show our base dependence formalism also meets this new criterion.

ABSTRACT. A central result in the AGM framework for belief revision is the construction of revision functions in terms of total preorders on possible worlds. These preorders encode comparative plausibility: r <= r' states that the world r is at least as plausible as r'. Indifference in plausibility, denoted r ~ r', is defined as r ~ r' iff r <= r' and r' <= r. Herein we take a closer look at plausibility indifference. We contend that the transitivity of indifference assumed in the AGM framework is not, in general, an intuitive property for comparative plausibility. Our argument originates from similar concerns in preference modelling, where a structure weaker than a total preorder, called a semiorder, is widely consider to be a more adequate model of preference. In this paper we essentially re-construct revision functions using semiorders instead of total preorders. We formulate postulate to characterise this new, wider, class of revision functions, and prove that the postulates are soundness and completeness with respect to the semiorders-based construction. Moreover, through the Levi and Harper Identities, we characterise axiomatically the corresponding class of contraction functions.

ABSTRACT. In the middle of the 1980s, David Poole introduced a semantical, model-theoretic notion of specificity to the artificial-intelligence community. Since then it has found further applications in non-monotonic reasoning, in particular in defeasible reasoning. Poole’s notion, however, turns out to be intricate and problematic, which — as we show — can be overcome to some extent by a closer approximation of the intuitive human concept of specificity. Besides the intuitive advantages of our novel specificity ordering over Poole’s specificity relation in the classical examples of the literature, we also report some hard mathematical facts: Contrary to what was claimed before, we show that Poole’s relation is not transitive. Our new notion of specificity is also monotonic w.r.t. conjunction.

ABSTRACT. We provide a sound and complete axiomatization for a class of logics appropriate for reasoning about the rationality of players in games. Essentially the same axiomatization applies to a wide class of decision rules.

ABSTRACT. We introduce dynamic causal calculus, a nonmonotonic formalism that can be viewed as a direct logical counterpart of the action description language C+ from \cite{GLMT01}. We formulate a nonmonotonic semantics of the associated causal language, and compare this semantics with the indirect, two-stage semantics for C+, given in \cite{GLMT01}. It will be shown, in particular, that the suggested semantics allows us to alleviate syntactic distinctions between propositional atoms, maintained by C+, as well as type restrictions imposed on its causal laws. We will describe also a logical formalism of dynamic causal inference that constitutes a complete description of the logic that is adequate for this dynamic calculus.

ABSTRACT. Causal models defined in terms structural equations have proved to be quite a powerful way of representing knowledge regarding causality. However, a number of authors have designed examples where it seems that the Halpern-Pearl (HP) definition of causality gives intuitively unreasonable answers. As has been pointed out by many authors, what gets counted as a cause is quite dependent on the choice of variables in the model. Here it is shown that in all the counterexamples suggested, there are two possible stories consistent with the counterexample, where intuitions regarding causality are quite different. By adding additional variables, we can disambiguate the stories; moreover, in the resulting causal models, the HP definition of causality gives the intuitively correct answer. The examples not only give insight into the modeling process, they also highlight some aspects of the definition of causality itself. Specifically, by extending one of the examples, it can be shown that a modification to the original HP definition made to deal with an example by Hopkins and Pearl may not be necessary. By extending another definition, a sequence of models can be constructed, each one a conservative extension of the one before, where the question of whether X=x is cause of Y=y alternates between being true and false.

ABSTRACT. We show that determining whether a Boolean game has an equilibrium that guarantees every player a given payoff is NEXP-hard. In the proof we encode a non-deterministic, exponential time Turing machine by having one player play a mixed strategy from which we can infer a computation history of the machine, and the other players verify that this history does in fact represent a valid, accepting run.

ABSTRACT. Two-way regular path queries (2RPQs) have received increased attention recently due to their ability to relate pairs of objects by flexibly navigating graph structured data. They are present in property paths in SPARQL~1.1, the new standard RDF query language, and in the XML query language XPath. In line with XPath, we consider the extension of 2RPQs with nesting, which allows one to require that objects along a path satisfy complex conditions, in turn expressed through (nested) 2RPQs. We study the computational complexity of answering nested 2RPQs and conjunctions thereof (CN2RPQs) in the presence of domain knowledge expressed in description logics (DLs). We establish tight complexity bounds in data and combined complexity for a variety of DLs, ranging from lightweight DLs (DL-Lite, EL) up to highly expressive ones. Interestingly, we are able to show that adding nesting to (C)2RPQs does not affect worst-case data complexity of query answering for any of the considered DLs. However, in the case of lightweight DLs, adding nesting to 2RPQs leads to a surprising jump in combined complexity, from P-complete to ExpTime-complete.

ABSTRACT. In the last few years there has been a large effort for analysing the computational properties of reasoning in fuzzy Description Logics. This has led to a number of papers studying the complexity of these logics, depending on their chosen semantics. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy DLs w.r.t. witnessed models over the Goedel t-norm. We show that in the logic G-IALC, reasoning cannot be restricted to finitely-valued models in general. Despite this negative result, we also show that all the standard reasoning problems can be solved in this logic in exponential time, matching the complexity of reasoning in classical ALC.

ABSTRACT. We investigate conjunctive query inseparability of description logic (DL) knowledge bases (KBs) w.r.t. a given signature, a fundamental problem for KB versioning, module extraction, forgetting and knowledge exchange. We study the data and combined complexity of deciding KB query inseparability for fragments of Horn-ALCHI, including the DLs underpinning OWL 2 QL and OWL 2 EL. While all of these DLs turn out to be P-complete for data complexity, the combined complexity ranges from P to EXPTIME and 2EXPTIME. We also resolve two major open problems for OWL 2 QL by showing that TBox query inseparability and the membership problem for universal UCQ solutions in knowledge exchange are both EXPTIME-complete for combined complexity.

ABSTRACT. In Description Logic (DL) knowledge bases (KBs) information is typically captured by crisp concepts. For many applications, querying the KB by crisp query concepts is too restrictive. A controlled way of gradually relaxing a query concept can be achieved by the use of concept similarity measures. In this paper we formalize the task of instance query answering for crisp DL KBs using concepts relaxed by concept similarity measures. We investigate computation algorithms for this task in the DL EL, their complexity and properties for the employed similarity measure regarding whether unfoldable or general TBoxes are used.

ABSTRACT. In this paper, we prove the decidability of stable model reasoning with guarded existential rules where rule bodies may contain negated atoms, as well as for reasoning using rules of the corresponding fragment of guarded Datalog+/-. In addition, we provide complexity results for these reasoning tasks (including conjunctive query answering) for a number of settings. Given that several lightweight description logics (in particular, DL-Lite, ELH, and OWL QL) can be directly translated to guardede Datalog+/-, we herewith obtain a direct stable model semantics for several description logics (DLs). This allows us to use negation (or complementation) directly in the axioms of a TBox, and to obtain a clear and natural semantics for such theories via their simple translation into an answer set program. We refer to this approach as to the "direct" stable model semantics in contrast to previous hybrid approaches that combine logic programming primitives with DL constructs, where the latter can be embedded into an answer set logic program, similar to generalized quantifiers (for example, the so-called dl-programs by Eiter et al. KR 2004; AIJ 2008).

ABSTRACT. We consider the scenario of ontology-based data access where a conjunctive query is evaluated against an ontological database. It is generally accepted that true scalability of conjunctive query answering in this setting can only be achieved by using standard relational database management systems (RDBMSs). An approach to conjunctive query answering that enables the use of RDBMSs is the so-called polynomial combined approach. We investigate this approach for the main guarded- and sticky-based classes of existential rules, and we highlight the assumptions on the underlying schema which are sufficient for the polynomial combined first-order rewritability of those classes. To the best of our knowledge, this is the first work which explicitly studies the polynomial combined approach for existential rules.

ABSTRACT. We study branching-time temporal description logics (BTDLs) based on the temporal logic CTL in the presence of rigid (time-invariant) roles and general TBoxes. There is evidence that, if full CTL is combined with the classical ALC in this way, then reasoning becomes undecidable. In this paper, we begin by substantiating this claim, establishing undecidability for a fragment of this combination. In view of this negative result, we then investigate BTDLs that emerge from combining fragments of CTL with lightweight DLs from the EL and DL-Lite families. We show that even rather inexpressive BTDLs based on EL exhibit very high complexity. Most notably, we identify two convex fragments which are undecidable and hard for non-elementary time, respectively. For BTDLs based on DL-Lite, we obtain tight complexity bounds that range from PSPACE to EXPTIME.

ABSTRACT. We study finite model reasoning in the popular expressive Horn description logics (DLs) Horn-SHIF and Horn-SHIQ, starting with a reduction of finite ABox consistency to unrestricted ABox consistency. The reduction relies on reversing certain cycles in the TBox, an approach that originated in database theory, was later adapted to the inexpressive DL DL-Lite_F, and is shown here to extend all the way to Horn-SHIQ. The model construction used to establish correctness sheds much more light on the structure of finite models than existing approaches to finite model reasoning in (non-Horn) DLs which rely on solving systems of inequations over the integers. Since the reduction incurs an exponential blow-up, we then devise a dedicated consequence-based algorithm for finite ABox consistency in Horn-SHIQ that implements the reduction on-the-fly rather than executing it up-front. The algorithm has optimal worst-case complexity and provides a promising foundation for implementations. Finally, we show that our approach can be adapted to finite (positive existential) query answering relative to Horn-SHIF TBoxes, which allows us to prove that this problem is ExpTime-complete in combined complexity and PTime-complete in data complexity.

ABSTRACT. We study polynomial time learning of description logic TBoxes in Angluin et al.'s framework of exact learning via queries. We admit entailment queries ("is a given subsumption entailed by the target TBox?") and equivalence queries ("is a given TBox equivalent to the target TBox?"), assuming that the signature and logic of the target TBox are known. We present four main results: (1) TBoxes formulated in DL-Lite with role inclusions and ELI concepts on the right-hand side of concept inclusions can be learned in polynomial time. (2) Neither general nor acyclic EL TBoxes can be learned in polynomial time. (3) EL TBoxes with only concept names on the right-hand side of concept inclusions can be learned in polynomial time. It follows, in particular, that non-polynomial time learnability of EL TBoxes is caused by the interaction between existential restrictions on the right and left-hand side of concept inclusions. Finally, we show that neither entailment nor equivalence queries alone are sufficient for learning TBoxes in polynomial time for any of the description logics in (1)-(3).

ABSTRACT. Nominal schemas extend description logics (DLs) with a restricted form of variables, thus integrating rule-like expressive power into standard DLs. They are also one of the most recently introduced DL features, and in spite of many works on algorithms and implementations, almost nothing is known about their computational complexity and expressivity. We close this gap by providing a comprehensive analysis of the reasoning complexities of a wide range of DLs---from EL to SROIQ---extended with nominal schemas. Both combined and data complexities increase by one exponential in most cases, with the one previously known case of SROIQ being the main exception. Our proofs employ general modeling techniques that exploit the power of nominal schemas to succinctly represent many axioms, and which can also be applied to study DLs beyond those we consider. To further improve our understanding of nominal schemas, we also investigate their semantics, traditionally based on finite grounding, and show that it can be extended to infinite sets of individuals without affecting reasoning complexities. We argue that this might be a more suitable semantics when considering entailments of axioms with nominal schemas.

ABSTRACT. We develop a clausal resolution-based approach for computing uniform interpolants of TBoxes formulated in the description logic ALC when such uniform interpolants exist. We also present an experimental evaluation of our approach and of its application to the logical difference problem for real-life ALC ontologies. Our results indicate that in many practical cases uniform interpolants exist and that they can be computed with the presented algorithm.

ABSTRACT. The standard way of answering queries over incomplete databases is to compute certain answers to them. These have always been defined as the intersection of query answers on all complete databases that are represented by the incomplete database. But is this universally accepted definition correct? Our goal is to argue that this `one-size-fits-all' definition can often lead to counterintuitive or just plain wrong results, and to propose an alternative framework for defining certain answers.

The idea of the framework is to move away from the standard, in the database literature, assumption that query results be given in the form of a database object, and to allow instead two alternative representations of answers: as objects defining all other answers, or as knowledge we can deduce with certainty about all such answers. We show that the latter is often easier to achieve than the former, that in general certain answers need not be defined as intersection, and may well contain missing information in them. We also show that with a proper choice of semantics, we can often reduce computing certain answers - as either objects or knowledge - to standard query evaluation. We describe the framework in the most general way, applicable to a variety of data models, and test it on three concrete relational semantics of incompleteness: open, closed, and weak closed world.

ABSTRACT. We consider the problem of representing and reasoning about computer programs, and propose a translator from a core procedural iterative programming language to first-order logic with quantification over the domain of natural numbers that includes the usual successor function and the ``less than'' linear order, essentially a first-order logic with a discrete linear order. Unlike Hoare's logic, our approach does not rely on loop invariants. Unlike typical temporal logic specification of programs, our translation does not require a transition system model of the program, and is compositional on the structures of the program. Some non-trivial examples are given to show the effectiveness of our translation for proving properties of programs.

ABSTRACT. Agents in real-world environments may have only \emph{partial} access to available information, often in an arbitrary, or hard to model, manner. By reasoning with knowledge at their disposal, agents may hope to recover some missing information. By acquiring the knowledge through a process of learning, the agents may further hope to guarantee that the recovered information is indeed correct.

Assuming only a black-box access to a learning process and a prediction process that are able to cope with missing information in some principled manner, we examine how the two processes should interact so that they improve their overall joint performance. We identify natural scenarios under which the interleaving of the processes is provably beneficial over their independent use.

ABSTRACT. We study disambiguating of pronoun references in Winograd Schemas, which are part of the Winograd Schema Challenge, a proposed replacement for the Turing test. In particular we consider sentences where the pronoun can be resolved to both antecedents without semantic violations in world knowledge, that means for both readings of the sentence there is a possible consistent world. Nevertheless humans will strongly prefer one answer, which can be explained by pragmatic effects described in Relevance Theory. We state formal optimization criteria based on principles of Relevance Theory in a simplification of Roger Schank's graph framework for natural language understanding. We perform experiments using Answer Set Programming and report the usefulness of our criteria for disambiguation and their sensitivity to parameter variations.

ABSTRACT. Multi-context systems (MCSs) define a versatile framework for integrating and reasoning about knowledge from different (heterogeneous) sources. In MCSs, different types of non-monotonic reasoning are characterized by different semantics such as equilibrium semantics and grounded equilibrium semantics [Brewka and Eiter, 2007].

We introduce a novel semantics of MCSs, a supported equilibrium semantics. Our semantics is based on a new notion of support. The ``strength'' of supports determines a spectrum of semantics that, in particular, contains the equilibrium and grounded equilibrium semantics. In this way, our supported equilibrium semantics generalizes these previously defined semantics. Moreover, the ``strength'' of supports gives us a measure to compare different semantics of MCSs.

ABSTRACT. Angry Birds is a popular video game where the task is to kill pigs protected by a structure composed of different building blocks that observe the laws of physics. The structure can be destroyed by shooting the angry birds at it. The fewer birds we use and the more blocks we destroy, the higher the score. One approach to solve the game is by analyzing the structure and identifying its strength and weaknesses. This can then be used to decide where to hit the structure with the birds.

In this paper we use a qualitative spatial reasoning approach for this task. We develop a novel qualitative spatial calculus for representing and analyzing the structure. Our calculus allows us to express and evaluate structural properties and rules, and to infer for each building block which of these properties and rules are satisfied. We use this to compute a heuristic value for each block that corresponds to how useful it is to hit that block. We evaluate our approach by comparing the consequences of the suggested shot with other possible shots.

ABSTRACT. Diagnostic problem solving involves a myriad of reasoning tasks associated with the determination of diagnoses, the generation and execution of tests to discriminate diagnoses, and the determination and execution of actions to alleviate symptoms and/or their root causes. Fundamental to diagnostic problem solving is the need to reason about action and change. In this work we explore these myriad of reasoning tasks through the lens of AI automated planning. We characterize a diversity of reasoning tasks associated with diagnostic problem solving, prove properties these characterizations, and define correspondences with established automated planning tasks and existing state-of-the-art planning systems. In doing so, we provide deeper insight into the computational challenges associated with diagnostic problems solving, as well as proposing practical algorithms for their realization.

ABSTRACT. In this paper we present a tableau-based method to decide the satisfiability of formulas in ATEL, an extension of the alternating-time temporal logic ATL including epistemic modalities for individual knowledge. Specifically, we analyse satisfiability of ATEL formulas under a number of conditions. We evaluate the impact of the assumptions of synchronicity and of a unique initial state, which have been proposed in the context of Interpreted Systems. Also, we consider satisfiability at a initial state as opposed to any state in the system. We introduce a tableau-based decision procedure for each of these combinations. Moreover, we adopt an agent-based approach to satisfiability, namely, the decision procedure returns a set of agents inducing a concurrent game structure that satisfies the specification at hand.

ABSTRACT. Our aim is to develop techniques for reasoning about game-like concurrent systems, where the components of the system act rationally and strategically in pursuit of logically-specified goals. We first present a computational model for such systems, and investigate its properties. We then define and investigate a branching-time logic for reasoning about the equilibrium properties of such systems. The key operator in this logic is a path quantifier [NE]phi, which asserts that phi holds on all Nash equilibrium computations of the system.

ABSTRACT. The paper presents an extension of temporal epistemic logic with epistemic operators that capture what agents could deduce from knowledge of the strategies of some subset of the set of agents. Some examples are presented to motivate the framework, and relationships to several variants of alternating temporal epistemic logic are discussed. Results on model checking the logic are then presented.

ABSTRACT. We introduce an abstraction methodology for the verification of multi-agent systems against specifications in alternating time temporal logic (ATL). Inspired by methodologies such as predicate abstraction, we define a three-valued semantics for the interpretation of ATL formulas on concurrent game structures and compare it to the standard two-valued semantics. We define abstract models and establish preservation results on the three-valued semantics between abstract models and their concrete counterparts. We illustrate the methodology on the large state spaces resulting from a card game.

ABSTRACT. When Lin and Reiter introduced the progression of basic action theories in the situation calculus, they were essentially motivated by long-lived robotic agents functioning over thousands of actions. However, their account does not deal with probabilistic uncertainty about the initial situation nor with effector or sensor noise, as needed in robotic applications. In this paper, we obtain results on how to progress continuous degrees of belief against continuous effector and sensor noise in a semantically correct fashion. Most significantly, and perhaps surprisingly, we identify conditions under which our account is not only as efficient as the filtering mechanisms commonly used in robotics, but considerably more general.

ABSTRACT. Among the most frequent reasoning tasks in the situation calculus are projection queries that query the truth of conditions in a future state of affairs. However, in long running action sequences solving the projection problem is complex. The main contribution of this work is a new technique which allows the length of the action sequences to be reduced by reordering independent actions and removing dominated actions; maintaining semantic equivalence with respect to the original action theory. This transformation allows for the removal of actions that are problematic with respect to progression, allowing for periodical update of the action theory to reflect the current state of affairs. We provide the logical framework for the general case and give specific methods for two important classes of action theories. The work provides the basis for handling more expressive cases, such as the reordering of sensing actions in order to delay progression, and forms an important step towards facilitating ongoing planning and reasoning by long-running agents. It provides a mechanism for minimising the need for keeping the action history while appealing to both regression and progression.

ABSTRACT. Verification of dynamic systems that manipulate data, stored in a database or ontology, has lately received increasing attention. A plethora of recent works has shown that verification of systems working over unboundedly many data is decidable even for very rich temporal properties, provided that the system is state-bounded. This condition requires the existence of an overall bound on the amount of data stored in each single state along the system evolution. In general, checking state-boundedness is undecidable. An open question is whether it is possible to isolate significant classes of dynamic systems for which state-boundedness is decidable. In this paper we provide a surprisingly strong negative answer, by resorting to a novel connection with variants of Petri nets. In particular, we show undecidability for systems whose data component contain unary relations only, and whose action component query and update such relations in a very limited way. To contrast this result, we propose interesting relaxations of the sufficient conditions proposed in the concrete setting of Data-Centric Dynamic Systems, building on recent results on chase termination for tuple-generating dependencies.

ABSTRACT. The situation calculus is a popular formalism for reasoning about actions and change. Since the language is first-order, reasoning in the situation calculus is undecidable in general. An important question then is how to weaken reasoning in a principled way to guarantee decidability. Existing approaches either drastically limit the representation of the action theory or neglect important aspects such as sensing. In this paper we propose a model of limited belief for the epistemic situation calculus, which allows very expressive knowledge bases and handles both physical and sensing actions. The model builds on an existing approach to limited belief in the static case. We show that the resulting form of limited reasoning is sound with respect to the original epistemic situation calculus and eventually complete for a large class of formulas. Moreover, reasoning is decidable.

ABSTRACT. Golog and ConGolog are languages defined in the situation calculus for cognitive robotics. Given a Golog program P, its semantics is defined by a macro Do(P,s,s') that expands to a logical sentence that captures the conditions under which performing P in s can terminate in s'. A similar macro is defined for ConGolog programs. In general, the logical sentences that these macros expand to are second-order, and in the case of ConGolog, may involve quantification over programs. In this paper, we show that by making use of the foundational axioms in the situation calculus, these macro expressions can actually be defined using first-order sentences.

ABSTRACT. Artifact-centric systems are a recent paradigm used to represent and implement business processes. We present further results on the verification problem of artifact-centric systems specified by means of FO-CTL specifications. While the general problem is known to be undecidable, results in the literature prove decidability for artifact systems with infinite domains under boundedness and conditions such as uniformity. We here follow a different approach and investigate the general case under the infinite domains assumption. We show the decidability for the class of artifact-centric systems whose database schemas consist of a single unary relation, and we show that that the problem is undecidable if artifact systems are defined by using one binary relation or two unary relations.

ABSTRACT. In this paper we develop a general framework that allows for both knowledge acquisition and forgetting in the Situation Calculus. Based on the Scherl and Levesque possible worlds approach to knowledge in the Situation Calculus, we allow for both sensing as well as explicit forgetting actions to take place. This model of forgetting is then compared to existing frameworks, particularly showing that forgetting is well-behaved with respect to the contraction operator of the well-known AGM theory of belief revision.

ABSTRACT. We present a cognitive design assistance system equipped with analytical capabilities aimed at anticipating architectural building design performance with respect to people-centred functional design goals. The paper focuses on the system capability to generate \emph{narratives of visuo-locomotive user experience} from digital computer-aided architecture design (CAAD) models. The system is based on an underlying declarative narrative representation and computation framework pertaining to conceptual, geometric, and qualitative spatial knowledge. The semantics of the declarative narrative model, i.e., the overall representation and computation model, is founded on: (a) conceptual knowledge formalised in an OWL ontology; (b) a general spatial representation and reasoning engine implemented in constraint logic programming; and (c) a declaratively encoded (narrative) construction process (over graph structures) implemented in answer-set programming.

We emphasise and demonstrate: complete system implementation, algorithmic scalability, and robust performance \& integration with industry-scale architecture industry tools (e.g., Revit, ArchiCAAD) \& standards (BIM, IFC).

ABSTRACT. In this paper we present SmartPM, a model and a prototype Process Management System featuring a set of techniques providing support for automatic adaptation of knowledge-intensive processes at run-time. Such techniques are able to automatically adapt process instances without explicitly defining policies to recover from exceptions and without the intervention of domain experts at run-time, aiming at reducing error-prone and costly manual ad-hoc changes, and thus at relieving users from complex adaptations tasks. To accomplish this, we make use of well-established techniques and frameworks from Artificial Intelligence, such as situation calculus, Indigolog and classical planning.

ABSTRACT. This paper presents Tweety, an open source project for scientific experimentation on logical aspects of artificial intelligence and particularly knowledge representation. Tweety provides a general framework for implementing and testing knowledge representation formalisms in a way that is familiar to researchers used to logical formalizations. This framework is very general, widely applicable, and can be used to implement a variety of knowledge representation formalisms from classical logics, over logic programming and computational models for argumentation, to probabilistic modeling approaches. Tweety already contains over 15 different knowledge representation formalisms and allows easy computation of examples, comparison of algorithms and approaches, and benchmark tests. This paper gives an overview on the technical architecture of Tweety and a description of its different libraries. We also provide two case studies that show how Tweety can be used for empirical evaluation of different problems in artificial intelligence.

ABSTRACT. Graphical belief models are compact and powerful tools for representing and reasoning under uncertainty. Possibilistic networks are graphical belief models based on possibility theory. In this paper, we address reasoning under uncertain inputs in both quantitative and qualitative possibilistic networks. More precisely, we first provide possibilistic counterparts of Pearl's methods of virtual evidence then compare them with the possibilistic counterparts of Jeffrey's rule of conditioning. As in the probabilistic setting, the two methods are shown to be equivalent in the quantitative setting regarding the existence and uniqueness of the solution. However in the qualitative setting, Pearl's method of virtual evidence which applies directly on graphical models disagrees with Jeffrey's rule and the virtual evidence method. The paper provides the precise situations where the methods are not equivalent. Finally, the paper addresses related issues like transformations from one method to another and commutativity.

ABSTRACT. Logistic regression is a commonly used representation for aggregators in Bayesian belief networks when a child has multiple parents. Variations of population, as well as a desire to model interactions between parents in relational models, introduce representational problems for using logistic regression in relational models. In this paper, we first examine the representational problems caused by population variation. We show how these problems arise even in simple cases with a single parametrized parent, and propose a linear relational logistic regression which we show can represent arbitrary linear (in population size) decision thresholds, where the traditional logistic regression cannot. Then we examine representing interactions between parents of a child node, and representing non-linear dependency on population size. We propose a multi-parent relational logistic regression which can represent interactions between parents and arbitrary polynomial decision thresholds. Finally, we show how other well-known aggregators can be represented using this relational logistic regression.

ABSTRACT. In this paper, we propose the Probabilistic Sentential Decision Diagram (PSDD), which is a canonical representation for probability distributions that are defined over the models of a propositional theory. Each parameter of a given PSDD can be viewed as the (conditional) probability of making a decision in a corresponding Sentential Decision Diagram (SDD), which itself is a recently proposed canonical representation of propositional theories. We explore a number of interesting properties of PSDDs, including the context-specific independencies that underlie them. We further show how the parameters of a PSDD can be efficiently estimated, in closed form, from complete data. We finally empirically evaluate the quality of PSDDs learned from data, when we have knowledge, a priori, of the logical theory supporting an otherwise unknown probability distribution.

ABSTRACT. Inconsistency measures help analyzing contradictory knowledge bases and resolving inconsistencies. In recent years several measures with desirable properties have been proposed, but often these measures correspond to combinatorial or non-convex optimization problems that are hard to solve in practice. In this paper, I study a new family of inconsistency measures for probabilistic knowledge bases. All members satisfy many desirable properties and can be computed by means of convex optimization techniques. For two members, I present linear programs whose computation is barely harder than a probabilistic satisfiability test.

ABSTRACT. In epistemic logic, some axioms dealing with the notion of knowledge are rather convoluted and it is difficult to give them an intuitive interpretation, even if some of them, like axioms .2 and .3, are considered by some epistemic logicians to be key axioms. We show that they can be characterized in terms of understandable interaction axioms relating knowledge and belief or knowledge and conditional belief. In order to show it, we first sketch a primitive theory dealing with the characterization of axioms in terms of interaction axioms in modal logic. We then apply its general results to obtain some specific results related to epistemic and doxastic logics.

ABSTRACT. Recently, several versions of functional stable model semantics have emerged in order to express defaults involving non-Herbrand functions. We present a new perspective on these formalisms by reducing them to the General Theory of Stable Models, which allows us to understand intensional functions in terms of intensional predicates. This perspective not only allows us to transfer theoretical results established for the General Theory of Stable Models, such as safety, splitting theorem, and strong equivalence, to functional stable model semantics, but also tells us how to make further extensions, such as allowing aggregates and generalized quantifiers. In addition, we show that the functional stable model semantics that allows partial functions is no more expressive than the one that does not, in the sense that partial functions can be eliminated in favor of total functions. Based on these results, we present an implementation of different versions of functional stable model semantics by using existing ASP solvers.

ABSTRACT. Identity relations are at the foundation of many logic-based knowledge representations. We argue that the traditional notion of equality, based on Leibniz’ principle of indiscernability, is unsuited for many realistic knowledge representation settings. The classical interpretation of equality is simply too strong when the equality statements are re-used outside their original context.

The most prominent modern example of such re-use of knowledge across contexts is the Linked Open Data initiative, and the SemanticWeb in general. On the SemanticWeb, equality statements are used to interlink multiple descriptions of the same object, using owl:sameAs assertions. And indeed, many practical uses of owl:sameAs are known to violate the formal Leibniz-style semantics.

First, we survey the problems with the classical definition of identity, both in general, and on the Semantic Web in particular. In order to provide a more flexible semantics to identity, we then propose a method that assigns meaning to the subrelations of an identity relation using the predicates that are used in a knowledge-base. Using those indiscernabilitypredicates, we define upper and lower approximations of equality in the style of rought-set theory, resulting in a quality-measure for the identity relation.

We illustrate our approach on a realistic Semantic Web dataset, and we experimentally verify that our approach yields the intuitively desired results on this dataset.

ABSTRACT. In a seminal paper, Lin and Reiter introduced the progression of basic action theories in the situation calculus. In this paper, we study the progression of knowledge in multiagent settings, where after actions, an agent updates his beliefs but also updates what he believes other agents know given what has occurred. By appealing to the notion of only knowing, we are able to avoid limitations of earlier work on multiagent progression, and obtain a new general account: we show that after an action, knowledge bases are updated in a Lin and Reiter fashion at every nesting of modalities. Consequently, recent results on the first-order definability of progression carry over to a multiagent setting without too much effort.

ABSTRACT. Given a set of conflicting arguments, there can exist multiple plausible opinions about which arguments should be accepted, rejected, or deemed undecided. Recent work explored some operators for deciding how multiple such judgments should be aggregated. Here, we generalize this line of study by introducing a family of operators called *interval aggregation methods*, and show that they contain existing operators as instances. While these methods fail to output a complete labelling in general, we show that it is possible to *transform* a given aggregation method into one that *does* always yield collectively rational labellings. This employs the *down-admissible* and *up-complete* constructions of Caminada and Pigozzi. For interval methods, collective rationality is attained at the expense of a strong *Independence* postulate, but we show that an interesting weakening of the Independence postulate is retained by this transformation. Our results open up many new directions in the study of generalized judgment aggregation in argumentation

ABSTRACT. Temporal Equilibrium Logic (TEL) is a non-monotonic temporal logic that extends Answer Set Programming (ASP) by introducing modal operators as those considered in Linear-time Temporal Logic (LTL). TEL allows proving temporal properties of ASP-like scenarios under the hypothesis of infinite time while keeping decidability. Formally, it extends Equilibrium Logic (the best-known logical formalisation of ASP) and, as the latter, it selects some models of a (temporal) monotonic basis: the logic of Temporal Here-and-There (THT). In this paper we solve a problem that remained unanswered for the last six years: we prove that equivalence in the logic of THT is not only a sufficient, but also a necessary condition for strong equivalence of two TEL theories. This result has both theoretical and practical consequences. First, it reinforces the need of THT as a suitable monotonic basis for TEL. Second, it has allowed constructing a tool, ABSTEM, that can be used to check different types of equivalence between two arbitrary temporal theories. More importantly, when the theories are not THT-equivalent, the system provides a context theory that makes them behave differently, together with a Buchi automaton showing the temporal stable models that arise from that difference.

ABSTRACT. Boolean games are a framework for reasoning about the rational behaviour of agents whose goals are formalised using propositional formulas. They offer an attractive alternative to normal-form games, because they allow for a more intuitive and more compact encoding. Unfortunately, however, there is currently no general, tailor-made method available to compute the equilibria of Boolean games. In this paper, we introduce a method for finding the pure Nash equilibria based on disjunctive answer set programming. Our method is furthermore capable of finding the core elements and the Pareto optimal equilibria, and can easily be modified to support other forms of optimality, thanks to the declarative nature of disjunctive answer set programming. Experimental results clearly demonstrate the effectiveness of the proposed method.

ABSTRACT. Forgetting has been addressed in different areas of Knowledge Representation, including classical logic, logic programming, modal logic, and description logics. In this paper, we present an account of forgetting as an abstract belief change operator, independent of an underlying logic. We argue that forgetting amounts to a reduction in the language, specifically the signature, of a logic. The central definition is simple: the result of forgetting signature $\sigma$ in a theory is simply the set of logical consequences over the reduced language. This definition offers various advantages. It provides a uniform approach to forgetting, with a single definition applicable to any logic with a well-defined consequence relation. Results obtained are obviously applicable to all subsumed formal systems, and in fact many results are obtained much more straightforwardly. We argue that the perspective provided by the approach leads to simpler approaches to computing forgetting in specific logics. This view also leads to insights with respect to specific logics: forgetting in first-order logic is somewhat different from the accepted approach; the definition relativised to logic programs yields a new syntax-independent notion of forgetting; in modal logic the specification is simpler. Moreover, the obtained perspective clarifies the relation between forgetting and the belief change operation of contraction.

ABSTRACT. This paper brings together the theory of argumentation in AI with the psychology of story comprehension to develop a KR\&R framework for narrative text comprehension. The proposed framework is based on a computational interpretation of the general psychological principles of coherency and cognitive economy for text comprehension. Part of a wider study, this paper concentrates on the central problem of integration (or elaboration) of explicit information from the text with implicit (in the reader's mind) common sense world knowledge pertaining to the topic(s) of the story. We show how some of the major challenges for successful story comprehension are closely related to those of NMR, as found in Default Reasoning and Reasoning about Action and Change, and more specifically Knowledge Qualification and Revision. We show how an appropriate formulation through argumentation can give a basis for automating the construction and revision of a coherent comprehension model of a narrative. We report on a first set of empirical experiments designed to harness the implicit world knowledge used by humans reading a story to guide the background knowledge given as input to our framework. We present a prototype system that is used to evaluate the ability of our approach to capture both the majority and the variability of understanding of a story by the human readers in the experiment.

ABSTRACT. Several researchers have developed properties that ensure compatibility of a concept similarity or dissimilarity measure with the formal semantics of Description Logics. While these authors have highlighted the relevance of the triangle inequality, none of their proposed dissimilarity measures satisfies it. In this work we present several dissimilarity measures with this property: first, a simple dissimilarity measure, based on description trees for the lightweight Description Logic EL; secondly, a general framework based on concept relaxations; last, an instantiation of the general framework using dilation operators from mathematical morphology, exploiting the link between Hausdorff distance and dilations using balls of the ground distance as structuring elements. A comparison between these definitions and their properties is provided as well.

ABSTRACT. The Region Connection Calculus (RCC) is a well-known calculus for representing part-whole and topological relations. It plays an important role in qualitative spatial reasoning, geographical information science, and ontology. The computational complexity of reasoning with RCC has been investigated in depth in the literature. Most of these works focus on the consistency of RCC constraint networks. In this paper, we consider the important problem of redundant RCC constraints. For a set $\Gamma$ of RCC constraints, we say a constraint (x R y) in $\Gamma$ is redundant if it can be entailed by the rest of $\Gamma$. A prime network of $\Gamma$ is a subset of $\Gamma$ which contains no redundant constraints but has the same solution set as $\Gamma$. It is natural to ask how to compute a prime network, and when it is unique. In this paper, we show that this problem is in general co-NP hard, but becomes tractable if $\Gamma$ is over a tractable subclass of RCC. If S is a tractable subclass in which weak composition distributes over non-empty intersections, then we can show that $\Gamma$ has a unique prime network, which is obtained by removing all redundant constraints from $\Gamma$. As a byproduct, we identify a sufficient condition for a path-consistent network being minimal.

ABSTRACT. Belief revision is an operation that aims at modifying old beliefs so that they become consistent with new ones. The issue of belief revision has been studied in various formalisms, in particular, in qualitative algebras (QAs) in which the result is a disjunction of belief bases that is not necessarily representable in a QA. This motivates the study of belief revision in formalisms extending QAs, namely, their propositional closures: in such a closure, the result of belief revision belongs to the formalism. Moreover, this makes it possible to define a contraction operator thanks to the Harper identity. Belief revision in the propositional closure of QAs is studied, an algorithm for a family of revision operators is designed, and an open-source implementation is made freely available on the web.

ABSTRACT. We contribute to the study of the meta-logical properties of argumentation frameworks, as introduced by Dung. Such frameworks are used in a variety of contexts in contemporary AI, not just as a means to model argumentative scenarios, but also as an abstract mathematical representation of non-monotonic reasoning patterns more generally. Importantly, Dung observed that by representing such patterns by directed graphs, various semantics for non-monotonic reasoning could be formulated in graph theoretic terms. In this paper we address so-called sceptical reasoning about argumentation frameworks, asking the following question: what are the propositional validities of abstract argumentation? We answer this by giving graph constructions demonstrating that the set of validities for a range of different argumentation semantics coincide and that it is axiomatized by three-valued Lukasiewicz logic.

ABSTRACT. In this paper we investigate the problem of building knowledge maps of graph-like information, motivated by representing knowledge on the Web. We introduce a mathematical formalism that captures the notion of map of a graph and enables its development and manipulation in a semi-automated way. We present an implementation of our formalism over the Web of Linked Data graph and discuss algorithms to efficiently generate and combine (via an algebra) regions and maps. We present the MaGE tool and discuss some examples of knowledge maps.

ABSTRACT. Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such properties is non-obvious and can be challenging indeed. In this paper, we take a number of tree-like properties into consideration and investigate various logic-based approaches to encode them. We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic, and linear programming. We study the compactness of encodings and the resulting computational performance on benchmarks involving tree-like constructs.

ABSTRACT. We propose a formalization framework for modeling how beliefs and intentions change over the course of a dialogue, in the case where the decisions taken during the dialogue affect the possibly conflicting goals of the agents involved. We illustrate our formalization with the game of Werewolf, as an example of such a domain.

We use Situation Calculus to model the evolution of the world and an observation model to analyze the evolution of intentions and beliefs. In our formalization, utterances, that only change the beliefs and intentions, are observations. The beliefs and intentions are modeled with Kripke structure-style accessibility relation predicates. We illustrate our model on instances of the game.

ABSTRACT. The paper develops a branching-time ontology that maintains the classical restriction of forward movement through a temporal tree structure, but permits the representation of paths in which one can perform inferences about time-travel scenarios. Central to the ontology is the notion of an agent embodiment whose beliefs are equivalent to those of an agent who has time-traveled from the future. We discuss the formalization of several example scenarios, define what it means for such scenarios to be motivated with respect to an agent embodiment, and relate the underlying structure to a more general theory of (non-time-travel) narrative.

ABSTRACT. In this paper, we provide foundations for deontic logic, by defining an undemanding semantics based on the sole notion of detachment. We introduce System O, which handles iteration of successive detachments in a more principled manner than the traditional systems do. This is achieved by injecting a new form of deontic detachment, called aggregative deontic detachment. It allows to keep track of previously detached obligations. Soundness and completeness of the proof system are established. Properties of the logic are discussed.

ABSTRACT. Situation calculus action theories allow full first-order expressiveness but, typically, restricted cases are studied such that projection or progression become decidable or first-order, respectively, and computationally feasible. In this work we focus on KBs that are specified as generalized databases with equality constraints, thus able to finitely represent complete information over possibly infinite number of objects. First, we show that this form characterizes the class of definitional KBs and provide a transformation for putting KBs in this form that we call \emph{generalized fluent DB}. Then we show that for action theories over such KBs, the KBs are closed under progression, and discuss how this view exposes some differences with existing progression methods compared to DB update. We also look into the temporal projection problem and show how queries over these theories can be decided based on an induced transition system and evaluation of local conditions over states. In particular, we look into a wide class of generalized projection queries that include quantification over situations and prove that it is decidable under a practical restriction. The proposed action theories are to date the most expressive ones for which there are known decidable methods for computing both progression and generalized projection.

ABSTRACT. The tendency to accept or reject arguments based on own beliefs or prior knowledge rather than on the reasoning process is called the belief-bias effect. A psychological syllogistic reasoning task which has been carried out by Evans, Barston and Pollard, aims at showing this phenomenon, wherein participants were asked whether they would accept or reject a given syllogism. We discuss one specific case which is commonly assumed to be believable but not logically valid. By introducing abnormalities, abduction and background knowledge, we adequately model this case under the weak completion semantics. Our formalization reveals new questions about possible extensions in abductive reasoning. For instance, observations and their explanations might include some relevant prior abductive contextual information concerning some side-effect or leading to a contestable or rebutable side-effect. A weaker notion indicates the support of some relevant consequences by a prior abductive context. Yet another definition describes jointly supported relevant consequences, which captures the idea of two observations containing mutually supportive side-effects. Though motivated with and exemplified by the running psychology application, the various new general abductive context definitions are introduced here and given a declarative semantics for the first time, and have a much wider scope of application. Inspection points, a concept introduced by Pereira and Pinto, allows us to express these definitions syntactically and intertwine them into an operational semantics. Future work within this setting may prospect notions about contextual explanatory plausibility, of contextual model-based fault-finding, and of contextual model representation debugging.

ABSTRACT. In this paper, we address the problem of applying AGM-style belief revision to non-classical logics. We discuss the idea of minimal change in revision and show that for non-classical logics, some sort of minimality postulate has to be explicitly introduced. We also present two constructions for revision which satisfy the AGM postulates and prove the representation theorems including minimality postulates. For each result, we point out the class of logics for which the theorem holds, giving some examples at the end.

ABSTRACT. We propose a novel approach to performance prediction of OWL reasoners. The existing strategies take a view of an entire ontology corpus: they extract multiple features from the ontologies in the corpus and use them for training machine learning models. We call these global approaches. In contrast, our approach is a local one: it examines a single ontology (independent of any corpus), selects suitable, small ontology subsets, and extrapolates their performance measurements to the whole ontology. Our results show that this simple idea leads to accurate performance predictions, comparable or superior to global approaches. Our second contribution concerns ontology features: we are the first to investigate intercorrelation of ontology features using Principal Component Analysis (PCA). We report that extracting multiple features - as global approaches do - makes surprisingly little difference for performance prediction. In fact, it turns out that the ontologies in two major corpora basically only differ in one or two features.

ABSTRACT. Canonical (logic) programs} (CP) refer to \emph{normal} programs (LP) augmented with connective $not\ not$. In this paper we address the question of whether CP are \emph{succinctly incomparable} with \emph{propositional formulas} (PF). Our main result shows that the PARITY problem, which can be polynomially represented in PF, \emph{only} has exponential representations in CP. In other words, PARITY \emph{separates} PF from CP. Simply speaking, this means that exponential size blowup is generally inevitable when translating a set of formulas in PF into an equivalent program in CP (without introducing new variables). Furthermore, since it has been shown by Lifschitz and Razborov that there is also a problem which separates CP from PF (assuming $\mathsf{P}\nsubseteq \mathsf{NC^1/poly}$), it follows that the two formalisms are indeed succinctly incomparable. In addition, we show that PARITY separates logic programs with \emph{cardinality constraints} and \emph{choice rules} (CC) from CP. Moreover, assuming $\mathsf{P}\nsubseteq \mathsf{NC^1/poly}$, CP and \emph{definite causal theories} (DT) are succinctly incomparable, \emph{two-valued} programs (TV) are strictly more succinct than CP and DT.

ABSTRACT. Planning as Satisfiability is an important approach to Propositional Planning. A serious drawback of the method is its limited scalability, as the instances that arise from large planning problems are often too hard for modern SAT solvers.

This work tackles this problem by combining two powerful techniques that aim at decomposing a planning problem into smaller sub-problems, so that the satisfiability instances that need to be solved do not grow prohibitively large. The first technique, incremental goal achievement, turns planning into a series of boolean optimization problem, each seeking to maximize the number of goals that are achieved within a limited planning horizon. This is coupled with a second technique, called heuristic guidance, that directs search towards a state that satisfies all goals. Heuristic guidance is based on the combination of a number of constraint relaxation techniques of varying strength.

Initial experiments with a system that implements these ideas demonstrate that enriching propositional satisfiability based planning with these methods delivers a competitive planning algorithm that is capable of generating plans of good quality for challenging problems in different domains.

ABSTRACT. It is well known that Reiter's original proposal for default logic in the first-order case is problematic because of Skolemization. This paper reconsiders this long-standing open problem, and proposes a new world view semantics for first-order default logic. Roughly speaking, a world view of a first-order default theory is a maximal collection of structures satisfying the default theory where the default part is fixed by the world view itself. We show that how this semantics generalizes propositional/closed default logic, classical first-order logic and first-order answer set programming, and we argue that first-order default logic under the world view semantics provides a rich framework for integrating classical logic and rule-based formalism in the first-order case.