We investigate the decidability and computational complexity of conservative extensions and the related notions of inseparability and entailment in Horn description logics (DLs) with inverse roles. We consider both query conservative extensions, defined by requiring that the answers to all conjunctive queries are left unchanged, and deductive conservative extensions, which require that the entailed concept inclusions, role inclusions, and functionality assertions do not change. Upper bounds for query conservative extensions are particularly challenging because characterizations in terms of unbounded homomorphisms between universal models, which are the foundation of the standard approach to establishing decidability, fail in the presence of inverse roles. We resort to a characterization that carefully mixes unbounded and bounded homomorphisms and enables a decision procedure that combines tree automata and a mosaic technique. Our main results are that query conservative extensions are 2ExpTime-complete in all DLs between ELI and Horn-ALCHIF and between Horn-ALC and Horn-ALCHIF, and that deductive conservative extensions are 2ExpTime-complete in all DLs between ELI and ELHIF_\bot. The same results hold for inseparability and entailment.
Centre for Artificial Intelligence Research（人工智能研究中心）；University of KwaZulu-Natal（夸祖鲁-纳塔尔大学）；CSIR Meraka Institute（科学与工业研究理事会梅拉卡研究所）
Standard belief change assumes an underlying logic containing full classical propositional logic. However, there are good reasons for considering belief change in less expressive logics as well. In this paper we build on recent investigations by Delgrande on contraction for Horn logic. We show that the standard basic form of contraction, partial meet, is too strong in the Horn case. This result stands in contrast to Delgrande's conjecture that orderly maxichoice is the appropriate form of contraction for Horn logic. We then define a more appropriate notion of basic contraction for the Horn cas…
CNRS（法国国家科学研究中心）；Inria（法国国家信息与自动化研究所）；University of Bremen（不来梅大学）；University of Liverpool（利物浦大学）
We study FO-rewritability of conjunctive queries in the presence of ontologies formulated in a description logic between EL and Horn-SHIF, along with related query containment problems. Apart from providing characterizations, we establish complexity results ranging from ExpTime via NExpTime to 2ExpTime, pointing out several interesting effects. In particular, FO-rewriting is more complex for conjunctive queries than for atomic queries when inverse roles are present, but not otherwise.
We study the problem of rewriting an ontology O1 expressed in a DL L1 into an ontology O2 in a Horn DL L2 such that O1 and O2 are equisatisfiable when extended with an arbitrary dataset. Ontologies that admit such rewritings are amenable to reasoning techniques ensuring tractability in data complexity. After showing undecidability whenever L1 extends ALCF, we focus on devising efficiently checkable conditions that ensure existence of a Horn rewriting. By lifting existing techniques for rewriting Disjunctive Datalog programs into plain Datalog to the case of arbitrary first-order programs with …
Saarland University（萨尔大学）；University of Freiburg（弗莱堡大学）
State constraints in AI Planning globally restrict the legal environment states. Standard planning languages make closed-domain and closed-world assumptions. Here we address open-world state constraints formalized by planning over a description logic (DL) ontology. Previously, this combination of DL and planning has been investigated for the light-weight DL DL-Lite. Here we propose a novel compilation scheme into standard PDDL with derived predicates, which applies to more expressive DLs and is based on the rewritability of DL queries into Datalog with stratified negation. We also provide a ne…
Aix Marseille Université（艾克斯-马赛大学）；CNRS（法国国家科学研究中心）；Vienna University of Technology（维也纳工业大学）
Recently, belief change within the framework of fragments of propositional logic has gained increasing attention. Previous works focused on belief contraction and belief revision on the Horn fragment. However, the problem of belief merging within fragments of propositional logic has been neglected so far. This paper presents a general approach to define new merging operators derived from existing ones such that the result of merging remains in the fragment under consideration. Our approach is not limited to the case of Horn fragment but applicable to any fragment of propositional logic charact…
Free University of Bozen-Bolzano（博岑-博尔扎诺自由大学）；University of Liverpool（利物浦大学）；University of Bremen（不来梅大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
The question whether an ontology can safely be replaced by another, possibly simpler, one is fundamental for many ontology engineering and maintenance tasks. It underpins, for example, ontology versioning, ontology modularization, forgetting, and knowledge exchange. What safe replacement means depends on the intended application of the ontology. If, for example, it is used to query data, then the answers to any relevant ontology-mediated query should be the same over any relevant data set; if, in contrast, the ontology is used for conceptual reasoning, then the entailed subsumptions between co…
Centrale Supelec（中央理工-高等电力学院）；Université Paris-Saclay（巴黎萨克雷大学）；Université Paris-Dauphine（巴黎多芬大学）；CNRS（法国国家科学研究中心）；Télécom ParisTech（巴黎电信学院）
Belief revision of knowledge bases represented by a set of sentences in a given logic has been extensively studied but for specific logics, mainly propositional, and also recently Horn and description logics. Here, we propose to generalize this operation from a model-theoretic point of view, by defining revision in an abstract model theory known under the name of satisfaction systems. In this framework, we generalize to any satisfaction systems the characterization of the well known AGM postulates given by Katsuno and Mendelzon for propositional logic in terms of minimal change among interpret…
In this paper we present the new logic programming language DALI, aimed at defining agents and agent systems. A main design objective for DALI has been that of introducing in a declarative fashion all the essential features, while keeping the language as close as possible to the syntax and semantics of the plain Horn--clause language. Special atoms and rules have been introduced, for representing: external events, to which the agent is able to respond (reactivity); actions (reactivity and proactivity); internal events (previous conclusions which can trigger further activity); past and present …
Answer-set programming (ASP) has emerged recently as a viable programming paradigm. We describe here an ASP system, DATALOG with constraints or DC, based on non-monotonic logic. Informally, DC theories consist of propositional clauses (constraints) and of Horn rules. The semantics is a simple and natural extension of the semantics of the propositional logic. However, thanks to the presence of Horn rules in the system, modeling of transitive closure becomes straightforward. We describe the syntax, use and implementation of DC and provide experimental results.
Artificial Intelligence Research Institute (IIIA) - CSIC（人工智能研究所 (IIIA) - CSIC）
The expressiveness of propositional non-clausal (NC) formulas is exponentially richer than that of clausal formulas. Yet, clausal efficiency outperforms non-clausal one. Indeed, a major weakness of the latter is that, while Horn clausal formulas, along with Horn algorithms, are crucial for the high efficiency of clausal reasoning, no Horn-like formulas in non-clausal form had been proposed. To overcome such weakness, we define the hybrid class $\mathbb{H_{NC}}$ of Horn Non-Clausal (Horn-NC) formulas, by adequately lifting the Horn pattern to NC form, and argue that $\mathbb{H_{NC}}$, along wit…
University of Leipzig（莱比锡大学）；Leipzig University of Applied Sciences（莱比锡应用科技大学）；Paderborn University（帕德博恩大学）
Graph representations of large knowledge bases may comprise billions of edges. Usually built upon human-generated ontologies, several knowledge bases do not feature declared ontological rules and are far from being complete. Current rule mining approaches rely on schemata or store the graph in-memory, which can be unfeasible for large graphs. In this paper, we introduce HornConcerto, an algorithm to discover Horn clauses in large graphs without the need of a schema. Using a standard fact-based confidence score, we can mine close Horn rules having an arbitrary body size. We show that our method…
The limit behavior of inductive logic programs has not been explored, but when considering incremental or online inductive learning algorithms which usually run ongoingly, such behavior of the programs should be taken into account. An example is given to show that some inductive learning algorithm may not be correct in the long run if the limit behavior is not considered. An inductive logic program is convergent if given an increasing sequence of example sets, the program produces a corresponding sequence of the Horn logic programs which has the set-theoretic limit, and is limit-correct if the…
Universität Bremen（不来梅大学）；Universiteit van Amsterdam（阿姆斯特丹大学）；University of Liverpool（利物浦大学）
We study complete approximations of an ontology formulated in a non-Horn description logic (DL) such as $\mathcal{ALC}$ in a Horn DL such as~$\mathcal{EL}$. We provide concrete approximation schemes that are necessarily infinite and observe that in the $\mathcal{ELU}$-to-$\mathcal{EL}$ case finite approximations tend to exist in practice and are guaranteed to exist when the original ontology is acyclic. In contrast, neither of this is the case for $\mathcal{ELU}_\bot$-to-$\mathcal{EL}_\bot$ and for $\mathcal{ALC}$-to-$\mathcal{EL}_\bot$ approximations. We also define a notion of approximation …
A General Sufficient Condition for Rewriting Horn-ALCHI Atomic Queries into GQL
LIRMM（蒙彼利埃计算机科学、机器人学与微电子实验室）；Inria（法国国家信息与自动化研究所）；University of Montpellier（蒙彼利埃大学）；CNRS（法国国家科学研究中心）；DI ENS（巴黎高等师范学院信息学系）；ENS（巴黎高等师范学院）；PSL University（巴黎文理研究大学）
Answer-set programming (ASP) has emerged recently as a viable programming paradigm well attuned to search problems in AI, constraint satisfaction and combinatorics. Propositional logic is, arguably, the simplest ASP system with an intuitive semantics supporting direct modeling of problem constraints. However, for some applications, especially those requiring that transitive closure be computed, it requires additional variables and results in large theories. Consequently, it may not be a practical computational tool for such problems. On the other hand, ASP systems based on nonmonotonic logics,…
In this paper we reexamine the place and role of stable model semantics in logic programming and contrast it with a least Herbrand model approach to Horn programs. We demonstrate that inherent features of stable model semantics naturally lead to a logic programming system that offers an interesting alternative to more traditional logic programming styles of Horn logic programming, stratified logic programming and logic programming with well-founded semantics. The proposed approach is based on the interpretation of program clauses as constraints. In this setting programs do not describe a singl…
In this paper we propose a framework for combining Disjunctive Logic Programming and Poole's Probabilistic Horn Abduction. We use the concept of hypothesis to specify the probability structure. We consider the case in which probabilistic information is not available. Instead of using probability intervals, we allow for the specification of the probabilities of disjunctions. Because minimal models are used as characteristic models in disjunctive logic programming, we apply the principle of indifference on the set of minimal models to derive default probability values. We define the concepts of …
Institut für Logic and Computation（逻辑与计算研究所）；Technische Universität Wien（维也纳技术大学）；Marmara University（马尔马拉大学）
We study abduction in First Order Horn logic theories where all atoms can be abduced and we are looking for preferred solutions with respect to three objective functions: cardinality minimality, coherence, and weighted abduction. We represent this reasoning problem in Answer Set Programming (ASP), in order to obtain a flexible framework for experimenting with global constraints and objective functions, and to test the boundaries of what is possible with ASP. Realizing this problem in ASP is challenging as it requires value invention and equivalence between certain constants, because the Unique…
Conjunctive query answering over expressive Horn Description Logic ontologies is a relevant and challenging problem which, in some cases, can be addressed by application of the chase algorithm. In this paper, we define a novel acyclicity notion which provides a sufficient condition for termination of the restricted chase over Horn-SRIQ TBoxes. We show that this notion generalizes most of the existing acyclicity conditions (both theoretically and empirically). Furthermore, this new acyclicity notion gives rise to a very efficient reasoning procedure. We provide evidence for this by providing a …
The dynamics of belief and knowledge is one of the major components of any autonomous system that should be able to incorporate new pieces of information. In order to apply the rationality result of belief dynamics theory to various practical problems, it should be generalized in two respects: first it should allow a certain part of belief to be declared as immutable; and second, the belief state need not be deductively closed. Such a generalization of belief dynamics, referred to as base dynamics, is presented in this paper, along with the concept of a generalized revision algorithm for knowl…
Stony Brook University（石溪大学）；University of Toronto（多伦多大学）
In this paper we present efficient evaluation algorithms for the Horn Transaction Logic (a generalization of the regular Horn logic programs with state updates). We present two complementary methods for optimizing the implementation of Transaction Logic. The first method is based on tabling and we modified the proof theory to table calls and answers on states (practically, equivalent to dynamic programming). The call-answer table is indexed on the call and a signature of the state in which the call was made. The answer columns contain the answer unification and a signature of the state after t…
Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of (possibly irregular) infinite data. Both instances of coinductive reasoning appeared in the literature before, but a systematic analysis of these two kinds of proofs and of their relation was lacking. We propose a general proof-theoretic framework for handling both kinds of coinduction arising in Horn clause logic. To this aim, we propose a coinductive extension of Miller et al's framework of uniform proofs and prove its soundness relative to co…
Universität Bremen（不来梅大学）；University of Liverpool（利物浦大学）
We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform inter- polants and their existence in terms of bisimula- tions, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model- theoretic and automata-theoretic methods that, as a by-product, also provides characterizations of and decision procedures for conservative extensions.
The dynamics of belief and knowledge is one of the major components of any autonomous system that should be able to incorporate new pieces of information. In order to apply the rationality result of belief dynamics theory to various practical problems, it should be generalized in two respects: first it should allow a certain part of belief to be declared as immutable; and second, the belief state need not be deductively closed. Such a generalization of belief dynamics, referred to as base dynamics, is presented in this paper, along with the concept of a generalized revision algorithm for knowl…
We report complexity results about redundancy of formulae in 2CNF form. We first consider the problem of checking redundancy and show some algorithms that are slightly better than the trivial one. We then analyze problems related to finding irredundant equivalent subsets (I.E.S.) of a given set. The concept of cyclicity proved to be relevant to the complexity of these problems. Some results about Horn formulae are also shown.
Distilling from a knowledge base only the part that is relevant to a subset of alphabet, which is recognized as forgetting, has attracted extensive interests in AI community. In standard propositional logic, a general algorithm of forgetting and its computation-oriented investigation in various fragments whose satisfiability are tractable are still lacking. The paper aims at filling the gap. After exploring some basic properties of forgetting in propositional logic, we present a resolution-based algorithm of forgetting for CNF fragment, and some complexity results about forgetting in Horn, ren…
Lehigh University Computer Science and Engineering（莱维大学计算机科学与工程系）；Los Angeles Pierce College Computer Science（洛杉矶派克学院计算机科学）；Colorado College Computer Science（科罗拉多学院计算机科学）
Dependence is an important concept for many tasks in artificial intelligence. A task can be executed more efficiently by discarding something independent from the task. In this paper, we propose two novel notions of dependence in propositional logic: formula-formula dependence and formula forgetting. The first is a relation between formulas capturing whether a formula depends on another one, while the second is an operation that returns the strongest consequence independent of a formula. We also apply these two notions in two well-known issues: belief update and conservative extension. Firstly…
Artificial Intelligence Research Institute (IIIA) - CSIC（人工智能研究所 (IIIA) - CSIC）
The relevance of polynomial formula classes to deductive efficiency motivated their search, and currently, a great number of such classes is known. Nonetheless, they have been exclusively sought in the setting of clausal form and propositional logic, which is of course expressively limiting for real applications. As a consequence, a first polynomial propositional class in non-clausal (NC) form has recently been proposed. Along these lines and towards making NC tractability applicable beyond propositional logic, firstly, we define the Regular many-valued Horn Non-Clausal class, or RH, obtained …
