**International Journal of Intelligence Science** Vol.3 No.2(2013), Article ID:30627,11 pages DOI:10.4236/ijis.2013.32011

A Comparison of Paraconsistent Description Logics^{*}

Faculty of Information Technology and Business, Cyber University, Tokyo, Japan

Email: drnkamide08@kpd.biglobe.ne.jp

Copyright © 2013 Norihiro Kamide. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Received December 27, 2012; revised January 29, 2013; accepted February 22, 2013

**Keywords:** Paraconsistent Description Logic; Paraconsistent Semantics; Four-Valued Semantics; Quasi-Classical Semantics; Single-Interpretation Semantics; Dual-Interpretation Semantics

ABSTRACT

Description logics (DLs) are a family of logic-based knowledge representation formalisms with a number of computer science applications. DLs are especially well-known to be valuable for obtaining logical foundations of web ontology languages (e.g., W3C’s ontology language OWL). Paraconsistent (or inconsistency-tolerant) description logics (PDLs) have been studied to cope with inconsistencies which may frequently occur in an open world. In this paper, a comparison and survey of PDLs is presented. It is shown that four existing paraconsistent semantics (i.e., four-valued semantics, quasi-classical semantics, single-interpretation semantics and dual-interpretation semantics) for PDLs are essentially the same semantics. To show this, two generalized and extended new semantics are introduced, and an equivalence between them is proved.

1. Introduction

Description logics (DLs) [2] are a family of logic-based knowledge representation formalisms with a number of computer science applications. DLs are especially wellknown to be valuable for obtaining logical foundations of web ontology languages (e.g., W3C’s ontology language OWL). Some useful DLs including a standard description logic [3] have been studied by many researchers. Paraconsistent (or inconsistency-tolerant) description logics (PDLs) [4-13] have been studied to cope with inconsistencies which may frequently occur in an open world.

Some recent developments of PDLs may be briefly summarized as follows. An inconsistency-tolerant fourvalued terminological logic was originally introduced by Patel-Schneider [10], three inconsistency-tolerant constructive DLs, which are based on intuitionistic logic, were studied by Odintsov and Wansing [8,9], some paraconsistent four-valued DLs including were studied by Ma et al. [4,5], some quasi-classical DLs were developed and studied by Zhang et al. [12,13], a sequent calculus for reasoning in four-valued DLs was introduced by Straccia [11], and an application of fourvalued DL to information retrieval was studied by Meghini et al. [6,7]. A PDL called has recently been proposed by Kamide [14,15] based on the idea of Kaneiwa [16] for his multiple-interpretation DL.

The logic [4], which is based on four-valued semantics, has a good translation into [3], and using this translation, the satisfiability problem for is shown to be decidable. But, and its variations have no classical negation (or complement). As mentioned in [17], classical and paraconsistent negations are known to be both useful for some knowledgebased systems. The quasi-classical DLs in [12,13], which are based on quasi-classical semantics, have the classical negation. But, translations of the quasi-classical DLs into the corresponding standard DLs were not proposed. [14], which is based on dual-interpretation semantics, has both the merits of and the quasiclassical DLs, i.e., it has the translation and the classical negation. The semantics of is taken over from the dual-consequence Kripke-style semantics for Nelson’s paraconsistent four-valued logic N4 with strong negation [18,19]. The constructive PDLs in [8] are based on single-interpretation semantics, which can be seen as a DL-version of the single-consequence Kripke-style semantics for N4 [20].

The following natural question arises: What is the relationship among the single-interpretation semantics of the constructive PDLs, the dual-interpretation semantics of, the four-valued semantics of, and the quasi-classical semantics of the quasi-classical DLs? This paper gives an answer to this question: These paraconsistent semantics are essentially the same semantics in the sense that some fragments of these PDLs are logically equivalent. More precisely, we show the following. A new PDL, called, is introduced based on a generalized quasi-classical semantics. It can be seen that the quasi-classical semantics and the fourvalued semantics are special cases of the semantics. An equivalence between and (a slightly modified version of) is proved. A new PDL, called, is introduced based on a modified single-interpretation semantics. An equivalence between and (a slightly modified version of) is proved. These results mean that the existing applications and theoretical results (e.g., decidability, complexity, embeddability and completeness) can be shared in these paraconsistent semantics.

