Logics in Artificial Intelligence

Justification Logic offers a new approach to a theory of knowledge, belief, and evidence, which possesses the potential to have significant impact on applications. The celebrated account of

knowledge

as

justified true belief

, which is attributed to Plato, has long been a focus of epistemic studies (cf. [10,15,18,26,30,32] and many others).

This talk is half-way between a survey and a report on ongoing research, most of which is joint work with Vincent Conitzer and Lirong Xia. The first part of the talk owes a lot to two survey papers co-authored with Yann Chevaleyre, Ulle Endriss and Nicolas Maudet [5,6].

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.

We provide conditions under which seriality is preserved during an update in the BMS framework. We consider not only whether the entire updated model is serial but also whether its generated submodels 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.

Defeasible logics are non-monotonic reasoning systems that have efficient implementations and practical applications. We list several desirable properties and 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 deduction algorithms to cater for a range of intuitions.

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 ↓ and ∃. We investigate complexity and succinctness issues for

HL

in terms of the number of variables and nesting depth of binder modalities. First, we present

direct

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 ≤ 

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

.

The study of interval temporal logics on linear orders is a meaningful research area in computer science and artificial intelligence. Unfortunately, even when restricted to propositional languages, most interval logics turn out to be undecidable. Decidability has been usually recovered by imposing severe syntactic and/or semantic restrictions. In the last years, tableau-based decision procedures have been obtained for logics of the temporal neighborhood and logics of the subinterval relation 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

whole

class of linearly ordered domains.

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 [1]. 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 (

NPN

) programs, which does allow for variables, and present the syntax and semantics. With the presence of variables, domain independence is no longer guaranteed. We study this issue in depth and define the class of safe

NPN

programs, which are guaranteed to be domain independent. Moreover, we show that for

NPN

programs which are also

NLP

s, our semantics coincides with the one of [1]; while keeping the standard meaning of answer sets on DLP programs with variables. Finally, we provide an algorithm which translates

NPN

programs into

DLP

programs, and does so in an efficient way, allowing for the effective implementation of the

NPN

language on top of existing DLP systems.

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.

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.

In this paper, we introduce and study a new paraconsistent inference relation ⊧ 

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

$Cn_{\models_c}(\Sigma)$

of any belief base

Σ

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).

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.

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.

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.

We provide an

ExpTime

algorithm for answering conjunctive queries (CQs) in

Horn

-

$\mathcal{SHIQ}$

, a Horn fragment of the well-known Description Logic

$\mathcal{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

-

$\mathcal{SHIQ}$

; the queries are answered by reasoning over the domino system. Our algorithm not only shows that CQ answering in

Horn

-

$\mathcal{SHIQ}$

is not harder than satisfiability testing, but also that it is polynomial in data complexity, making

Horn

-

$\mathcal{SHIQ}$

an attractive expressive Description Logic.

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.

In this paper we propose a nonmonotonic extension

of the Description Logic

$\mathcal{ALC}$

for reasoning about prototypical properties and inheritance with exception. The logic

is built upon a previously introduced (monotonic) logic

, that is obtained by adding a typicality operator

T

to

$\mathcal{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

for

. The intuition is that preferred, or minimal models are those that maximise typical instances of concepts. By means of

we are able to infer defeasible properties of (explicit or implicit) individuals. We also present a tableau calculus for deciding

entailment.

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.

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

.

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.

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.

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 semantics 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.

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 processes.

Abstract argumentation (Dung 1995) is a theory of dialectic that allows us to formalise and study various notions of argument acceptability. We depart from this standard approach and formalise a measure of argument strength by applying the concept of value of a game, as defined in Game Theory (von Neumann 1928). The measure thus obtained satisfies a number of intuitively appealing properties that can be derived mathematically from the minimax theorem.

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” [7]. 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.

Hybrid

$\cal 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

$\cal EL$

w.r.t. hybrid TBoxes.

This work studies the extension of the

existential entailment algorithm

of

Carin

to DLs of the

$\mathcal{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

$\mathcal{ALCNR}$

with non-recursive

Datalog

, the blocking conditions of the standard tableaux procedure for

$\mathcal{ALCNR}$

were modified. Here we discuss a similar adaptation to the

$\mathcal{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.

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.

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.

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

$\mathcal{SHOIQ}$

and

$\mathcal{SROIQ}$

, serving as the logical underpinning of OWL and the forthcoming OWL 2, can accommodate arbitrary Boolean expressions. The prominent OWL-fragment

$\mathcal{SHIQ}$

can be safely extended by safe role expressions, and the tractable fragments

$\mathcal{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.

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.

The computation of literal projection generalizes predicate quantifier elimination by permitting, so to speak, quantifying upon an arbitrary sets of ground literals, instead of just (all ground literals with) a given predicate symbol. Literal projection allows, for example, to express predicate quantification upon a predicate just in positive or negative polarity. Occurrences of the predicate in literals with the complementary polarity are then considered as unquantified predicate symbols. We present a formalization of literal projection and related concepts, such as literal forgetting, for first-order logic with a Herbrand semantics, which makes these notions easy to access, since they are expressed there by means of straightforward relationships between sets of literals. With this formalization, we show properties of literal projection which hold for formulas that are free of certain links, pairs of literals with complementary instances, each in a different conjunct of a conjunction, both in the scope of a universal first-order quantifier, or one in a subformula and the other in its context formula. These properties can justify the application of methods that construct formulas without such links to the computation of literal projection. Some tableau methods and direct methods for second-order quantifier elimination can be understood in this way.

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 giving a set of rules, whilst default reasoning is the problem of what are the possible candidate beliefs by giving 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 to different classes. Finally, we show that this framework can be reduced into answer set programming.

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.