Paraconsistent OWL and Related Logics

Paper Title: 
Paraconsistent OWL and Related Logics
Authors: 
Frederick Maier, Yue Ma, and Pascal Hitzler
Abstract: 
The Web Ontology Language OWL is currently the most prominent formalism for representing ontologies in Semantic Web applications. OWL is based on description logics, and automated reasoners are used to infer knowledge implicitly present in OWL ontologies. However, because typical description logics obey the classical principle of explosion, reasoning over inconsistent ontologies is impossible in OWL. This is so despite the fact that inconsistencies are bound to occur in many realistic cases, e.g., when multiple ontologies are merged or when ontologies are created by machine learning or data mining tools. In this paper, we present four-valued paraconsistent description logics which can reason over inconsistencies. We focus on logics corresponding to OWL DL and its profiles. We present the logic SROIQ4, showing that it is both sound relative to classical SROIQ and that its embedding into SROIQ is consequence preserving. We also examine paraconsistent varieties of EL++, DL-Lite, and Horn-DLs. The general framework described here has the distinct advantage of allowing classical reasoners to draw sound but nontrivial conclusions from even inconsistent knowledge bases. Truth-value gaps and gluts can also be selectively eliminated from models (by inserting additional axioms into knowledge bases). If gaps but not gluts are eliminated, additional classical conclusions can be drawn without aaffecting paraconsistency.
Full PDF Version: 
Submission type: 
Full Paper
Responsible editor: 
Krzysztof Janowicz
Decision/Status: 
Accept
Reviews: 

Review 1 by anonymous reviewer

I've checked the new version of the paper; it has been greatly improved with several examples, so I am now satisfied.

The reviews below are for the second round review, which resulted in an accept with minor revisions. The current manuscript is the subsequent revised submission.

Review 1 by anonymous reviewer
The authors addressed my issues and from my point of view the paper is fine now.

Review 2 by anonymous reviewer

Recommendation: New revision

The initial review raised several issues; in the following, each issue will be
revisited, along with a discussion of how the authors addressed them:

1) Confusion over what material is new w.r.t. other related publications:

The authors provided an adequate description of what is new in their response, and
appear to have updated the manuscript accordingly.

2) Empirical evaluation:

The small changes requested regarding clarifications were addressed satisfactorily.

The authors did not agree with the need to expand the content of this section, and offered
to remove the section completely. Though this is ultimately up to the authors, doing so would
perhaps compromise the amount of new material.

3) Examples and readability:

In their response, the authors claim that examples are short because this is a theoretical
paper and they are mainly used to show that properties do not hold. I would argue that the
fact that it is a theoretical paper actually means that examples are even more important, since
they help along the discussion and allow the reader to ground the more abstract parts.
Though whether or not to devise a running example (as originally suggested) is up to the authors,
revising the current ones (adding comments on what the example is conveying) and adding at least
one or two that focus on illustrating concepts (not using p, q, etc) is necessary to motivate the
presentation and make the paper readable by people who are not specialists in the topic.

4) Related work:

The discussion has been revised and extended, and is now greatly improved.

5) Other minor comments:

I still believe that the word "argument" as used in the manuscript is confusing; the
authors claim that other words like "conditional" or "implication" would be worse since
they may be confused by formal statements of a logic; however, the authors are doing
just that. The word "argument" could be confused with its use in the area of Argumentation
(as a dialectical form of reasoning, such as in the work of Anthony Hunter et al., and similar in
spirit to the work of Jaskowski now being cited by the authors). I may be completely misunderstanding
the authors' use of the term, but if this is the case, it only reinforces my point.

Apart from this, the other original minor comments have all apparently been adequately addressed.

SUMMARY:

I recommend a second revision in order to address point (3) above, i.e., commenting on the existing
examples and adding one or two illustrative ones.

The reviews below are for the original submission.

Review 1 by anonymous reviewer

The paper discusses paracosnistent OWL 2 and their profiles, based on Belnap’s four-valued logic.

The paper is well-written, self-contained and pleasant to read. While it appears as a summary of previous papers, I still think that it is worthwhile to publish it.

I’ve only some concerns on some Propositions that I think do not hold: specifically Propositions 33, 34, 36. However, they are of marginal interest. Anyway, in case I’m wrong, I'm sorry. In that case, counter argument my counter-examples. In case I’m right, just drop these propositions and place the counter-examples as examples.

Other minor corrections are in the annotated pdf as attachment.