It is remarked that this paper does not give a “comprehensive” comparison, since the existing paraconsistent semantics have some different constructors (or logical connectives), i.e., it is difficult to compare the whole parts of these existing semantics. But, this paper gives an “essential” comparison with respect to the common part with the constructors (paraconsistent negation), (intersection), (union), (universal concept quantification) and (existential concept quantification). To obtain such a comparison with some exact proofs, we need some small modifications of the existing paraconsistent semantics. Since all the logics discussed in this paper are defined as semantics, we will occasionally identify the semantics with the logic determined by it.

The contents of this paper are then summarized as follows.

In Section 2, the essential parts of the existing paraconsistent semantics (i.e., -semantics, four-valued semantics, quasi-classical semantics and single interpretation semantics) are addressed.

In Section 3, two new semantics (i.e., the - semantics and the -semantics) are introduced, and the equivalence among the -semantics, the -semantics and the -semantics is proved. It is observed that the essential parts of the four-valued semantics and the quasi-classical semantics are special cases of the -semantics. It is also observed that the -semantics is regarded as a classical version of the -semantics (single-interpretation semantics) for a constructive description logic introduced by Odintsov and Wansing.

In Section 4, some remarks on constructive PDLs and temporal DLs.

In Section 5, this paper is concluded.

2. Existing Paraconsistent Semantics

2.1. Semantics

In the following, we present the logic [14], which has dual-interpretation semantics. The - concepts are constructed from atomic concepts, roles, ~ (paraconsistent negation), (classical negation or complement), (intersection), (union), (universal concept quantification) and (existential concept quantification). We use the letters and for atomic concepts, the letter for roles, and the letters and for concepts.

Definition 2.1 Concepts are defined by the following grammar:

Definition 2.2 A paraconsistent interpretation is a structure where 1) is a non-empty set2) is an interpretation function which assigns to every atomic concept a set and to every role a binary relation3) is an interpretation function which assigns to every atomic concept a set and to every role a binary relation4) for any role,.

The interpretation functions are extended to concepts by the following inductive definitions:

, (1)

, (2)

, (3)

, (4)

, (5)

, (6)

, (7)

, (8)

, (9)

, (10)

, (11)

.(12)

An expression is defined as. A paraconsistent interpretation is a model of a concept (denoted as) if . A concept is said to be satisfiable in if there exists a paraconsistent interpretation such that.

The interpretation functions and are intended to represent “verification” (or “support of truth”) and “falsification” (or “support of falsity”), respectively. It is noted that includes [3] as a subsystem since in includes in.

Intuitively speaking, is constructed based on the following additional axiom schemes for:

, (1)

, (2)

, (3)

, (4)

, (5)

. (6)

It is noted that the interpretations for ~ and in correspond to the axiom scheme, which means that ~ and are self duals with respect to and ~, respectively. We now give an intuitive example for this axiom. Let stand for the claim that is poor, and let stand for the claim that is rich. Intuitively, is verified (falsified) iff is falsified (verified, respectively). Suppose now that is indeed falsified. This should mean that it is verified that is poor or neither poor or rich. But this is the case iff is not verified, which means that is not falsified.

For each concept, we can take one of the following cases:

1) is verified, i.e., 2) is falsified, i.e., 3) is both verified and falsified4) is neither verified nor falsified.

Thus, may be regarded as a four-valued logic.

In general, a semantic consequence relation ‘is called paraconsistent with respect to a negation connective: if there are formulas and such that does not hold. In the case of, assume a paraconsistent interpretation such that, and not- for a pair of distince atomic concepts and. Then, does not hold, and hence is paraconsistent with respect to:. It is remarked that is not paraconsistent with respect to.

Next, we explain about some differences and similarities between [16] and. In

, the set of multiple interpretation functions were used. These interpretation functions include the following characteristic conditions for negations:

1) for any atomic concept, 2) for any atomic concept, 3) for any atomic concept, 4)5) with6)7)8).

It is remarked that the condition 1 above means that is not paraconsistent with respect to. The subsystem (or special case) (of), which adopts two interpretation functions and, is similar to. The conditions for the constructors and of are almost the same as those of. The main differences are presented as follows:

1) has the “non-paraconsistent” condition: for any atomic concept,

but has no this condition2) adopts the condition:

but has no this condition and adopts the condition:

instead of it.

2.2. Four-Valued Semantics and Quasi-Classical Semantics

