## 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<k$, there is a succinctness gap between the fragments $\HL^k$ and $\HL^h$ with binder nesting depth at most $k$ and $h$, respectively, of exponential height equal to $k-h$. |

Paul-Amaury Matt and Francesca Toni. On Games of Strategy in Abstract Argumentation Frameworks |

Abstract: This paper is concerned with the problem of quantifying the strength of arguments in controversial debates represented as abstract argumentation frameworks (Dung 1995). Standard approaches to abstract argumentation provide a qualitative account of the status of arguments in debates, whilst a numerical measures of argument strength may provide a sharper assessment of the individual status of arguments composing a debate. In order to measure argument strength, we combine ideas from abstract argumentation with Game Theory. For any given abstract argumentation framework and chosen argument in that framework, we introduce a zero-sum two-person game of imperfect information opposing a proponent to an opponent of the argument. The game's value (proponent's payoff on the long run) is adopted as measure of the chosen argument's strength. This value fundamentally reflects the average degree of acceptability of the extensions embracing the argument versus those attacking it. We then exploit von Neumann's minimax theorem to derive several important properties of this new argument strength measure. |

Felicidad Aguado, Pedro Cabalar, Gilberto Perez and Concepcion Vidal. Strongly Equivalent Temporal Logic Programs |

Abstract: This paper analyses the idea of strong equivalence for transition systems represented as logic programs under the Answer Set Programming (ASP) paradigm. To check strong equivalence, we use a linear temporal extension of Equilibrium Logic (a logical characterisation of ASP) and its monotonic basis, the intermediate logic of Here-and-There (HT). Trivially, equivalence in this temporal extension of HT provides a sufficient condition for temporal strong equivalence and, as we show in the paper, it can be transformed into a provability test into the standard Linear Temporal Logic (LTL), something that can be automatically checked using any of the LTL available provers. The paper shows an example of the potential utility of this method by detecting some redundant rules in a simple actions reasoning scenario. |

Sébastien Konieczny and Ramon Pino Perez. Confluence operators |

Abstract: In the logic based framework of knowledge representation and reasoning many operators have been defined in order to capture different kinds of change: revision, update, merging and many others. There are close links between revision, update, and merging. Merging operators can be considered as extensions of revision operators to multiple belief bases. And update operators can be considered as pointwise revision, looking at each model of the base, instead of taking the base as a whole. Thus, a natural question is the following one: Are there natural operators that are pointwise merging, just as update are pointwise revision? The goal of this work is to give a positive answer to this question. In order to do that, we introduce a new class of operators: the confluence operators. These new operators can be useful in modelling negotiation process. |

Christoph Wernhard. Polarity Sensitive Predicate Quantifiers |

Abstract: A polarity sensitive predicate quantifier permits to quantify upon a predicate only in positive or negative polarity. Occurrences of the predicate in literals with the complementary polarity are considered as unquantified predicate symbols. Literal projection and literal forgetting are related concepts. We present a formalization of these notions for first-order logic with a Herbrand semantics, which makes them easy to access, since they are expressed there by means of straightforward relationships between sets of literals. We use the formalization to show properties of polarity sensitive predicate quantification which apply to formulas that are free of certain links, pairs of literals with complementary instances, each in a different conjunct of a conjunction or both in the scope of a universal first-order quantifier. Such properties can justify the application of methods that construct formulas without certain links (for example tableau methods) to the elimination of polarity sensitive predicate quantifiers. |

Annamaria Bria, Wolfgang Faber and Nicola Leone,. Normal Form Nested Programs |

Abstract: Disjunctive logic programming under the answer set semantics (DLP, ASP) has been acknowledged as a versatile formalism for knowledge representation and reasoning during the last decade. Lifschitz, Tang, and Turner have introduced an extended language of DLP, called Nested Logic Programming (NLP), in 1999. It often allows for more concise representations by permitting a richer syntax in rule heads and bodies. However, that language is propositional and thus does not allow for variables, one of the strengths of DLP. In this paper, we introduce a language similar to NLP, called Normal Form Nested (NFN) programs, which does allow for variables, and present the syntax and semantics. With the presence of variables, however, domain independence is no longer guaranteed. We study this issue in depth and define the class of safe NFN programs, which are guaranteed to be domain independent. Moreover, we show that for NFN programs which are also NLPs, our semantics coincides with the one of Lifschitz, Tang, and Turner. Finally, we provide an algorithm which translates NFN programs into DLP programs, and does so in an efficient way, allowing for the effective implementation of the NFN language on top of existing DLP systems. |

Jérôme Mengin, Meghyn Bienvenu and Andreas Herzig. Uniform interpolation by resolution in modal logic |

Abstract: The problem of computing a uniform interpolant of a given formula on a sublanguage is known in Artificial Intelligence as variable forgetting. In propositional logic, there are well known methods for performing variable forgetting. Variable forgetting is more involved in modal logics, because one must forget a variable not in one world, but in several worlds. It has been shown that modal logic K has the uniform interpolation property, and a method has recently been proposed for forgetting variables in a modal formula (of mu-calculus) given in disjunctive normal form. However, there are cases where information comes naturally in a more conjunctive form. In this paper, we propose a method, based on an extension of resolution to modal logics, to perform variable forgetting for formulae in conjunctive normal form, in the modal logic K. |

Magdalena Ortiz. Extending CARIN to the Description Logics of the SH Family |

Abstract: This work studies the extension of the existential entailment algorithm of CARIN to DLs of the SH family. The CARIN family of knowledge representation languages was one of the first hybrid languages combining Datalog rules and Description Logics. For reasoning in one of its prominent variants, which combines ALCNR with non-recursive Datalog, the blocking conditions of the standard tableaux procedure for ALCNR were modified. Here we discuss a similar adaptation to the SHOIQ tableaux, which provides some new decidability results and tight data complexity bounds for reasoning in non-recursive CARIN, as well as for query answering over Description Logic knowledge bases. |

#### Contact:

If you have any queries please contact the organizers at

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