I recommend: Accept with minor revision and I would like to see the author's revision.

The reviewer provided an annotated PDF document containing more details and corrections.

Review 2 by anonymous reviewer

Paper Title: Paraconsistent OWL and Related Logics

Auhors: Frederick Maier, Yue Ma, and Pascal Hitzler

Recommendation: Accept after major revision

Overview:

This article starts out by arguing that reasoning over inconsistent OWL ontologies

is impossible due to the principle of explosion (every sentence in the language can be

derived from an inconsistent ontology). The approach adopted to remedy this is to extend

OWL DL and related logics to manage four truth values instead of the two classical ones.

Important results are shown to hold in the resulting logics, such as their soundness

relative to their classical variants, as well as consequence preservation. Finally, an

experimental evaluation is presented.

Detailed comments

-----------------

The paper is well written, well organized, and contains important results for reasoning

with inconsistent ontologies. My recommendation is motivated by two main concerns:

1) The material in the paper is heavily based on the past work of the authors; it is mentioned

at the end of Section 1 (and in other places as well) that it is a longer version of [24] and [31],

and these are in turn based on [25] through [29]; [30] is also mentioned elsewhere as containing

some of the results described in this paper.

After carefully looking through these references, I was left wondering exactly what material

presented here is new. While it is clear that some parts are new, the novelty of others is

difficult to determine. Furthermore, some comments are rather confusing; an example of this is

the comment regarding reference [24] at the beginning of Section 6, which says that "This was a

point overlooked in the earlier work on SROIQ4 [24], and we discuss it here.". However, the

subsequent discussion was already present in [31].

Another such example can be found in Section 10, Page 21, where it says:

"SROIQ4 was first presented in [24], though there it lacks role chains, role assertions, and

\exists R.Self..."; again, these elements are included in the material in [31].

As part of the revision, the authors should address all such occurrences to avoid this kind of

confusion.

Finally, could the authors please provide a detailed list of what material is new in this manuscript?

2) The empirical evaluation is somewhat weak for a journal paper. First of all, the authors

don't discuss any of the details about how the synthetic ontologies were created; please provide a

description of the process devised to do this so the reader has a better idea of how to interpret

the results.

The other concern is regarding the experiments themselves, which only measure the

time taken to classify the ontologies (which I assume means to infer the consistency and

properties such as superclasses and equivalence between classes; please clarify this in the

manuscript). I would expect to see a more complete set of experiments, with parameter variations

for the synthetic ontologies and some query answering tasks as well. The number of varied

parameters need not be great; choosing the two or three that the authors consider to have the most impact

on the running time for the task in question should be enough to convey a better picture than

the current experiments.

Other comments:

---------------

- Though the presentation and readability of the paper are good, the examples are quite short and

almost no discussion is provided. Perhaps adding a running example, with adequate discussion, that

ties together the presentation would help in this respect. Otherwise, the existing examples should

be expanded to address this.

- The discussion of related work focuses only on paraconsistent approaches to dealing with

inconsistency. There are other approaches in the Data Management literature that should at

least be mentioned here for completeness. These include the following, which are just representatives

of some alternative approaches; though some refer to relational databases or logical knowledge bases,

they are clearly related to the present work through well-known translations.

a) The knowledge base is regarded as a departure from some correct, consistent version. These

approaches prescribe changes to be applied in order to arrive at a "better" version. Some examples:

Grant and Hunter: "Measuring the Good and the Bad in Inconsistent Information". Proceedings of

IJCAI 2011.

Alchourron et al.: "On the logic of theory change: partial meet contraction and

revision functions". Journal of Symbolic Logic, 1985.

Falappa et al.: "On the evolving relation between Belief Revision

and Argumentation". Knowledge Engineering Review, 2011.

Reiter: "A Logic for Default Reasoning". Artificial Intelligence, 1980.

Martinez et al.: "Inconsistency Management Policies". Proceedings of KR 2008.

b) The knowledge base is considered to be an overspecified set of constraints, and "repairs" are

considered to be maximally consistent subsets of such constraints:

Arenas et al.: "Consistent Query Answers in Inconsistent Databases". Proceedings of PODS 1999.

Lembo et al.: "Inconsistency-tolerant Semantics for Description Logics". Proceedings of RR 2010.

Commenting on these alternatives would add to the manuscript's completeness.

Minor errors and typos:

-----------------------

- The use of the word "argument" on Page 1, Col.2 is not very clear. Perhaps "conditional"