Some four-valued semantics in [4] were based on, , DL-Lite, etc., and the quasi-classical semantics in [13] was based on. The four-valued semantics in [4] has no classical negation, but has some new inclusion constructors such as strong inclusion. In addition, the quasi-classical semantics in [13] has two kinds of definitions called QC weak semantics and QC strong semantics. The following explanation is based on and QC weak semantics. We use the common language based on, , and/or.

We cannot compare the existing paraconsistent semantics (i.e., the four-valued semantics, the quasi-classical semantics, the single-interpretation semantics and the dual-interpretation semantics) themselves since the underlying DLs are different. Moreover, the motivations of introducing the existing semantics are completely different. For example, in the quasi-classical semantics, the main motivation is to satisfy three important inference rules: modus ponens, modus tollens and disjunctive syllogism. These inference rules are strongly dependent on a specific inclusion constructor and a specific QC entailment. Thus, our comparison without is regarded as not so comprehensive or essential in the sense of the original motivation of the quasi-classical semantics.

The following definition is a slight modification of the definition of [4].

Definition 2.3 (Four-valued semantics) A fourvalued interpretation is defined using a pair of subsets of and the projection functions and. The interpretations are then defined as follows:^{1}

1) a role is assigned to a relation2) for an atomic concept, where3) if4) if for5) if for^{6}^{) }

^{7}^{) }

In the four-valued semantics for [4], different kinds of implications were introduced:

1) (material inclusion)

2) (internal inclusion)

3) (strong inclusion).

The interpretations of, and are respectively presented as follows:

(1)

(2)

(3)

These implications provide flexible way to model inconsistent ontologies.

The extension of four-valued semantics to the expressive description logic, and the extensions of four-valued semantics to some tractable description logics, Horn-DLs and DL-Lite family were studied in [5].

Next, we discuss about quasi-classical description logic. The following definition is a slight modification of the definition of quasi-classical description logics [12, 13].

Definition 2.4 (Quasi-classical semantics) A quasiclassical weak interpretation is defined using a pair of subsets of without using projection functions. The interpretations are then defined as follows:^{2}

1) a role is assigned to a pair of binary relations2) for an atomic concept, where3)4)5)6)^{7}^{) }

^{8}^{) }

The quasi-classical semantics for QC [12] were extended to that of QC [13] to handle inconsistent ontologies. It composes two kinds of semantics, i.e., QC weak semantics and QC strong semantics. QC weak semantics inherits the characteristics of four-valued semantics, and QC strong semantics redefines the interpretation for disjunction and conjunction of concepts to make the three important inference rules (i.e., modus ponens, modus tollens and disjunctive syllogism) hold.

Let be a QC entailment and be a paraconsistent negation connective, which is represented as ~ in the above definition. Then, the following hold:

1) (modus ponense)

2) (modus tollens)

3) (disjunctive syllogism).

Two basic query entailment problems (i.e., instance checking and subsumption checking) were also defined and discussed in [13]. It was also shown that the two basic inference problems can be reduced into the consistency problem.

Finally in this subsection, it is remarked that the pairing functions used in the four-valued and quasiclassical semantics have been used in some algebraic semantics for Nelson’s logics (see e.g., [21] and the references therein). On the other hand, the semantics of is defined using two interpretation functions and instead of the pairing functions. These interpretation functions have been used in some Kripketype semantics for Nelson’s logics (see e.g., [22] and the references therein). It will be shown in the next section that the “horizontal” semantics using paring functions and the “vertical” semantics using two kinds of interpretation functions have thus essentially the same meaning.

2.3. Single-Interpretation Semantics

Three constructive PDLs, which have single-interpretation semantics, were introduced and studied by Odintsov and Wansing [8]:

1): Constructive version of. It is obtained via a translation into first-order classical logic. A tableau algorithm for was presented in [9].

2): It is obtained via a translation into the quantified N4. The role restrictions and are not dual.

3): It is obtained via an alternative translation into the quantified N4. The role restrictions and are dual. The decidability of was obtained in [8] from a translation into Fischer Servi’s intuitionistic modal logic.

We now give an overview of as follows. has no classical negation connective, but has a paraconsistent negation connective. Also it has no classical implication (or classical inclusion), but has a constructive implication (or constructive inclusion).

uses interpretations where 1) is a non-empty set2) is a reflexive and transitive relation of informational accessibility3) is an interpretation function with some conditions, e.g.a) it maps every atomic concept to a subset ofb) it maps every negated atomic concept to a subset of.

The interpretation function has the following conditions:

