## Accepted Papers

 Paul Dunne and Martin Caminada. Computational Complexity of Semi-stable Semantics in Abstract Argumentation Frameworks Abstract: Semi-stable semantics offer a further extension based formalism by which the concept of "collection of justified arguments" in abstract argumentation frameworks may be described. In contrast to the better known stable semantics, one advantage of semi-stability is that any finite argumentation framework always has at least one semi-stable extension. Although there has been some development of the formal logical theory of semi-stable semantics so that several computational properties of these extensions have been identified, with the exception of some algorithmic studies, more detailed investigation of computational complexity issues has been neglected. Our purpose in this article is to present a number of results on the complexity of some natural decision questions for semi-stable semantics. Ekaterina Komendantskaya and John Power. Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness. Abstract: We introduce a fibrational semantics for many-valued logic programming, use it to define an SLD-resolution for annotation-free many valued logic programs as defined by Fitting, and prove a soundness and completeness result relating the two. We show that fibrational se- mantics corresponds with the traditional declarative (ground) semantics and deduce a soundness and completeness result for our SLD-resolution algorithm with respect to the ground semantics. Sebastian Rudolph, Markus Krötzsch and Pascal Hitzler. Cheap Boolean Role Constructors for Description Logics Abstract: We investigate the possibility of incorporating Boolean role constructors on simple roles into some of today's most popular description logics, focussing on cases where those extensions do not increase complexity of reasoning. We show that the expressive DLs SHOIQ and SROIQ, serving as the logical underpinning of OWL and the forthcoming OWL 2, can accommodate arbitrary Boolean expressions. The prominent OWL-fragment SHIQ can be safely extended by safe role expressions, and the tractable fragments EL++ and DLP retain tractability if extended by conjunction on roles, where in the case of DLP the restriction on role simplicity can even be discarded. Luciano Caroprese and Mirek Truszczynski. Declarative Semantics for Revision Programming and Connections to Active Integrity Constraints Abstract: We investigate revision programming, a formalism to describe constraints on belief sets (databases, knowledge bases), and to specify preferred ways to enforce them. We propose several semantics for revision programs combining ideas from logic programming and active integrity constraints, a formalism to model preferred ways to enforce integrity constraints on databases. We present results on the complexity of the semantics we introduce. We also show that all these semantics are invariant under "shifting". Finally, we prove that from the perspective of a broad semantic landscape of revision programming, there is a direct correspondence between revision programs and active integrity constraints. Aleksandar Perovic, Zoran Ognjanović, Miodrag Raskovic and Zoran Markovic. How to restore compactness into probabilistic logics? Abstract: The paper offers a proof of the compactness theorem for the $^*\mathbb R$-valued polynomial weight formulas. We also provide a complete axiomatization for the polynomial weight formulas. John McCabe-Dansted. A Tableau for RoBCTL* Abstract: It can be desirable to specify polices that require a system to achieve some outcome even if a certain number of failures occur. The temporal logic of robustness RoCTL* extends CTL* with operators from Deontic logic, and a novel operator referred to as "Robustly". The only known decision procedure for RoCTL* involves a reduction to QCTL*. This paper presents a tableau for the related bundled tree logic RoBCTL*; this is the first decision procedure for RoBCTL*, and although non-elementary in degenerate cases has much better performance than the QCTL* based decision procedure for RoCTL*. The degenerate cases where this tableau performs poorly provide clues as to where we might look to prove that RoBCTL* is non-elementary. Pietro Sala, Angelo Montanari, Davide Bresolin and Guido Sciavicco. An Optimal Tableau for Right Propositional  Neighborhood Logic over Linear Orders Abstract: The study of interval-based temporal logics on linearly or- dered domains is a meaningful research area in computer science. Unfor- tunately, even when restricted to propositional languages, interval logics turn out to be undecidable in most cases. Decidability has been usu- ally recovered by imposing severe syntactic and/or semantic restrictions on the logics. In the last years, some unrestricted decidability results, based on tableau methods, have been obtained for logics of temporal neighborhoods and logics of subinterval relations over specific classes of temporal structures. In this paper, we develop an optimal NEXPTIME tableau-based decision procedure for the future fragment of Propositional Neighborhood Logic over the class of all linearly ordered sets. Koen Hindriks and Wiebe van der Hoek. GOAL Agents Instantiate Intention Logic Abstract: It is commonly believed there is a big gap between agent logics and computational agent frameworks. In this paper, we show that this gap is not as big as believed by showing that GOAL agents instantiate Intention Logic of Cohen and Levesque. That is, we show that GOAL agent programs can be formally related to Intention Logic. We do so by proving that the GOAL Verification Logic can be embedded into Intention Logic. It follows that (a fragment of) Intention Logic can be used to prove properties of GOAL agents. The work reported is an important step towards the application of standard tools from modal logic for e.g. model checking agent programs. Our results also prove useful for extending the expressiveness of the GOAL agent language. This is illustrated by incorporating temporally extended goals into GOAL agents. Sylvie Coste-Marquis and Pierre Marquis. Recovering Consistency by Forgetting Inconsistency Abstract: In this paper, we introduce and study a new paraconsistent inference relation $\models_c$ in the setting of 3-valued paraconsistent logics. Using inconsistency forgetting as a key mechanism for recovering consistency, it guarantees that the deductive closure $\models_c(\Sigma)$ of any belief base $\Sigma$ is classically consistent and classically closed. This strong feature, not shared by previous inference relations in the same setting, allows to interpret an inconsistent belief base as a set of classical worlds (hence to reason classically from them). David Billington. Propositional Clausal Defeasible Logic Abstract: Defeasible logics are non-monotonic reasoning systems that have efficient implementations and practical applications.  By listing several desirable properties we note that each defeasible logic fails to have some of these properties.  We define and explain a new defeasible logic, called clausal defeasible logic (CDL), which has all these properties.  CDL is easy to implement, consistent, detects loops, terminates, and has a range of different deduction algorithms to cater for a range of different intuitions. Laura Giordano, Valentina Gliozzi, Nicola Olivetti and Gian Luca Pozzato. Reasoning about typicality in preferential description logics Abstract: In this paper we propose a nonmonotonic extension ALC + Tmin of the Description Logic ALC for reasoning about prototypical properties and inheritance with exception. The logic ALC + Tmin is built upon a previously introduced (monotonic) logic ALC + T, that is obtained by adding a typicality operator T to ALC. The operator T is intended to select the "most normal" or "most typical" instances of a concept, so that knowledge bases may contain subsumption relations of the form "T(C ) is subsumed by P", expressing that typical C-members have the property P. In order to perform nonmonotonic inferences, we define a "minimal model" semantics ALC + Tmin for ALC + T. The intuition is that preferred, or minimal models are those that maximise typical instances of a concept. By means of ALC + Tmin we are able to infer defeasible properties of (explicit or implicit) individuals. We also present a tableau calculus for deciding ALC + Tmin entailment. Yi Zhou and Yan Zhang. Rule Calculus: Semantics, Axioms and Applications Abstract: We consider the problem of how a default rule can be deduced from a default theory. For this purpose, we propose an axiom system which precisely captures the deductive reasoning about default rules. We show that our axiomatic system is sound and complete under the semantics of the logic of here-and-there. We also study other important properties such as substitution and monotonicity of our system and prove the essential decision problem complexity. Finally, we discuss applications of our default rule calculus to various problems. Yi Zhou and Yan Zhang. Meta Level Reasoning and Default Reasoning Abstract: In this paper, we propose a logic framework for meta level reasoning as well as default reasoning in a general sense, based on an arbitrary underlying logic. In this framework, meta level reasoning is the task of how to deduce new meta level rules by given a set of rules, whilst default reasoning is the problem of what are the possible candidate beliefs by given them. We define the semantics for both meta level reasoning and default reasoning and investigate their relationships. We show that this framework captures various nonmonotonic paradigms, including answer set programming, default logic, contextual default reasoning, by applying the underlying logic into different classes. Finally, we show that this framework can be reduced into answer set programming. Fabio Cuzzolin. On the credal structure of consistent probabilities Abstract: In this paper we introduce a novel, simpler form of the polytope of inner Bayesian approximations of a belief function, or `consistent probabilities". We prove that the set of vertices of this polytope is generated by all possible permutations of elements of the domain, mirroring a similar behavior of outer consonant approximations. Renate Schmidt. Improved Second-Order Quantifier Elimination in Modal Logic Abstract: This paper  introduces improvements for second-order quantifier elimination methods based on Ackermann's Lemma and investigates their application in modal correspondence theory. In particular, we define refined calculi and procedures for solving the problem of eliminating quantified propositional symbols from modal formulae. We prove correctness results and use the approach to compute first-order frame correspondence properties for modal axioms and modal rules. Our approach can solve two new classes of formulae which have wider scope than existing classes known to be solvable by second-order quantifier elimination methods. Norihiro Kamide. Linear exponentials as resource operators: A decidable first-order linear logic with bounded exponentials Abstract: It is known that Girard's linear logics can elegantly represent the concept of "resource consumption". The linear exponential operator $!$ in linear logics can express a specific infinitely reusable resource (i.e., it is reusable not only for any number, but also many times).  It is also known that the propositional intuitionistic linear logic with $!$ and the first-order  intuitionistic linear logic without $!$ (called here ILL) are undecidable and  decidable, respectively. In this paper, a new decidable first-order intuitionistic linear logic, called the resource-indexed linear logic RL[$l$], is introduced by extending and generalizing ILL. The logic RL[$l$] has an $l$-bounded exponential operator $!_l$, and this operator can express a specific finitely usable resource (i.e., it is usable in any positive number less than $l+1$, but only once). The embedding theorem of RL[$l$] into ILL is proved, and by using this theorem, the cut-elimination and decidability theorems for RL[$l$] are shown. Novak Novakovic. Proof-theoretic Approach to Deciding Subsumption and Computing Least Common Subsumer in EL w.r.t. Hybrid TBoxes Abstract: Hybrid EL-TBoxes combine general concept inclusions (GCIs), which are interpreted with descriptive semantics, with cyclic concept definitions, which are interpreted with greatest fixpoint (gfp) semantics. We introduce a proof-theoretic approach that yields a polynomial-time decision procedure for subsumption, and present a proof-theoretic computation of least common subsumers in EL w.r.t. hybrid TBoxes. Jan Broersen, Rosja Mastop, John-Jules Meyer and Paolo Turrini. A logic for closed-world interaction Abstract: The aim of the work is to provide a language to reason about closed-world interaction, that is all those situations in which the outcomes of an interaction can be determined by the agents themselves and in which Nature does not play an active role. We formalize this intuition by identifying all such interactions and axiomatizing their logic. We apply the formal tools to reason about games and their regulation. Miki Hermann and Reinhard Pichler. Counting Complexity of Minimal Cardinality and Minimal Weight Abduction Abstract: Abduction is an important method of non-monotonic reasoning with many applications in artificial intelligence and related topics. In this paper, we concentrate on propositional abduction, where the background knowledge is given by a propositional formula. We have recently started to study the counting complexity of propositional abduction. However, several important cases have been left open, namely, the cases when we restrict ourselves to solutions with minimal cardinality or with minimal weight.  These cases -- possibly combined with priorities -- are now settled in this paper. We thus arrive at a complete picture of the counting complexity of propositional abduction. Conrad Drescher and Michael Thielscher. A Fluent Calculus Semantics for ADL with Plan Constraints Abstract: Plan constraints are the most recent addition to the ever growing Planning Domain Definition Language (PDDL). In this work we consider the PDDL fragment consisting of basic ADL extended by plan constraints. We provide a purely declarative semantics for this fragment by interpreting it in the basic Fluent Calculus. We thus obtain a logical semantics for this fragment of PDDL instead of the usual meta-theoretical state transition semantics. guillaume aucher. Consistency preservation and crazy formulas in BMS Abstract: We provide conditions under which seriality is preserved dur- ing an update in the BMS framework. We consider not only whether the entire updated model is serial but also whether its generated submod- els are serial. We also introduce the notion of crazy formulas which are formulas such that after being publicly announced at least one of the agents' beliefs become inconsistent. Satu Eloranta, Raul Hakli, Olli Niinivaara and Matti Nykänen. Accommodative Belief Revision Abstract: Accommodative revision is a novel method of non-prioritized belief revision. The epistemic state of an agent contains both knowledge that is immune to revision and beliefs that are allowed to change. Incoming information is first revised by the knowledge of the agent, and then the epistemic state of the agent is revised using this modified input. The properties of the method are studied and examples of its use are given. Henry Prakken. Combining Modes of Reasoning: an Application of Abstract Argumentation Abstract: Many reasoning problems involve subproblems that can be solved in different ways. Therefore, hybrid reasoning architectures have long been a research topic in AI. However, most work in this area has either focused on particular combinations of reasoning methods or has ignored the problem of handling alternative solutions to subproblems. The present paper  proposes an abstract framework for combining modes of reasoning and handling alternative solutions. It is argued that current abstract argumentation systems are either too abstract or too specific for this purpose, so that an intermediate level of abstraction is needed. Thomas Eiter, Georg Gottlob, Magdalena Ortiz and Mantas Simkus. Query Answering in the Description Logic Horn-SHIQ Abstract: We provide an ExpTime algorithm for answering conjunctive queries (CQs) in Horn-SHIQ, a Horn fragment of the well-known Description Logic SHIQ underlying the OWL-Lite standard. The algorithm employs a domino system for model representation, which is constructed via a worst-case optimal tableau algorithm for Horn-SHIQ; the queries are answered by reasoning over the domino system. Our algorithm not only shows that CQ answering in Horn-SHIQ is not harder than satisfiability testing, but also that it is polynomial in data complexity, making Horn-SHIQ an attractive expressive Description Logic. Laura Bozzelli and Ruggero Lanotte. Complexity and Succinctness issues  for linear-time hybrid logics Abstract: Full linear-time hybrid logic (\HL) is a non-elementary and equally expressive extension of standard LTL + past obtained by adding the well-known binder operators $\downarrow$ and $\exists$. We investigate complexity and succinctness issues for \HL in terms of the number of variables and nesting depth of binder modalities. First, we present automata-theoretic decision procedures for  satisfiability and model-checking of $\HL$, which  require space of exponential height equal to the nesting depth of binder modalities. The proposed algorithms are proved to be   asymptotically optimal by providing matching lower bounds. Second, we show that   for the one-variable fragment of $\HL$, the considered problems are elementary and, precisely, \EXPSPACE-complete. Finally, we show that for all \$0\leq h

#### Contact:

If you have any queries please contact the organizers at

Further information about JELIA 2008 is available at: www.jelia.eu/2008.