or "implication" would be better.

- Page 4, Col. 1: "Below P and Q are ..." --> "Below, P and Q are ..."

- Awkward spacing in some formulas, see for instance the top of Col. 2 on Page 4.

There are other cases as well, especially with the = sign.

- In Def. 4, the composition operator is used without prior introduction.

- Page 14, right before Example 37: It says that "tractability is affected"; is it possible to

provide any insight on how much it is affected?

- Proposition 48 should refer to Table 9, otherwise H1, ... H4, B1, ..., B3 lacks context.

- Page 20, Col. 1: The phrase "This may be used..." could be rephrased to something like

"This argument supports the use of paraconsistent logics, and dispels the general doubts

that sometimes occur around these approaches.".

- Page 20, Col. 2:

"... the ALC fragment of SROIQ4 appears to identical to the logic described in [43]),

which are distinct from Patel-Schneider's ..." -->

"... the ALC fragment of SROIQ4 appears to be identical to the logic described in [43]),

which are distinct from those of Patel-Schneider's ...".

- Page 21, Col. 1: "... for translating his first order logic into FOL ..." --> (?)

"... for translating his logic into FOL ..."

Tags: 

Comments

We thank both reviewers very much for their feedback. As indicated above, a revised paper has been uploaded. Specific comments for each of the reviews are given below. The first review included a PDF with comments, which we discuss here.

Response to Review 1:

Page 8, comment 1: The reviewer notes that $\top$ and $\bot$ are not 4-valued, and suggests that, e.g., $\langle \Delta^{I}, N \rangle$ be used as the interpretation of $\top$. The scheme used in the paper preserves the equivalence of $\neg \top$ and $\bot$. Under the reviewer's proposed new scheme, $\neg \top$ is read as $\langle N, \Delta^{I}\rangle$, which intuitively (to us at least) does not bear much resemblance to a suitable candidate for $\bot$.

Also, sticking with the original scheme allows us to do some other things---e.g., write axioms to enforce the law of noncontradiction in selected instances.

Page 8, comment 2: The reviewer asks us to point out two equivalences.

neg \exists R. C \equiv \forall R.\neg C

\neg \geq n R. C \equiv \leq n+1 R. \neg C

The first of these appears on the previous page in proposition 15. The second is not quite correct in our opinion. Let $C^{I} = \langle \{0,1,2\}, \varnothing\rangle$ and $R^{I} = \langle \{(0,1),(0,2)\}, \varnothing\rangle$). If the reviewer meant another equivalence, then was it item 9 in proposition 15?

Page 8, comment 3: The comment observes that (in)equality is classical. Yes, this is very much true. In general, equality is a very troublesome issue in the framework. If it were paraconsistent, then the resulting formalism would not be easy to embed into a classical logic (we have not thought of a way, at least) so that existing tools (Pellet, etc.) could be used to reason according to the paraconsistent semantics. Since that is a big motivation behind the framework, nonclassical (in)equality comes at a very high a price. We'd very much like a solution---but haven't found one.

The comment asks us to make a note of the classical semantics for (in)equality. We have added to the passage on page 7 to stress this. Equality is also discussed somewhat in sections 5, 6, and 7. Propositions 34 and 36 also deal with the issue explicitly. Observe also that the example in the comment makes use of nominals. The problems nominals introduce are discussed explicitly in section 6.

Page 10, comment 1: The reviewer indicates that he/she would prefer we use the phrase ``X is a 4-model of Y'' rather than ``X 4-models Y''. We have altered the paper, saying ``4-satisfies'' rather than ``4-models''.

Page 12, comment 1: The reviewer points out an error in the example (in the second column) which we have now corrected. What we intended to show is that the use of nominals restricts the cardinality of the positive extension of an interpretation, which causes problems when used with DL cardinality restrictions.