1) for an atomic concept, 2) for an atomic concept, 3)4)5)^{6}^{)}7)8)9)10)11)12)^{13}^{)}.

It is remarked that the order relation needs some more conditions. For the details, see [8,9].

3. New Paraconsistent Semantics

3.1. Semantics

Similar notions and terminologies for are also used for the new logic. The -concepts are the same as the -concepts. The semantics is defined as a generalization and modification of the quasi-classical weak semantics defined in Definition 2.4. Thus, we use the term “quasi-classical” in the following definition.

Definition 3.1 A quasi-classical interpretation is a structure where 1) is a non-empty set2) is a positive (negative, resp.) polarity function which assigns to every atomic concept a set

(, resp.)3) is an interpretation function which assigns to every atomic concept a pair of sets and to every role a pair of binary relations4) for any role,.

The polarity functions are extended to concepts by the following inductive definitions:

, (1)

, (2)

, (3)

, (4)

, (5)

, (6)

, (7)

, (8)

, (9)

, (10)

, (11)

. (12)

The interpretation function is extended to concepts by:

.

An expression is defined as and. A quasi-classical interpretation

is a model of a concept

(denoted as) if. A concept is said to be satisfiable in if there exists a quasiclassical interpretation such that.

We have the following propositions, which mean that Definition 3.1 is essentially the same definitions as those of the original quasi-classical [12,13] and four-valued [4,5] semantics. See Definitions 2.4 and 2.3.

Proposition 3.2 Let be an interpretation function on a quasi-classical interpretation. Then, the following conditions hold:

, (1)

, (2)

, (3)

, (4)

(5)

(6)

Proposition 3.3 Let be an interpretation function on a quasi-classical interpretation. Let and be now represented by P and N, respectively. Also, and for a concept be represented by and, respectively. Define and Then, the following conditions hold:

, (1)

, (2)

, (3)

(4)

(5)

Next, we show the equivalence between and.

Theorem 3.4 (Equivalence between and) For any concept, is satisfiable in iff is satisfiable in.

Proof.: Suppose that is a quasi-classical interpretation. Then, it is sufficient to construct a paraconsistent interpretation

such that, for any concept,

iff. We define a paraconsistent interpretation by:

1)2) is an interpretation function which assigns to every atomic concept a set and to every role a binary relation3) is an interpretation function which assigns to every atomic concept a set and to every role a binary relation.

Then, we have the fact: for any role,.

It is sufficient to show the following claim which implies the required fact. For any concept,

, (1)

. (2)

By (simultaneous) induction on. We show some cases.

Case (is an atomic concept): For 1, we have the following by the definition:. For 2, we have the following by the definition:.

Case: For 1, we have:

(by induction hypothesis for 2). For 2, we have: (by induction hypothesis for 1).

Case: For 1, we have:

(by induction hypothesis for 1). For 2, we have: (by induction hypothesis for 2).

Case: For 1, we have: (by induction hypothesis for 1). For 2, we have: (by induction hypothesis for 2).

Case: For 1, we have:

(by induction hypothesis for 1)

.

For 2, we have:

,

(by induction hypothesis for 2),

.

: Suppose that is a paraconsistent interpretation. Then, it is sufficient to construct a quasi-classical interpretation such that, for any concept, iff. We define a quasi-classical interpretation by:

1)2) is a positive (negative, resp.) polarity function which assigns to every atomic concept a set (, resp.)3) is an interpretation function which assigns to every atomic concept a pair of sets and to every role a pair of binary relations .

Then, we have the fact: for any role,.

It is sufficient to show the following claim which implies the required fact. For any concept,

, (1)

. (2)

Since this claim can be shown in the same way as in the claim of the direction, the proof is omitted here. □

3.2. Semantics

We introduce a new logic, which has a singleinterpretation function. The idea of this formulation is inspired from the paraconsistent semantics for a constructive PDL proposed in [8]. These single-interpretation semantics can also be adapted to Nelson’s paraconsistent logic (see [20]).

Similar notions and terminologies for are also used for. The -concepts are the same as the -concepts.

Definition 3.5 Let be the set of atomic concepts and be the set. A single paraconsistent interpretation is a structure where 1) is a non-empty set2) is an interpretation function which assigns to every atomic (or negated atomic) concept a set and to every role a binary relation.

The interpretation function is extended to concepts by the following inductive definitions:

, (1)

, (2)

, (3)

, (4)

, (5)

, (6)

, (7)

