Ontology languages are an important method to represent knowledge. A description logic has di culty reasoning under inconsistent information, as well as providing an explanation of how a result of a query is reached and why it is acceptable. Justi cation has been shown to be an e ective type of explanation to bring about changes in the system [7]. Formal argumentation, as a method for handling reasoning with inconsistent information, provides various ways to explain why a claim is justi ed, which makes it a promising tool to solve the problems above. ASP IC+ [5, 6] is a rule based argumentation framework, in which ( nite) arguments are constructed by strict or defeasible rules from the set of premises. Strict rules are applied to model certain inferences, while defeasible rules are applied to model uncertain inferences. ASP IC+ can resolve con icts between arguments by preferences, and can evaluate whether an argument is acceptable based on abstract argumentation frameworks and argumentation semantics [2]. For more details, please see [5, 6, 1, 2]. Compared with other applicable argumentation systems, such as DeLP [3], in this paper we chose ASP IC+ because: 1) it supports modeling di erent types of attack relations between arguments (i.e., rebutting, undermining and undercutting), and hence can more exibly express inconsistency; 2) it supports skeptical and credulous justi cation, which can re ect users' di erent attitudes. For the reasons above, we propose deriving an argumentation theory called DL-AT , which translates a DL ontology into ASPIC+. What's more, we propose a novel de nition of explanation. This paper considers ontology based on ALC expression. To translate a DL ontology into an argumentation theory (AT), the logical language L of AT represents concepts C as unary predicates C(x), while the roles P are represented as binary predicates P (x; y). For ABox assertions, x, y are individuals, and formulas in ABox are contained in the set of premises K in DL-AT . As for the TBox, inspired by [4], we interpret the declarations in it as strict/defeasible rules in the set R of AT as shown in Table 1, where C, D are basic concepts, P , Q are roles, ? We would like to thank the anonymous reviewers of DL 2020 for their valuable comments. This work is supported by the China Postdoctoral Science Foundation [No. 2019M663353], the MOE Project of Key Research Institute of Humanities and Social Sciences in Universities [No. 18JJD720005] and the Fundamental Research Funds for the Central Universities of China [No. 20wkpy104]. Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
x, y are individuals and , are free variables. ! and ) denote strict rules and defeasible rules respectively. According to speci ed context, a formula can only be translated to one type of rule.
De nition 1. Let = (T; A) be a DL ontology, a DL-AT = (L; RT ; KA) is an argumentation theory constructed with , such that RT is the set of rules corresponding to T based on Table 1, and KA is the set of premises based on A.
Based on De nition 1, arguments can be constructed by rules in RT from the set of premises KA.
According to paper [
De nition 2. Given a DL-AT = (L; RT ; KA), let A be the set of all the argument constructed based on it. An assertion X is skeptically/credulously acceptable under certain argumentation semantics S, i 9A 2 A, s.t. A is skeptically/credulously justi ed w.r.t. ES and Conc(A) = X.
De nition 2 translates the query about whether an assertion X is acceptable in DL-AT into the query about whether an argument A whose conclusion is X is acceptable. The evaluation of this assertion corresponds to the evaluation of argument A. Based on De nition 2, the following de nition shows how to perform a traditional reasoning task (instances checking). Due to space restriction, de nitions for other reasoning tasks are omitted.
Argumentation Theory for Reasoning with Inconsistent Ontologies De nition 3. Let ' be an individual, skeptically or credulously, it holds that ' is an instance of class: { C (/:C), i 9A 2 A, s.t. A is skeptically/credulously justi ed w.r.t. ES and
Conc(A) = C(')(=:C('); { C u D, i 9A; B 2 A s.t. A and B are both skeptically/credulously justi ed w.r.t. ES and Conc(A) = C('), Conc(B) = D('); { C t D, i 9A; B 2 A s.t. at least one of A and B are skeptically/credulously justi ed w.r.t. ES and Conc(A) = C('), Conc(B) = D('); { 9P:D, i 9A; B 2 A s.t. A and B are both skeptically/credulously justi ed w.r.t. ES and Conc(A) = P ('; x), Conc(B) = D(x) (x is an individual); { 8P:D, i 1) 9A 2 A s.t. Conc(A) = P ('; x); and 2) 8A 2 fAjConc(A) = P ('; x)g, 9B 2 A, s.t. Conc(B) = D(x).
According to De nition 3, the query about whether an instance is a member of a complex concept can be divided into several queries about whether this instance is a member of some basic concepts, while these answers can be obtained based on De nition 2.
At last, we de ne the explanation of the acceptance of an assertion as follows. De nition 4 (Explanation). Assuming that X is a skeptically/credulously acceptable assertion under certain argumentation semantics S, then 9A 2 A s.t. Conc(A) = X, { the explanation of how this assertion is reached is P rem(A) [ Rule(A); { the explanation of why this assertion is acceptable is P rem(B) [ Rule(B), s.t. 8C 2 A, if C successfully attacks A, then B successfully attacks C.
De nition 4 gives a formal explanation of why an assertion X concluded by argument A is acceptable, which consists of two parts. The rst part explains how X is reached by presenting all the premises contained in KA and all the rules contained in RT that applied to construct argument A. In other words, it indicates all the declarations contained in the ABox and TBox of DL ontology that used to conclude X. The second part explains why this assertion is acceptable by presenting all the premises and rules applied to construct the arguments defend A. Similarly, this explanation indicates all the relevant declarations of DL ontology.
In summary, we propose an argumentation theory called DL-AT to handle reasoning with inconsistent ontology, and provide a formal de nition of explanation. In future work, we will explore how to apply our approach to some more expressive description languages, such as SHI.