Page 12, comment 2: The reviewer asks whether Proposition 33 holds, indicating $\geq 2 R \sqcap \leq 1 R$ as a counterexample. The proposition does hold, in our opinion. It requires that neither $\top$ nor $\bot$ appear in the concept. While the reviewer is correct that the example given is unsatisfiable, $\top$ appears implicitly (because we don't allow unqualified cardinality restrictions).

Page 13, comment 1: The reviewer indicates that the same example ($\geq 2 R \sqcap \leq 1 R$) can be used as a counterexample to Proposition 34. Again, $\top$ is used implicitly. If it appeared explicitly (which we require), it would be removed using the transformation $SF$ described on page 12.

Page 13, comment 2: The reviewer indicates that $\{a \neq b, \{a\} \sqsubseteq \{b\}\}$ can be used as a counter-example to Proposition 36. The reviewer is correct that the set of axioms has no 4-models. However, Proposition 36 specifically excludes the use of inequality assertions, and so the example does not apply.

Page 14, comment 1: The reviewer asks where the nominals are in the discussion of Horn logics.

This is indeed a mistake! Nominals should have been included, too. The wording has been changed appropriately.

Page 18, comment 1: The reviewer notes that the embedding of the 4-valued DL into its 2-valued counterpart will sometimes result in additional inclusion axioms being included, even if only internal inclusion is used. Yes, that is true, and we have reworded the passage to indicate this.

Page 20, comment 1: The reviewer indicates more work is needed on the experiments. Yes, very much so. However, the focus of the paper is on the basic formalism and proofs of propositions. Though we think the experiments do support the theoretical material of the paper (and that's why we included them), the paper itself is really a theory paper, and we are content to leave a more thorough empirical investigation to another paper (which would have a different sort of reader).

Page 20, comment 2: The reviewer asks us to rephrase ``Inconsistencies are obligatory in real world situations'' (which is too strong). We have done so: ``Inconsistencies often arise in real world situations'' now appears, which we take to be less offensive.

Response to Review 2:

The reviewer is correct that the present paper is an expanded version of earlier ones (which we note in the current paper). In our view it is OK practice to present expanded versions of conference and workshop papers for submission to a journal (where the length restrictions aren't so severe).

Indeed, if the journal accepts this present paper, it is our understanding that it will be included in a special issue devoted to extended versions of papers from RR 2010.

As for the confusing passages noted in the review, they have been removed or rephrased appropriately.

Regarding new material in the paper: The material comprising Sections 8 and 9 has never appeared in a conference or journal paper (though some of it appears as an unpublished technical report). There is an example and proposition (involving the deduction theorem) in Section 2 that does not appear elsewhere. In section 3, several additional concepts (e.g., strong and weak subsumption) are presented, and 8 propositions are now shown versus the 3 appearing in the RR 2010 paper (which forms part of the current paper). In Section 7, Propositions 40 and 41 are new. Throughout the paper, discussions have in general been expanded.

As for the empirical evaluations, we agree that they are limited. However, please observe that they comprise a relatively small part of the paper. While we feel they do add something to the paper, the main thrust of the paper is to present the paraconsistent framework and prove properties about it. The paper is mainly a theoretical one. While a more thorough investigation is needed, we think it should be part of a separate paper. Our first preference is to keep the discussion of the evaluations as it is. If not that, then we would prefer to remove that section completely from the paper (leaving only theoretical subject matter).

Regarding the synthetic knowledge bases, we have added passages describing them in more detail. Only two were generated for the experiments (the general characteristics the ontologies are presented in Table 11, but we have now given more information about them). These were the University ontologies, and as noted in Table 10, they were generated with the Lehigh Benchmark suite.

Note that one of the other ontologies was removed from the paper, as no suitable external reference to it was found.

As for the examples, we note again that the paper is primarily a theory paper, and the examples given typically serve the role of counter-examples (they demonstrate that certain properties do not hold). While a running example might help with the presentation, this is really a matter of style (and the reviewer has already said that the presentation and readability of the paper are good).

Related Work: As the reviewer has suggested, we have extended the related work, including references to some of the papers indicated. We also discuss paraconsistent logics not based on 4-values as well as nonmonotonic formalisms (including Reiter's default logic). While the nonmonotonicity is not the same as paraconsistency, both sorts of formalisms can be viewed as ways of handling conflicts.

Other Comments:

The reviewer writes, "The use of the word 'argument' on Page 1, Col.2 is not very clear. Perhaps `conditional' or 'implication' would be better."

Here we think conditional or implication would be worse, as they might be taken as formal statements of a logic. In our view, `argument' has a standard enough meaning to cause less confusion here.

The reviewer writes, "Page 14, right before Example 37: It says that 'tractability is affected'; is it possible to provide any insight on how much it is affected?"

The passage has been changed to say "the guarantee of tractability is lost", which is accurate. Is the reviewer asking how much of a problem this will be in practice? We think this depends on the nature of the reasoning needed by the user.

As for other comments, We have altered the paper accordingly.