, (8)

, (9)

, (10)

. (11)

An expression is defined as. A single paraconsistent interpretation is a model of a concept (denoted as) if. A concept is said to be satisfiable in if there exists a single paraconsistent interpretation such that.

It is remarked that the logic in [8] has the same interpretations for A (atomic concept), (negated atomic concept), and as in. Since is constructive, it has no classical negation, but has constructive inclusion (constructive implication) which is defined by:

.

Next, we show the equivalence between and.

Theorem 3.6 (Equivalence between and) For any concept, is satisfiable in iff is satisfiable in.

Proof. Let be the set of atomic concepts, be the set, and be the set of roles.

: Suppose that is a single paraconsistent interpretation such that has the domain. Then, it is sufficient to construct a paraconsistent interpretation such that, for any concept, iff. We define a paraconsistent interpretation by:

1)2) is an interpretation function which assigns to every atomic concept a set and to every role a binary relation3) is an interpretation function which assigns to every atomic concept a set and to every role a binary relation4) for any role, 5) the following conditions hold:

, (a)

. (b)

It is noted that and have the domain.

It is sufficient to show the following claim which implies the required fact. For any concept,

, (1)

. (2)

By (simultaneous) induction on. We show some cases.

Case (is an atomic concept): By the definition.

Case: For 1, we have: (by induction hypothesis for 2). For 2, we have: (by induction hypothesis for 1).

Case: For 1, we have: (by induction hypothesis for 1). For 2, we have: (by induction hypothesis for 2).

Case: For 1, we have: (by induction hypothesis for 1). For 2, we have: (by induction hypothesis for 2).

Case: For 1, we have:

(by induction hypothesis for 1)

.

For 2, we have:

,

(by induction hypothesis for 2),

.

: Suppose that is a paraconsistent interpretation such that and have the domain. Then, it is sufficient to construct a single paraconsistent interpretation such that, for any concept, iff. We define a single paraconsistent interpretation by:

1)2) is an interpretation function which assigns to every atomic (or negated atomic) concept a set and to every role a binary relation3) the following conditions hold:

, (a)

. (b)

It is noted that has the domain.

It is sufficient to show the following claim which implies the required fact. For any concept,

, (1)

. (2)

Since this claim can be shown in the same way as in the claim of the direction, the proof is omitted here. □

4. Remarks

4.1. Constructive Semantics

As mentioned before, three constructive PDLs:, and were introduced and studied in [8,9]. By our comparison results of the present paper, we can consider to present the four-valued semantics, the quasi-classical semantics and the dual-interpretation semantics for these constructive PDLs. The notions of constructiveness and paraconsistency are known to be important for logical systems. From the point of view of the truth and falsehood in a logic, the principle of explosion and the excluded middle are the duals of each other. Paraconsistent logics are logics without the principle of explosion, and paracomplete logics are the logics without the excluded middle. Constructive logics are classified as a paracomplete logic. The logics with both the paraconsistency and the paracompleteness are called paranormal (or nonalethic) logics.

Since the precise definitions of the original semantics for and are rather complex, we now present only an outline of the (slightly modified versions of the) semantics of and.

A constructive interpretation is a structure where 1) is a non-empty set2) is a poset3) is a domain function from to (written ad for) such that a) for any, is non-emptyb) for any, if, then.

For each, we interpret an atomic concept and a negated atomic concept ~A as and, respectively. Examples of the interpretations of the composite concepts are presented as follows: For each,

, (1)

, (2)

, (3)

. (4)

The interpretations of and are rather complex, and hence omitted here. Such interpretations of and imply the differences between the -semantics and the -semantics.

4.2. Temporal Semantics

It is remarked that the temporal next-time operator in the temporal description logic [23] is similar to the paraconsistent negation connective in. As mentioned, the connective in is from the paraconsistent negation connective in Nelson’s paraconsistent logic N4 [19,20]. The next-time operator in is from Prior’s tomorrow tense logic [24].

In the following, we explain and the similarities between in and in.

Similar notions and terminologies for are also used for. The symbol is used to represent the set of natural numbers. The -concepts are constructed from the -concepts by adding (next-time operator). An expression is inductively defined by and.

Definition 4.1 - concepts are defined by the following grammar:

Definition 4.2 A temporal interpretation is a structure where 1) is a non-empty set2) each is an interpretation function which assigns to every atomic concept a set and to every role a binary relation3) for any role and any,.

The interpretation function is extended to concepts by the following inductive definitions:

, (1)

, (2)

, (3)

, (4)

, (5)

. (6)

For any, an expression is defined as. A temporal interpretation

is a model of a concept

(denoted as) if. A concept is said to be satisfiable in if there exists a temporal interpretation such that.

The interpretation functions are intended to represent “verification at a time point “.

Intuitively speaking, is constructed based on the following additional axiom schemes for:

, (1)

where (2)

where. (3)

It is noted that in and in are based on some similar axiom schemes. While is regarded as a de Morgan type negation connective, is regarded as a kind of “twisted” de Morgan type connective. By this similarity, we can prove a theorem for embedding into. Such an embedding theorem is similar to a theorem for embedding into. Thus, in an abstract sense, and can be viewed as the same kind of embeddable logics. Indeed, the same embedding-based method can be applied to these logics uniformly.

5. Conclusions

In this paper, a comparison of paraconsistent description logics was addressed. New paraconsistent description logics and were introduced, and the equivalence among, and were proved. The -semantics is regarded as a generalization of both the four-valued semantics [4,5] and the quasi-classical semantics [12,13]. The -semantics is regarded as a small modification of the singleinterpretation semantics [8,9]. The -semantics [14], also called dual-interpretation semantics, was taken over from the dual-consequence Kripke-style semantics for Nelson’s paraconsistent logic N4 [18,19].

Finally, some recent developments on paraconsistent logics based on N4 are addressed. In [25], proof theory of N4 and its variations were presented. In [26], completeness and cut-elimination theorems were proved for some trilattice logics which are regarded as generalizations of N4. In [27], a paraconsistent linear-time temporal logic was introduced extending the well-known linear-time temporal logic (LTL). In [28], a paraconsistent computation-tree logic was introduced extending the well-known computation-tree logic (CTL). In [29], a constructive temporal paraconsistent logic was introduced combining N4 and a constructive version of LTL.

REFERENCES

- N. Kamide, “Paraconsistent Semantics for Description Logics: A Comparison,” Proceedings of the 15th International Conference on Knowledge-Based and Intelligent Information and Engineering Systems, Lecture Notes in Artificial Intelligence, Vol. 6881, 2011, pp. 599-608.
- F. Baader, D. Calvanese, D. McGuinness, D. Nardi and P. F. Patel-Schneider, “The Description Logic Handbook: Theory, Implementation and Applications,” Cambridge University Press, Cambridge, 2003.
- M. Schmidt-Schauss and G. Smolka, “Attributive Concept Descriptions with Complements,” Artificial Intelligence, Vol. 48, 1991, pp. 1-26. doi:10.1016/0004-3702(91)90078-X
- Y. Ma, P. Hitzler and Z. Lin, “Algorithms for Paraconsistent Reasoning with OWL,” Proceedings of the 4th European Semantic Web Conference, Lecture Notes in Computer Science, Vol. 4519, 2007, pp. 399-413.
- Y. Ma, P. Hitzler and Z. Lin, “Paraconsistent Reasoning for Expressive and Tractable Description Logics,” Proceedings of the 21st International Workshop on Description Logic, Technical University of Aachen (RWTH), Aachen, 2008.
- C. Meghini and U. Straccia, “A Relevance Terminological Logic for Information Retrieval,” Proceedings of the 19th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval, New York, 1996, pp. 197-205. doi:10.1145/243199.243267
- C. Meghini, F. Sebastiani and U. Straccia, “Mirlog: A Logic for Multimedia Information Retrieval,” Uncertainty and Logics: Advanced Models for the Representation and Retrieval of Information, Kluwer Academic Publishing, Dordrecht, 1998, pp. 151-185.
- S. P. Odintsov and H. Wansing, “Inconsistency-Tolerant Description Logic: Motivation and Basic Systems,” In: V. F. Hendricks and J. Malinowski, Eds., Trends in Logic: 50 Years of Studia Logica, Kluwer Academic Publishers, Dordrecht, 2003, pp. 301-335. doi:10.1007/978-94-017-3598-8_11
- S. P. Odintsov and H. Wansing, “Inconsistency-Tolerant Description Logic. Part II: Tableau Algorithms,” Journal of Applied Logic, Vol. 6, No. 3, 2008, pp. 343-360. doi:10.1016/j.jal.2007.06.001
- P. F. Patel-Schneider, “A Four-Valued Semantics for Terminological Logics,” Artificial Intelligence, Vol. 38, No. 3, 1989, pp. 319-351. doi:10.1016/0004-3702(89)90036-2
- U. Straccia, “A Sequent Calculus for Reasoning in FourValued Description Logics,” Proceedings of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, Vol. 1227, 1997, pp. 343-357.
- X. Zhang and Z. Lin, “Paraconsistent Reasoning with Quasi-Classical Semantics in ALC,” Proceedings of the 2nd International Conference on Web Reasoning and Rule Systems, Lecture Notes in Computer Science, Vol. 5341, 2008, pp. 222-229.
- X. Zhang, G. Qi, Y. Ma and Z. Lin, “Quasi-Classical Semantics for Expressive Description Logics,” Proceedings of the 22nd International Workshop on Description Logic, Vol. 477, Technical University of Aachen, Aachen, 2009.
- N. Kamide, “Paraconsistent Description Logics Revisited,” Proceedings of the 23rd International Workshop on Description Logics, Vol. 573, Technical University of Aachen, 2010, 12 p.
- N. Kamide, “Embedding-Based Approaches to Paraconsistent and Temporal Description Logics,” Journal of Logic and Computation, Vol. 22, No. 5, 2012, pp. 1097-1124. doi:10.1093/logcom/exr016
- K. Kaneiwa, “Description Logics with Contraries, Contradictories, and Subcontraries,” New Generation Computting, Vol. 25, No. 4, 2007, pp. 443-468. doi:10.1007/s00354-007-0028-2
- G. Wagner, “A Database Needs Two Kinds of Negations,” Proceeding of the 3rd Symposium on Mathematical Fundamentals of Database and Knowledge Bases Systems, Lecture Notes in Computer Science, Vol. 495, 1991, pp. 357-371.
- A. Almukdad and D. Nelson, “Constructible Falsity and Inexact Predicates,” Journal of Symbolic Logic, Vol. 49, 1984, pp. 231-233. doi:10.2307/2274105
- D. Nelson, “Constructible Falsity,” Journal of Symbolic Logic, Vol. 14, 1949, pp. 16-26. doi:10.2307/2268973
- N. Kamide, “An Embedding-Based Completeness Proof for Nelson’s Paraconsistent Logic,” Bulletin of the Section of Logic, Vol. 39, No. 3-4, 2010, pp. 205-214.
- S. P. Odintsov, “Algebraic Semantics for Paraconsistent Nelson’s Logic,” Journal of Logic and Computation, Vol. 13, No. 4, 2003, pp. 453-468. doi:10.1093/logcom/13.4.453
- H. Wansing, “The Logic of Information Structures,” Lecture Notes in Artificial Intelligence, Vol. 681, 1993, pp. 1-163.
- N. Kamide, “A Compatible Approach to Temporal Description Logics,” Proceedings of the 23rd International Workshop on Description Logics, Vol. 573, Technical University of Aachen, 2010, 12 p.
- A. N. Prior, “Time and Modality,” Clarendon Press, Oxford, 1957.
- N. Kamide and H. Wansing, “Proof Theory of Nelson’s Paraconsistent Logic: A Uniform Perspective,” Theoretical Computer Science, Vol. 415, 2012, pp. 1-38. doi:10.1016/j.tcs.2011.11.001
- N. Kamide and H. Wansing, “Completeness and CutElimination Theorems for Trilattice Logics,” Annals of Pure and Applied Logic, Vol. 162, No. 10, 2011, pp. 816-835. doi:10.1016/j.apal.2011.03.001
- N. Kamide and H. Wansing, “A Paraconsistent LinearTime Temporal Logic,” Fundamenta Informaticae, Vol. 106, No. 1, 2011, pp. 1-23.
- K. Kaneiwa and N. Kamide, “Paraconsistent Computation Tree Logic,” New Generation Computing, Vol. 29, No. 4, 2011, pp. 391-408. doi:10.1007/s00354-009-0116-6
- N. Kamide and H. Wansing, “Combining Linear-Time Temporal Logic with Constructiveness and Paraconsistency,” Journal of Applied Logic, Vol. 8, 2010, pp. 33-61. doi:10.1016/j.jal.2009.06.001

NOTES

^{*}This paper includes the results of the conference presentation [1].

^{1}In [4], the symbol is used for the paraconsistent negation.

^{2}In [12,13], the symbols and: are used for the paraconsistent negation and the classical negation, respectively.