We present in this paper a reformulation of the usual set-theoretical
semantics of the description logic $\mathcal{ALC}$ with general TBoxes by using
categorical language. In this setting, $\mathcal{ALC}$ concepts are represented
as objects, concept subsumptions as arrows, and memberships as logical
quantifiers over objects and arrows of categories. Such a category-based
semantics provides a more modular representation of the semantics of
$\mathcal{ALC}$. This feature allows us to define a sublogic of $\mathcal{ALC}$
by dropping the interaction between existential and universal restrictions,
which would be responsible for an exponential complexity in space. Such a
sublogic is undefinable in the usual set-theoretical semantics, We show that
this sublogic is {\sc{PSPACE}} by proposing a deterministic algorithm for
checking concept satisfiability which runs in polynomial space.
Abstract. We present in this paper a reformulation of the usual set-theoretical semantics of the description logic ALC with general TBoxes by using categorical language.
In this setting, ALC concepts are represented as objects, concept subsumptions as arrows, and memberships as logical quantifiers over objects and arrows of categories.
This feature allows us to define a sublogic of ALC by dropping the interaction between existential and universal restrictions, which would be responsible for an exponential complexity in space.
Such a sublogic is undefinable in the usual set-theoretical semantics, We show that this sublogic is PSPACE by proposing a deterministic algorithm for checking concept satisfiability which runs in polynomial space.
1 Introduction Languages based on Description Logics (DLs) [1] such as OWL [2], OWL2 [3], are widely used to represent ontologies in semantics-based applications.
ALC is the smallest DL involving roles which is closed under negation.
ALCは、否定の下で閉鎖される役割を含む最小のDLである。
0.70
It is a suitable logic for a first attempt to replace the usual set-theoretical semantics by another one.
これは、通常の集合論的な意味論を別のものに置き換える最初の試みに適した論理である。
0.65
A pioneer work by Lawvere [4] provided an appropriate axiomatization of the category of sets by replacing set membership with the composition of functions.
In this paper, we propose a rewriting of the usual set-theoretical semantics of ALC by using objects and arrows, the two fundamental elements of category theory, to represent concepts and subsumptions respectively.
Hence, the interaction between existential and universal restrictions with general TBoxes would be responsible for an intractable space complexity if PSPACE(EXPTIME.
The main motivation of this work consists in identifying a sublogic of ALC with general TBoxes which allows to reduce the reasoning complexity without losing too much of the expressive power.
To reduce space complexity when reasoning with ALC under the usual set-theoretical semantics, one can restrict expressiveness of TBoxes by preventing them from having cyclic axioms [9].
This restriction may be too strong for those who wish to express simple knowledge of cyclic nature such as Human ⊑ ∃hasParent.Human.
この制限は、人間のような循環自然の単純な知識を表現したい人には強すぎるかもしれない。
0.73
英語（論文から抽出）
日本語訳
スコア
However, we can find a sublogic of ALC under category-theoretical semantics such that it allows to fully express general TBoxes and only needs to drop a part of the semantics of universal restrictions.
Such a sublogic is undefinable in the usual set-theorectical semantics.
そのような部分論理は通常の集合論的意味論では定義できない。
0.45
Indeed, a universal restriction ∀R.C in ALC can be defined under categorytheoretical semantics by using the following two informal properties (that will be developed in more detail below, Section 4, Definition 8):
(C ⊓ D). We can observe that Property (ii) is a (weak) representation of the interaction be-
(c:d)。 プロパティ (ii) が相互作用 be の (弱) 表現であることを観察することができる。
0.52
tween universal and existential restrictions.
普遍的で実存的な制限です
0.53
As will be shown below (Section 5), if we may just remove this interaction from the categorical semantics of universal restriction, we obtain a new logic, namely ALC ∀, in which reasoning will be tractable in space.
As in the usual set-theoretical semantics, nobody can be a HappyChild under categorytheoretical semantics: the concept is unsatisfiable in this world.
通常の集合論的な意味論のように、カテゴリー論的な意味論の下でハッピーチルドになることはできない。
0.55
Indeed, according to the first axiom if somebody is a HappyChild, then they must simultaneously (1) have some Dessert to eat, and (2) eat only HotMeal, which contradicts the second axiom.
Now, if the second axiom is removed from the TBox, under set-theoretical semantics, the first axiom entails that if somebody is a HappyChild, then they eat HotMeal.
In fact, the first subconcept (∃eatsFood.Dessert) ensures that there exists at least one food item that they eat, and the second one (∀eatsFood.HotMeal) that this food is necessarily HotMeal.
Under the category-theoretical semantics that we will define in this paper (ALC∀), the first axiom alone does not allow to entail that if somebody is a HappyChild then they eat HotMeal.
This is due to the fact that the element of the definition of universal quantification that was there to represent Property (ii) has been dropped, and that unlike set-theoretical semantics, we no longer have a set of individuals providing an extensional “support” for the second subconcept.
For instance, it is not sufficient to define category-theoretical semantics of negation ¬C by stating C ⊓ ¬C −→ ⊥ and ⊤ −→ C ⊔ ¬C because it is not possible to obtain arrows such as C ←−−−−→ ¬¬C from this definition [10].
In Section 5, we begin by identifying a sublogic of ALC, namely ALC∀, by dropping a property from the categorical semantics of universal restriction which would lead to an intractable complexity in space.
There have been very few works on connections between category theory and DLs.
圏論とdlsの関係についてはほとんど研究されていない。
0.47
Spivak et al [12] used category theory to define a high-level graphical language comparable with OWL (based on DLs) for knowledge representation rather than a foundational formalism for reasoning.
Codescu et al [13] introduced a categorical framework to formalize a network of aligned ontologies.
Codescu et al [13]は、整列オントロジーのネットワークを形式化する分類的フレームワークを導入した。
0.69
The formalism on which the framework is based is independent from the logic used in ontologies.
フレームワークがベースとなる形式主義は、オントロジーで使われる論理とは独立している。
0.77
It is shown that all global reasoning over such a network can be reduced to local reasoning for a given DL used in the ontologies involved in the network.
Definition 1 (Syntax and set-theoretical semantics).
定義 1 (syntax and set-theoretical semantics)。
0.88
Let R and C be non-empty sets of role names and concept names respectively.
r と c をそれぞれ役割名と概念名の空でない集合とする。
0.74
The set of ALC-concepts is defined as the smallest set containing all concept names in C with ⊤, ⊥ and complex concepts that are inductively defined as follows: C ⊓ D, C ⊔ D, ¬C, ∃R.C, ∀R.C where C and D are ALC-concepts, and R is a role name in R. An axiom C ⊑ D is called a general concept inclusion (GCI) where C, D are (possibly complex) ALC-concepts.
alc-concepts のセットは、c のすべての概念名、および、c の帰納的に定義される複素概念を含む最小の集合として定義される: c , d , c , d , s , s , sr.c , sr.c , c と d は alc-concepts であり、r は r のロール名である。 訳抜け防止モード: ALC - 概念の集合は、C 内のすべての概念名を含む最小の集合として定義され、この概念は , , , , , , , , , , , , , , , , , , , , , , と帰納的に定義される。 C と D は ALC の概念である。 R は R におけるロール名である。 一般的な概念包含(GCI )では、C, D は ALC - 概念である。
0.83
An ALC ontology O (or general TBox) is a finite set of GCIs.
ALCオントロジー O ( or general TBox) は GCI の有限集合である。
0.68
An interpretation I = h∆I , ·Ii consists of a non-empty set ∆I (domain), and a function ·I (interpretation function) which associates a subset of ∆I to each concept name, an element in ∆I to each individual, and a subset of ∆I × ∆I to each role name such that
⊤I ⊥I (C ⊓ D)I = CI ∩ DI (C ⊔ D)I = CI ∪ DI (¬C)I = ∆I \ CI (∃R.C)I = {x ∈ ∆I | ∃y ∈ ∆I ,hx, yi ∈ RI ∧y ∈ CI} (∀R.C)I = {x ∈ ∆I | ∀y ∈ ∆I , hx, yi ∈ RI =⇒ y ∈ CI}
s = y ∈ RI = y ∈ CI , hx, yi ∈ RI = y ∈ CI , hx, yi ∈ RI = y ∈ CI , hx, yi ∈ RI = y ∈ CI}
0.17
An interpretation I satisfies a GCI C ⊑ D if CI ⊆ DI .
解釈は、CI > DI であれば GCI C > D を満たす。
0.58
I is a model of O, written I |= O, if I satisfies each GCI of O. In this case, we say that O is set-theoretically consistent, and set-theoretically inconsistent otherwise.
I は O のモデルであり、I |= O と書けば、O の各 GCI を満たす。 訳抜け防止モード: I |= O と書かれた O のモデルである。 もし私がOの各GCIを満たすなら。この場合、 我々は、O は、理論的に一貫性があり、集合であり、理論的には矛盾しないと言う。
0.65
A concept C is set-theoretically satisfiable with respect to O if there is a model I of O such that CI 6= ∅, and settheoretically unsatisfiable otherwise.
概念 C が O に関して集合論的に満足できるのは、O のモデル I が存在して CI 6 = ... であり、それ以外は集合論的に満足できないことである。 訳抜け防止モード: 概念 c が集合-o に関して理論的に満足できる o のモデル i は ci 6= s であり、そうでなければ settheoretically は満足できない。
0.75
We say that a GCI C ⊑ D is set-theoretically entailed by O, written O |= C ⊑ D, if CI ⊆ DI for all models I of O. The pair hC, Ri is called the signature of O.
ここで、GCI C > D は O |= C > D と書かれ、O のすべてのモデル I に対して CI > DI と書かれる。 訳抜け防止モード: 理論上は O に関係のある GCI C を D とする。 O |= C > D, if CI > DI for all model I of O. The pair hC, 理はOの署名と呼ばれる。
0.73
We finish this section by introducing notations that will be used in the paper.
本稿で使用する表記法を導入することで、この節を締めくくります。
0.70
We use |S| to denote the cardinality of a set S. Given an ALC ontology O, we denote by sub(O) the set of all sub-concepts occurring in O. The size of an ontology O, denoted bykOk, is the size of all GCIs.
集合 S の濃度を表すために |S| を用いる。 ALC オントロジー O が与えられたとき、O で生じるすべての部分概念の集合を sub(O) で表す。 訳抜け防止モード: ALCオントロジー O を与えられた集合 S の濃度を表すために |S| を用いる。 O で生じるすべての部分-概念の集合を sub(O ) で表す。 bykOk と書くと、すべての GCI のサイズである。
0.72
Analogously, we use kCk to denote the size of a concept C. It holds that |sub(O)| is polynomially bounded by kOk since if a concept is represented as string then a sub-concept is a substring.
We can observe that the set-theoretical semantics of ALC is based on set membership relationships, while ontology inferences, such as consistency or concept subsumption, involve set inclusions.
This explains why inference algorithms developed in this setting often have to build sets of individuals connected in some way for representing a model.
In particular, there are initial and terminal objects R⊥ and R⊤ in Cr with arrows R −→ R⊤ and R⊥ −→ R for all object R of Cr.
特に、Cr のすべての対象 R に対して、矢印 R − → R と R − → R を持つ初期および終対象 R が存在する。
0.79
There is also an identity arrow R −→ R for each object R of Cr.
また、Cr の各対象 R に対して単位矢印 R − → R が存在する。
0.81
2. Each concept name in C is an object of Cc.
2. C における各概念名は Cc の対象である。
0.89
In particular, ⊥ and ⊤ are respectively initial and terminal objects, i.e. there are arrows C −→ ⊤ and ⊥ −→ C for each object C of Cc.
すなわち、cc の各対象 c に対して、矢印 c −→ s と −→ c が存在して、それぞれ始終対象と終端対象である。
0.66
Furthermore, for each object C of Cc there is an identity arrow C −→ C, and for each object R of Cr there are two objects of Cc, namely dom(R) and cod(R).
さらに、Cc の各対象 C に対して恒等矢印 C − → C が存在し、Cr の各対象 R に対して Cc の二つの対象、すなわち dom(R) と cod(R) が存在する。
0.85
英語（論文から抽出）
日本語訳
スコア
3. If there are arrows E −→ F and F −→ G in Cc (resp. Cr), then there is an arrow
3. Cc に矢 E −→ F と F −→ G がある場合(resp. Cr)、矢がある。
0.72
E −→ G in Cc (resp. Cr).
E −→G in Cc (resp. Cr)。
0.43
4. There are two functors dom and cod from Cr to Cc, i.e. they associate two objects
4. crからccへの2つの関手domとcod、すなわち2つのオブジェクトを関連付ける
0.67
dom(R) and cod(R) of Cc to each object R of Cr such that
In the sequel, we introduce category-theoretical semantics of disjunction, conjunction, negation, existential and universal restriction objects if they appear in CchC, Oi.
続編では, CchC, Oi に現れる場合, 解離, 結合, 否定, 存在, 普遍的制約オブジェクトのカテゴリー論的意味論を紹介する。
0.80
Some of them require more explicit properties than those needed for the set-theoretical semantics.
それらのいくつかは集合論的な意味論に必要なものよりも明示的な性質を必要とする。
0.49
This is due to the fact that set membership is translated into arrows in a syntax category.
これは、集合のメンバシップが構文カテゴリの矢印に翻訳されるためである。
0.67
Since semantics of an object in a category depends to relationships with another ones, the following definitions need to add to CchC, Oi and CrhC, Oi new objects and arrows.
カテゴリ内のオブジェクトのセマンティクスは、他のオブジェクトとの関係に依存するため、以下の定義はcchc、oi、crhc、oi new object、arrowsに追加する必要がある。
0.75
Definition 4 (Category-theoretica l semantics of disjunction).
定義4(分節のカテゴリー理論的意味論)。
0.70
Let C, D, C ⊔ D be concept objects of CchC, Oi.
C, D, C , D を CchC, Oi の概念対象とする。
0.81
Category-theoretical semantics of C ⊔ D is defined by using arrows in CchC, Oi as follows.
C > D のカテゴリー論的意味論は、CchC, Oi の矢印を用いて定義される。
0.69
There are arrows i, j from C and D to C ⊔ D,
矢印 i, j は c と d から c と d への矢印である。
0.74
英語（論文から抽出）
日本語訳
スコア
X f k C i
X f k C 私は
0.53
C ⊔ D g j D
略称はD。 g j D
0.44
Fig. 1: Commutative diagram for disjunction
第1図:分断の可換図
0.57
and if there is an object X and arrows f, g from C, D to X, then there is an arrow k such that the following diagram commutes :
そして、対象 X が存在して、C, D から X への矢印 f, g が存在するなら、次の図が可換になるような矢印 k が存在する。
0.70
The diagram in Figure 1 can be rephrased as follows:
図1の図は次のように表現できる。
0.76
C −→ C ⊔ D and D −→ C ⊔ D ∀X, C −→ X and D −→ X =⇒ C ⊔ D −→ X
C −→ C > D と D −→ C > D > X, C −→ X と D −→ X は C > D > X である。
0.83
(1) (2) Intuitively speaking, Properties (1) and (2) tell us that C ⊔D is the “smallest” object which is “greater” than C and D. The following lemma establishes the connection between the usual set semantics of disjunction and the category-theoretical one given in Definition 4.
(1) (2) 直観的には、特性 (1) と (2) は c が c と d よりも「大きい」「最も小さい」対象であることを示す。 訳抜け防止モード: (1) (2) 直感的に言えば、 性質 ( 1 ) と ( 2 ) は、C は C と D よりも "より大きい" オブジェクトであることを示す。 そして、そのカテゴリ - 定義4で与えられる理論的カテゴリ。
0.48
In this lemma, Properties (3) and (4) are rewritings of Properties (1) and (2) in set theory.
Lemma 1. The category-theorectica l semantics of C ⊔ D characterized by Definition 4 is compatible with the set-theoretical semantics of C ⊔ D, that means if h∆I , ·Ii is an interpretation under set-theoretical semantics, then the following holds:
レマ1号。 定義 4 で特徴づけられる c と d の圏論的意味論は、c と d の集合論的意味論(英語版)(set-theoretical semantics)と互換性がある。
0.54
(C ⊔ D)I = CI ∪ DI iff
(c、d)i = ci、di iff である。
0.68
CI ⊆ (C ⊔ D)I , DI ⊆ (C ⊔ D)I ∀X ⊆ ∆I , CI ⊆ X, DI ⊆ X =⇒ (C ⊔ D)I ⊆ X
CI ^ (C ^ D)I, DI ^ (C ^ D)I ^ (C ^ D)I ^ (C ^ D)I, CI ^ X, DI ^ X = ^ (C ^ D)I ^ X
0.35
(3) (4) Proof.
(3) (4) 証明。
0.49
“⇐=”. Due to (3) we have CI ∪ DI ⊆ (C ⊔ D)I .
“⇐=”. (3) のため、CI は DI は (C は D)I である。
0.44
Let X = CI ∪ DI .
X = CI > DI とする。
0.70
Due to (4) we have (C ⊔ D)I ⊆ X = CI ∪ DI .
(4) のため、(C は D)I は X = CI は DI である。
0.71
“=⇒”. From (C ⊔D)I = CI ∪DI , we have (3).
“=⇒”. C(D)I = CI(D) から (3) が成り立つ。
0.54
Let x ∈ (C ⊔D)I .
x ∈ (C )D)I とする。
0.78
Due to (C ⊔D)I = CI ∪ DI , we have x ∈ CI or x ∈ DI.
C > D)I = CI > DI であるため、x ∈ CI あるいは x ∈ DI が存在する。
0.75
Hence, x ∈ X since CI ⊆ X and DI ⊆ X.
したがって、X ∈ X は CI は X であり、DI は X である。
0.74
At first glance, one can follow the same idea used in Definition 4 to define categorytheoretical semantics of C ⊓ D as described in Figure 2.
一見すると、図2で述べられているように、定義 4 で使われるのと同じアイデアに従って C > D の圏論的意味論を定義することができる。
0.60
They tell us that C ⊓ D is the “greatest” object which is “smaller” than C and D.
彼らは、C > D は C と D よりも "小さい" 物体であると言う。 訳抜け防止モード: 彼らは私たちにそれを言う。 C > D は C と D よりも "小さい" 対象である。
0.78
However, this definition is not strong enough to entail the distributive property of
しかし、この定義は分配的性質を伴わないほど強いものではない。
0.69
conjunction over disjunction. Hence, we need a stronger definition for conjunction.
譲歩を乗り越える。 したがって、結合にはより強固な定義が必要です。
0.44
Definition 5 (Category-theoretica l semantics of conjunction).
定義5(結合の圏論的意味論)。
0.66
Let C, D, E, C ⊓ D, C ⊓ E, D ⊔ E, C ⊓ (D ⊔ E) and (C ⊓ D) ⊔ (C ⊓ E) be objects of CchC, Oi.
C, D, E, C は E, D は E, C は E, C は E, C は E, C は E, C は E, C は E, C は E, C は E, C は E, C は E, C は E である。 訳抜け防止モード: C、D、E、C、D、C、E、 D は E, C は E, D は E である。 そして、(C ) D ) ) (C ) E ) は CchC, Oi の対象である。
0.80
Category-theoretical semantics of C ⊓ D is defined by using the following properties in CchC, Oi.
C > D のカテゴリー論的意味論は、CchC, Oi の以下の性質を用いて定義される。
0.64
C ⊓ D −→ C and C ⊓ D −→ D ∀X, X −→ C and X −→ D =⇒ X −→ C ⊓ D C ⊓ (D ⊔ E) −→ (C ⊓ D) ⊔ (C ⊓ E)
C シュ D −→ C と C シュ D −→ D シュX, X −→ C と X −→ D = シュ X −→ C シュ D C シュ (D シュ E) −→ (C シュ D) シュ (C シュ E) 訳抜け防止モード: C は D −→ C であり、C は D −→ D は X である。 X −→ C および X −→ D = > X −→ C > D C > ( D ^ E ) −→ ( C ^ D ) > ( C ^ E )
0.85
(5) (6) (7)
(5) (6) (7)
0.43
英語（論文から抽出）
日本語訳
スコア
X f k C i
X f k C 私は
0.53
C ⊓ D g j D
略称はD。 g j D
0.44
Fig. 2: Commutative diagram for a weak conjunction
図2:弱結合の可換図
0.52
Lemma 2. The following properties hold:
レマ2号。 以下の特性がある。
0.63
C ⊔ D ←−−−−→ D ⊔ C C ⊓ D ←−−−−→ D ⊓ C (C ⊔ D) ⊔ E ←−−−−→ C ⊔ (D ⊔ E) (C ⊓ D) ⊓ E ←−−−−→ C ⊓ (D ⊓ E)
C > D > D > D > D > C > C > D > C > D > C > D > D > D > C > C > C > D > D > E > D > D > E > E > D > D > D > E > E > D > E > D > E > D > D > C > E > E > E > E > − − − > C > C > (D > E > E > E である。
0.17
(8) (9) (10)
(8) (9) (10)
0.43
(11) In other words, ⊔ and ⊓ are commutative and associative with relation to the objects.
(11) 言い換えると、 s と s は可換であり、対象との関係で関連付けられる。
0.54
Proof. These properties are direct consequences of the previous definitions.
証明。 これらの性質は以前の定義の直接的な結果である。
0.61
1. We start by proving Property (8).
1. プロパティを証明することから始める(8)。
0.73
Consider object D ⊔C: from Property (1), we have D −→ D ⊔ C and C −→ D ⊔ C. Then, recall Property (2) above, which states that for all object X such that C −→ X and D −→ X then C ⊔ D −→ X. Replace X by D ⊔ C to obtain C ⊔ D −→ D ⊔ C. We obtain arrow D ⊔ C −→ C ⊔ D by switching the roles of D ⊔ C and C ⊔ D from the above reasoning.
c −→ x と d −→ x であるすべての対象 x に対して、c −→ x と d −→ x であるようなすべての対象 x に対して、c −→ d −→ x は、x を d に置き換えて c −> d −> c を得る。 訳抜け防止モード: 対象 D > C を考える : 性質 ( 1 ) から D −→ D > C とする。 すると、プロパティー (2 ) を上から思い出す。 これは、C − → X と D − → X が成り立つすべての対象 X に対して、C > D − → X を D > C によって置き換え、X を C > D − → D > C とする。 D と C と D の役割を上記の推論から切り換える。
0.73
2. Property (9): use the first part of the conjunction definition (5) on D ⊓ C to obtain D ⊓ C −→ D and D ⊓ C −→ C. From Property (6), we know that for all object X such that X −→ C and X −→ D then X −→ C ⊓ D. Thus replace X by D ⊓ C to get D ⊓ C −→ C ⊓ D. As above, the inverse arrow is obtained by swapping the roles of D ⊓ C and C ⊓ D.
2. 性質 (9): 接続定義 (5) の第一部分を使って D > C と D > C > C を得る 性質 (6) から、X − → C と X − → D であるようなすべての対象 X に対して、X は D > C > C > D となる。 訳抜け防止モード: 2 . 性質 (9 ) : 接続定義 (5 ) の最初の部分を使って D > C −→ D を得る。 と D は C から C へ (6 ) すべての対象 X に対して X −→ C と X −→ D が成り立つなら、X −→ C は D である。 上述のように、X を D から C に置き換え、D から C −→ C から D に置き換える。 逆矢印は D > C と C > D の役割を交換する。
0.77
3. Property (10): We start by proving that
3. 財産(10):その証明から始める
0.59
(C ⊔ D) ⊔ E −→ C ⊔ (D ⊔ E).
(C は D) は E −→ C は (D は E) である。
0.78
Let X = C ⊔ (D ⊔ E), we have C −→ X by (1), as well as D −→ D ⊔ E −→ X, then by (2), we get C ⊔ D −→ X. Noting we also have E −→ D ⊔ E −→ X by definition, we can conclude that
X = C > (D > E) と C − → X を (1) と D −→ D > E −→ X とすると、(2) によって C > D −→ X が得られる。 訳抜け防止モード: X = C {\displaystyle X} を ( 1 ) {\displaystyle (1)} で C − → X とする。 D −→ D > E −→ X と同様に、 ( 2 ) によって。 C は D − → X である。 また、定義により E − D > E − → X も成立する。 結論は
0.85
(C ⊔ D) ⊔ E −→ X.
(C は D) は E −→ X である。
0.75
The other direction can be proven with no loss of generality by changing the order by which we apply the arrows.
他方の方向は、矢印を適用する順序を変更することによって一般性を失うことなく証明できる。
0.75
4. Property (11): As above, proving one direction is virtually the same as proving the other one by swapping the role of C ⊓ D and D ⊓ E. Thus we just need to prove the following property:
4. 性質 (11): 上述のように、一方の方向の証明は、もう一方の方向の証明とほとんど同じであり、一方の方向の証明は C > D と D > E の役割を交換することによって行われる。
0.56
C ⊓ (D ⊓ E) −→ (C ⊓ D) ⊓ E
e) −→ (d) (d) −e である。
0.49
英語（論文から抽出）
日本語訳
スコア
Let X = C ⊓(D⊓E).
x = c(d) とする。
0.59
From (5), we get X −→ C and X −→ D ⊓ E −→ D. Applying (6), we obtain X −→ C ⊓ D. Property (5) also gives us X −→ D ⊓ E −→ E; so, applying (6) once again, we end up with:
(5) から X −→ C と X −→ D > E −→ D を得る。 (6) を適用すれば、X −→ C > D が得られる。 訳抜け防止モード: 5 から X −→ C と X −→ D > E −→ D が得られる。 性質 (5 ) もまた、X − → D > E − → E を与える。 もう一度 (6 ) を適用すれば 最終的には:
0.67
which concludes the proof. X −→ (C ⊓ D) ⊓ E
証明を結論づけます x −→ (c が d である) は e である。
0.56
Lemma 3. Assume that we have D −→ E, then the following properties hold:
第3弾。 D − → E と仮定すると、以下の性質が成り立つ。
0.63
C ⊔ D −→ C ⊔ E C ⊓ D −→ C ⊓ E.
C > D −→ C > E C > D −→ C > E である。
0.77
(12) (13) Proof.
(12) (13) 証明。
0.49
By hypothesis the arrow D −→ E exists.
仮説により、矢印 D − → E が存在する。
0.70
If we let X = C ⊔ E, then by (1) we have C −→ X and E −→ X, since D −→ E, by definition we have D −→ X and then by (2), C ⊔ D −→ X.
X = C > E とすると、(1) によって C − → X と E − → X が成り立つが、これは定義によって D − → E となり、(2) によって C > D − → X となる。
0.84
Let X = C⊓D, then by hypothesis and (5), we have X −→ C and X −→ D −→ E.
X = C とすると、仮説と(5)により、X −→ C と X −→ D −→ E が成り立つ。
0.82
Using (6), we get X −→ C ⊓ E.
6) を用いて、X − → C > E を得る。
0.80
Note that under the set-theoretical semantics the distributive property of disjunction over conjunction is not independent, i.e. it is a consequence of the definitions of disjunction and conjunction.
However, this does not hold under the category-theoretical semantics.
しかし、これは圏論的意味論には当てはまらない。
0.52
The following lemma provides the connection between the usual set semantics of conjunction and the category-theoretical one given in Definition 5.
下記の補題は、接続の通常の集合意味論と定義5で与えられる圏論的意味論の間の関係を提供する。
0.65
In this lemma, Properties (14-16) are rewritings of Properties (5-7) in set theory.
この補題では、性質 (14-16) は集合論における性質 (5-7) の書き換えである。
0.62
Lemma 4. The category-theoretical semantics of C ⊓ D characterized by Definition 5 is compatible with the set-theoretical semantics of C ⊓ D, that means if h∆I , ·Ii is an interpretation under set-theoretical semantics, then the following holds:
第4回。 定義 5 を特徴とする c の圏論的意味論は c の集合論的意味論(英語版)と相容れ、つまり h が集合論的意味論(英語版)の下での解釈であるなら、次のようになる。
0.52
(U ⊓ V )I = U I ∩ V I for all concepts U, V iff
(U > V )I = U I > V I for all concept U, V iff
0.38
(C ⊓ D)I ⊆ CI , (C ⊓ D)I ⊆ DI ∀X ⊆ ∆I , X ⊆ CI , X ⊆ DI =⇒ X ⊆ (C ⊓ D)I (C ⊓ (D ⊔ E))I ⊆ ((C ⊓ D) ⊔ (C ⊓ E))I
Definition 6 (Category-theoretica l semantics of negation).
定義6(否定の圏論的意味論)。
0.65
Let C, ¬C, C ⊓¬C, C ⊔¬C be objects of CchC, Oi.
C, > C, C > C > C > C > C > C > C を CchC, Oi の対象とする。
0.56
Category-theoretical semantics
カテゴリー理論的意味論
0.50
of ¬C is defined by using the following arrows in CchC, Oi.
Oi の CchC は以下の矢印を用いて定義される。
0.67
C ⊓ ¬C −→ ⊥ ⊤ −→ C ⊔ ¬C ∀X, C ⊓ X −→ ⊥ =⇒ X −→ ¬C ∀X, ⊤ −→ C ⊔ X =⇒ ¬C −→ X
c は x を、c は x は x を、c は x は x を、c は x は x を、c は x を、c は x を、c は x を、c は x を、c は x を成す。
0.38
(17) (18) (19)
(17) (18) (19)
0.43
(20) Informally, Property (19) tells us that ¬C is the “greatest” object satisfying (17) while Property (20) tells us that ¬C is the “smallest” object satisfying (18).
Lemma 5. The category-theoretical semantics of ¬C characterized by Definition 6 is compatible with the set-theoretical semantics of ¬C, that means if h∆I , ·Ii is an interpretation under set-theoretical semantics, then the following holds:
1. By Properties (17) and (19) where C gets ¬C and X gets C, we have C −→ ¬¬C.
1. 性質 (17) と (19) により、C は C となり、X は C となる。 訳抜け防止モード: 1 . 性質 (17 ) と (19 ) により、C は C となり、X は C となる。 C −→ >C である。
0.79
Analogously, by Properties (18) and (20), we obtain ¬¬C −→ C. Hence, (23) is proved.
同様に、18) と (20) の性質により、c −→ c が得られるので、 (23) が証明される。
0.65
2. To prove (24), we need C ⊓ D −→ ⊥ which follows from C ⊓ D −→ C −→ ¬D and C ⊓ D −→ D, and thus C ⊓ D −→ D ⊓ ¬D −→ ⊥.
2. (24) を証明するためには、C は D −→ C −→ D、C は D −→ D、C は D −→ D、C は D −→ D は D −→ D から従う必要がある。
0.78
Conversely, if D −→ ¬C, then we have C ⊓ D −→ D −→ ¬C and C ⊓ D −→ C thus C ⊓ D −→ ⊥ and we have finished the proof.
逆に、D −→ >C の場合、C は D −→ D −→ >C であり、C は D −→ C であり、C は D −→ >C であり、証明は完了した。
0.68
英語（論文から抽出）
日本語訳
スコア
3. To prove (25), we start by proving C −→ ¬D =⇒ C ⊓ D −→ ⊥.
3. (25) を証明するためには、まず C − → > D = > C > D −→ > を証明することから始める。 訳抜け防止モード: 3) 証明する(25) まず、C − → > D = > C > D −→ > の証明から始める。
0.73
We have C ⊓ D −→ D and C ⊓ D −→ C −→ ¬D.
C は D −→ D であり、C は D −→ C −→ シュD である。
0.73
By definition of conjunction, we obtain C ⊓ D −→ D ⊓ ¬D −→ ⊥.
結合性の定義により、 c {\displaystyle c} が c {\displaystyle c} となる。
0.50
To prove the other direction, we use (19) with X = D or X = C.
他の方向を証明するために、(19) を X = D または X = C で表す。
0.87
4. To prove (26), we need the definitions of conjunction, disjunction and negation.
4.(26)を証明するには、結合、切断、否定の定義が必要である。
0.70
We have C ⊓ D −→ C and C ⊓ D −→ D. Due to (24), we obtain ¬C −→ ¬(C ⊓ D) and ¬D −→ ¬(C ⊓D).
C は D −→ C であり、C は D −→ D であり、(24) により、(C は D は C は C である)、(C は D は C である)。
0.65
By the definition of disjunction, we obtain ¬C ⊔¬D −→ ¬(C ⊓D).
解離の定義により、 > C > D −→ >(C >D) を得る。
0.56
To prove the inverse, we take arrows ¬C −→ ¬C ⊔ ¬D and ¬D −→ ¬C ⊔ ¬D from the definition of disjunction.
逆数を証明するために、分離の定義から矢印 ,c −→ ,c ,d −→ ,c ,d を取ればよい。
0.57
Due to (24), it follows that ¬(¬C ⊔ ¬D) −→ C and ¬(¬C ⊔ ¬D) −→ D. By definition, we obtain ¬(¬C ⊔ ¬D) −→ C ⊓ D. Due to (24) and (23), it follows that ¬(C ⊓ D) −→ ¬C ⊔ ¬D.
Due to (24), we have C −→ ¬(¬C ⊓ ¬D) and D −→ ¬(¬C ⊓ ¬D).
24) のため、c −→(c ) と d −→(c ) が成立する。 訳抜け防止モード: 24) のため、C −→ > ( > C > > D ) となる。 そして、D −→ は、(...) である。
0.60
By the definition of disjunction, we have C ⊔ D −→ ¬(¬C ⊓ ¬D), and by (24) we obtain (¬C ⊓ ¬D) −→ ¬(C ⊔ D).
分断の定義により、 c {\displaystyle c} は c {\displaystyle c} が成立し、 (24) は (c {\displaystyle c} が成立する。 訳抜け防止モード: 逆数の定義により、 c {\displaystyle c} は c {\displaystyle c} である。 そして、 (24 ) によって、 ( , c ) −→ , (c , d ) を得る。
0.58
To prove the inverse, we take arrows C −→ C ⊔D and D −→ C ⊔D obtained from the definition of disjunction.
逆数を証明するために、解離の定義から得られた矢印 C − → C ^ D と D − → C ^ D を取る。
0.69
Due to (24), we have ¬(C ⊔ D) −→ ¬C and ¬(C ⊔ D) −→ ¬D.
(24) のため、(c) −→ (c) −→ (d) −→ (d) である。
0.64
By definition, we have ¬(C ⊔ D) −→ ¬C ⊓ ¬D.
定義上は、 > ( C ) D) −→ (C ) D である。
0.73
In order to define category-theoretical semantics of existential restrictions, we need to introduce new objects and arrows to CchC, Oi and CrhC, Oi, and use the functors dom and cod as described in Figure 3.
実存的制約の圏論的意味を定義するためには、CchC, Oi, CrhC, Oi に新しい対象と矢を導入し、図3に示すように関手 dom と cod を使用する必要がある。 訳抜け防止モード: カテゴリーを定義するために - 存在制約の理論的意味論。 新しいオブジェクトと矢印をCchC、Oi、CrhCに導入する必要があります。 Oi, and use the functors dom and cod as described in Figure 3 .
0.84
R′ k l R
R' k うーん R
0.52
R(∃R.C)
R (複数形 Rs)
0.68
cod cod dom
コッド コッド ドム
0.43
dom cod(R′)
ドム cod (複数形 cods)
0.41
C cod(R(∃R.C))
C cod (複数形 cods)
0.34
i j dom(R′)
私は j dom (複数形 doms)
0.52
m dom(R(∃R.C))
M dom (複数形 doms)
0.42
Fig. 3: Category-theoretical semantics for existential restriction
第3図:存在制限に対するカテゴリー理論的意味論
0.74
Definition 7 (Category-theoretica l semantics of existential restriction).
定義7(Category-theoretic al semantics of existential limit)。
0.89
Let ∃R.C, C be objects of CchC, Oi, and R, R(∃R.C) be objects of CrhC, Oi.
r.c, c を cchc, oi, r のオブジェクトとし、r(r.c) を crhc, oi のオブジェクトとする。
0.66
Category-theoretical semantics of ∃R.C is defined by using arrows in CchC, Oi and CrhC, Oi as follows.
CchC, Oi および CrhC, Oi の矢印を用いて、R.C のカテゴリー論的意味論を定義する。
0.72
R(∃R.C) −→ R, cod(R(∃R.C)) −→ C dom(R(∃R.C)) ←−−−−→ ∃R.C ∀R′, R′ −→ R, cod(R′) −→ C =⇒
r(r.c) −→ r, cod(r(sr.c)) −→ c dom(r(sr.c)) -> c dom(r(sr.c)) -−−−−→ sr', r′ −→ r, cod(r′) −→ c = である。 訳抜け防止モード: r(r.c ) −→ r, cod(r(r.c ) ) −→ c dom(r(r.c ) ) r′ −→ r , cod(r′ ) −→ c = である。
0.68
dom(R′) −→ dom(R(∃R.C))
dom(R′) −→ dom(R(\R.C))
0.43
(28) (29) (30)
(28) (29) (30)
0.43
英語（論文から抽出）
日本語訳
スコア
The following lemma establishes the connection between set-theoretical semantics of existential restriction and the category-theoretical one given in Definition 7.
Lemma 7. The category-theoretical semantics of ∃R.C characterized by Definition 7 is compatible with the set-theoretical semantics of ∃R.C, that means if h∆I , ·Ii is an interpretation under set-theoretical semantics such that
We have R(∃R.C) −→ R and cod(R(∃R.C)) −→ C −→ D. By definition, we obtain dom(R(∃R.C)) −→ dom(R(∃R.D)).
r(r.c) −→ r と cod(r(r.c)) −→ c −→ d と定義すれば、dom(r(r.c)) −→ dom(r(r.d)) が得られる。
0.63
The set-theoretical semantics of universal restriction can be defined as negation of existential restriction.
普遍制限の集合論的意味論は存在制限の否定として定義することができる。
0.68
However, ∀R.C ←−−−−→ ¬∃R.
但し、r.c.---------------r . である。
0.37
¬C does not allow to obtain usual connections between existential and universal restrictions such as ∃R.D ⊓ ∀R.C −→ ∃R.
c は存在的制約と普遍的制約との間の通常の接続を得ることを許していない。
0.63
(D ⊓ C) under the category-theoretical semantics (the “property (ii)” mentioned in our introduction).
(d:c) カテゴリー理論的意味論(紹介で述べた「プロパティ(ii)」)。
0.67
Therefore, we need more arrows to define category-theoretical semantics of universal restriction as follows.
したがって、普遍的制限の圏論的意味論を定義するには、もっと多くの矢が必要である。
0.47
英語（論文から抽出）
日本語訳
スコア
Definition 8 (Category-theoretica l semantics of universal restriction).
定義8(Category-theoretic al semantics of universal limit)。
0.45
Let ∀R.C, C be objects of CchC, Oi, and R be an object of CrhC, Oi.
C を CchC, Oi, R の対象とし、CrhC, Oi の対象とする。
0.72
Category-theoretical semantics of ∀R.C is defined by using arrows in CchC, Oi and CrhC, Oi as follows.
CchC, Oi および CrhC, Oi の矢印を用いて、R.C のカテゴリー論的意味論を定義する。
0.72
∀R.C ←−−−−→ ¬∃R.
略称は「-------------------- --」。
0.25
¬C ∀R′, R′ −→ R, dom(R′) −→ ∀R.C =⇒ cod(R′) −→ C
r′, r′ −→ r, dom(r′) −→ シュル.c = シュコド(r′) −→ c
0.73
(36) (37) We formulate and prove the connection between the usual set-theoretical semantics
(36) (37) 私たちは、通常の集合論的意味論の間の関係を定式化し、証明する
0.44
of universal restriction and the category-theoretical one given in Definition 8.
普遍的制限と定義8で与えられる圏論的制限の
0.73
Lemma 9. The category-theoretical semantics of ∀R.C characterized by Definition 8 is compatible with the set-theoretical semantics of ∀R.C, that means if h∆I , ·Ii is an interpretation under set-theoretical semantics, then the following holds:
3. To prove (42) we need category-theoretical semantics of existential and universal restrictions.
3. (42) 実存的・普遍的制約のカテゴリー論的意味論が必要であることを証明する。
0.59
We define an object RX in Cr such that RX −→ R(∃R.D) and dom(RX ) ←−−−−→ ∃R.D ⊓ ∀R.C. This implies that cod(RX ) −→ cod(R(∃R.D)) due to the functor cod from Cr to Cc, and dom(RX ) −→ ∀R.C. By definition, we have cod(R(∃R.D)) −→ D. Thus, cod(RX ) −→ D. Due to Arrow (37) and dom(RX ) −→ ∀R.C, we obtain cod(RX ) −→ C. Hence, cod(RX ) −→ C ⊓ D. By the definition of existential restrictions, we obtain dom(RX ) −→ ∃R.
Since all properties in Lemma 6, 8 and 10 are consequences of those given in these definitions, they can be used to obtain derived arrows (i.e. not independent ones).
It holds that hC0, Oi |= X ⊑ Y (under set-theoretical semantics) if X −→ Y is an arrow in CchC0, Oi.
もし X − Y が Oi の CchC0 の矢印であれば、hC0, Oi |= X > Y (集合論的意味論の下で) が成り立つ。
0.73
Proof. First, each arrow ⊤ −→ ¬E ⊔ F added to CchC0, Oi implies E −→ F due to Arrows (20) and (23) for each axiom E ⊑ F of O. By set-theoretical semantics, we have hC0, Oi |= E ⊑ F .
証明。 まず、cchc0 に加えられた各矢印 ; −→ 〜e , f は、o の各公理 e に対して (20) と (23) の矢印により e −→ f を意味する。 訳抜け防止モード: 証明。 まず、各矢印は、CchC0に付加される。 Oi は Arrows (20 ) による E − → F を意味する。 と (23 ) は O の各公理 E × F に対して成立する。 hC0 , Oi |= E > F である。
0.71
Due to Lemmas 1, 4, 5, 7 and 9, for each arrow X −→ Y introduced by Definitions 4, 5, 6, 7, 8, we have hC0, Oi |= X ⊑ Y .
Lemmas 1, 4, 5, 7 and 9 により、定義 4 5, 6, 7, 8 で導入された各矢印 X − Y は hC0, Oi |= X > Y となる。
0.80
(cid:3)
(第3話)
0.44
英語（論文から抽出）
日本語訳
スコア
We now introduce category-theoretical satisfiability of an ALC concept with respect
ALC概念のカテゴリー論的満足度について紹介する。
0.67
to an ALC ontology.
ALCオントロジーに移行。
0.49
Definition 9. Let C0 be an ALC concept, O an ALC ontology.
定員9名。 C0 を ALC の概念、O を ALC オントロジーとする。
0.68
C is category-theoretical ly unsatifiable with respect to O if there is an ontology category CchC0, Oi which has an arrow C0 −→ ⊥.
c が o に関して圏論的に到達できない(英語版)(category-theoretic ally unsatable)とは、オントロジー圏 cchc0, oi が存在して、矢印 c0 −→ 訳抜け防止モード: C が圏であり、オントロジー圏 CchC0 が存在する場合、理論的には O に対して満足できない。 矢印が C0 − → となる。
0.56
Since an ontology category CchC0, Oi may consist of objects arbitrarily built from the signature, Definition 9 offers possibilities to build a larger ontology category from which new arrows can be discovered by applying arrows given in Definitions (4-8).
Theorem 2. Let O be an ALC ontology and C0 an ALC concept.
定理2。 O を ALC オントロジーとし、C0 を ALC の概念とする。
0.67
C0 is categorytheoreticall y unsatifiable with respect to O iff C0 is set-theoretically unsatifiable.
C0 は O iff C0 に対して圏論的に満足できない。
0.62
To prove this theorem, we need the following preliminary result.
この定理を証明するためには、以下の予備的な結果が必要である。
0.55
Lemma 11. Let O be an ALC ontology and C0 an ALC concept.
背番号11。 O を ALC オントロジーとし、C0 を ALC の概念とする。
0.63
If C0 is set-theoretically unsatifiable with respect to O then C0 is category-theoretical ly unsatifiable.
c0 が o に関して集合論的に不可逆であるなら、c0 は圏論的に可逆である。
0.45
In order to prove this lemma, we use a tableau algorithm to generate from an unsatisfiable ALC concept with respect to an ontology a set of completion trees each of which contains a clash (⊥ or a pair {A, ¬A} where A is a concept name).
この補題を証明するために、我々はtableauアルゴリズムを使用して、a が概念名であるような衝突を含む完備木の集合のオントロジーに関して、不満足な alc 概念から生成する。 訳抜け防止モード: この補題を証明するために、我々はtableauアルゴリズムを使用して、衝突を含む完備木の集合のオントロジーに関して、不満足なalc概念から生成される。 あるいは、ペア { a, \a } ここで a は概念名 )。
0.66
To ensure self-containedness of the paper, we describe here necessary elements which allow to follow the proof of the lemma.
本論文の自己完結性を確保するために, 補題の証明に従うために必要な要素について述べる。
0.77
We refer the readers to [15,16] for formal details.
正式な詳細については読者を[15,16]に参照する。
0.66
We use sub(C0, O) to denote a set of subconcepts in NNF (i.e. negations appear only in front of concept name) from C0 and O. This set is defined as the smallest set such that the following conditions hold :
我々は、C0 と O から NNF における部分概念の集合(すなわち、否定は概念名の前にのみ現れる)を表すために sub(C0, O) を用いる。 訳抜け防止モード: sub(c0, o ) は nnf(すなわち、nnf における部分概念の集合を表す。 概念名の前にのみ現れる否定 ) c0 と o から、この集合は以下の条件が成り立つ最小集合として定義される。
0.76
1. C0 ∈ sub(C0, O) and ¬E ⊔ F ∈ sub(C0, O) for each axiom E ⊑ F ; 2. if ¬C ∈ sub(C0, O) then C ∈ sub(C0, O);
1. c0 ∈ sub(c0, o) で、各公理 e(c0, o) に対して、c0 ∈ sub(c0, o) と、f ∈ sub(c0, o) は、c ∈ sub(c0, o) である。 訳抜け防止モード: 1 . C0 ∈ sub(C0, O ) および >E > F ∈ sub(C0,O) O ) for each axiom E > F ; 2 . if >C ∈ sub(C0, すると C ∈ sub(C0 , O ) ;
0.95
3. if C ⊓ D or C ⊔ D ∈ sub(C0, O) then C, D ∈ sub(C0, O);
3) C, D ∈ sub(C0, O) ならば、C, D ∈ sub(C0, O) である。
0.82
4. if ∃R.C or ∀R.C ∈ sub(C0, O) then C ∈ sub(C0, O).
4. c ∈ sub(c0, o) のとき、c ∈ sub(c0, o) となる。
0.87
A completion tree T = hv0, V, E, Li is a tree where V is a set of nodes, and each node x ∈ V is labelled with L
完備木 T = hv0, V, E, Li は、V がノードの集合であり、各ノード x ∈ V が L でラベル付けされる木である。
0.87
(x) ⊆ sub(C0, O), and a root v0 ∈ V with C ∈ L(v0); E is a set of edges, and each edge hx, yi ∈ E is labelled with a role Lhx, yi = {R} and R ∈ R. In a completion tree T , a node x is blocked by an ancestor y if L
c ∈ l(v0); e の根 v0 ∈ v は辺の集合であり、各辺 hx, yi ∈ e は lhx, yi = {r} および r ∈ r としてラベル付けされる。 訳抜け防止モード: ( x ) > sub(C0, O ) and a root v0 ∈ V with C ∈ L(v0 ) ; E はエッジの集合である。 それぞれの辺 hx, yi ∈ E はロール Lhx でラベル付けされる。 yi = { R } かつ R ∈ R である。 ノード x が L のとき、祖先 y によってブロックされる
0.82
(x) = L (y).
(x) = L (y)。
0.40
To build completion trees, a tableau algorithm starts by initializing a tree T0 and applies the following completion rules to each clash-free tree T (i.e. no node contains a clash):
1. [⊑-rule] for each axiom E ⊑ F of O and each node x, if ¬E ⊔ F /∈ L(x) then
1. O の各公理 E と各ノード x に対し、(a-rule) が sE の F に対して L(x) であるとき、(a-rule) が成り立つ。
0.59
L(x) ← L(x) ∪ {¬E ⊔ F };
L(x) は L(x) である。
0.49
2. [⊓-rule] if E ⊓ F ∈ L(x) and {E, F } * L(x) then L(x) ← L(x) ∪ {E, F };
2) E > F ∈ L(x) かつ {E, F } * L(x) ならば、L(x) > L(x) > {E, F } である。
0.77
3. [⊔-rule] if E ⊔ F ∈ L(x) and {E, F } ∩ L(x) = ∅ then it creates two copies T1 and T2 of the current tree T , and set L(x1) ← L(x1) ∪ {E}, L(x2) ← L(x2) ∪ {F } where xi in Ti is a copy of x from T .
3) E , F ∈ L(x) と {E, F } のとき、現在のツリー T の 2 つのコピー T1 と T2 を生成し、集合 L(x1) を L(x1) と L(x1) と L(x2) を L(x2) と L(x2) と L(x2) と L(x2) の 2 とすると、Ti の xi は T から x のコピーである。
0.81
4. [∃-rule] if ∃R.C ∈ L(x), x is not blocked and x has no edge hx, x′i with L(hx, x′i) =
When [⊔-rule] is applied to a node x of a completion tree T with E ⊔ F ∈ L(x), it generates two children trees T1 and T2 with a node x1 in T1 such that E⊔F, E ∈ L(x1), and a node x2 in T2 such that E ⊔ F, F ∈ L(x2) as described above.
完備木 T のノード x に E の F ∈ L(x) を施すと、T1 のノード x1 と T2 のノード x2 の2つの子木 T1 と T2 のノード x2 を、前述の E の F, F ∈ L(x2) が成り立つ。 訳抜け防止モード: 完備木 t のノード x に対して e が f ∈ l(x ) であるとき、[ ]-rule ] が適用される。 これは2つの子木 t1 と t2 を生成し、ノード x1 を t1 に持つ。 e ∈ l(x1 ) と t2 のノード x2 で e を f とする。 上述の f ∈ l(x2 ) である。
0.81
In this case, we say that T is parent of T1 and T2 by x; or T1 and T2 are children of T by x; x is called a disjunction node by E ⊔F ; and x1, x2 are called disjunct nodes of x by E ⊔F .
この場合、T は x による T1 と T2 の親、または T1 と T2 は x による T の子供、x は E >F による解和ノード、x1, x2 は E >F による x の解和ノードと呼ばれる。
0.85
We use T to denote the tree whose nodes are completion trees generated by the tableau algorithm as described above.
上記のtableauアルゴリズムによって生成されたノードが完了ツリーである木を表すのにtを用いる。
0.79
At any moment, a complete rule is applied only to leaf trees of T. A completion tree is complete if no completion rule is applicable.
完了木は完了規則が適用されない場合、完備木は完備である。
0.40
It was shown that if C is set-theoretically unsatisfiable with respect to O then all complete completion trees contain a clash (an incomplete completion tree may contain a clash) [15,16].
C が O に対して集合論的に満足できないならば、すべての完備木は衝突を含む(不完全完備木は衝突を含むかもしれない) [15,16] 。
0.70
Since this result does not depend on the order of applying completion rules to nodes, we can assume in this proof that the following order [⊑-rule], [⊓-rule], [⊔-rule], [∃-rule] and [∀-rule] is used, and a completion rule should be applied to the most ancestor node if applicable.
(P1) If a node x of a completion tree T contains a clash then x is a leaf node of T .
(P1) 完了木 t のノード x が衝突を含むならば、x は t の葉ノードである。
0.57
(P2) For a completion tree T , if a node y is an ancestor of a node x in T such that x is a disjuntion node and y is a disjunt node of y′, then the children trees by y′ are ancestors of the children trees by x in T.
(P2) 完備木 T に対して、ノード y が T 内のノード x の祖先であり、x が解離ノードであり y が y′ の解離ノードであるなら、y′ による子供ツリーは T における x による子供ツリーの祖先である。
0.65
(P1) tells us that when a clash is discovered in a completion tree T , no rule is applied to any node of T while (P2) is a consequence of the order of rule applications and the fact that each completion rule is applied to the most ancestor node in a completion tree if applicable.
(P1) は、完了ツリー T で衝突が発見されたとき、T の任意のノードには規則が適用されないが、(P2) は規則適用の順序の結果であり、各完了ルールが適用されれば、完了ツリーの最も祖先ノードに適用されるという事実を言う。
0.83
Proof of Lemma 11.
Lemma 11の証明。
0.69
We define an ontology category CchC0, Oi from T by starting from leaf trees of T. By (P1), each leaf tree T of T contains a clash in a leaf node y.
オントロジー圏 CchC0, Oi を T の葉木から始めることにより定義し(P1)、T の各葉木 T は葉ノード y に衝突を含む。
0.65
We add an object dY ∈L(y) Y and an arrow dY ∈L(y) Y −→ ⊥ to CchC0, Oi.
対象 dY ∈L(y) Y と矢印 dY ∈L(y) Y −→ > を CchC0, Oi に追加する。
0.88
In the sequel, we try to define a sequence of arrows started with dY ∈L(y) Y −→ ⊥ which makes clashes propagate from the leaves into the root of T. This propagation has to get through two crucial kinds of passing: from a node of a completion tree to an ancestor that is a disjunct node; and from such a disjunct node in a completion tree to its disjunction node in the parent completion tree in T.
Let T1 and T2 be two leaf trees of T whose parent is T , and y1, y2 two leaf nodes of T1, T2 containing a clash.
T1 と T2 を親が T である T の2本の葉木とし、y1, y2 は衝突を含む T1, T2 の2本の葉ノードとする。 訳抜け防止モード: T1 と T2 を親が T である2本の葉木とする。 and y1, y2 two leaf node of T1, T2 containing a collision 。
0.88
By construction, Ti has a disjunct node xi which is an ancestor of yi with xi 6= yi, and there is no disjunct node between xi and yi (among descendants of xi).
構成上、Ti は xi 6= yi を持つ yi の祖先である分節ノード xi を持ち、xi と yi の間には分節ノードがない(xi の子孫)。
0.74
For each node z between yi and xi if it exists, we add objects dZ∈L(z) Z to CchC0, Oi.
yi と xi の間の各ノード z に対して、CchC0, Oi に対象 dZ∂L(z)Z を加える。
0.76
Let z′ be the parent node of yi.
z′ を yi の親ノードとする。
0.69
By construction, there is a concept ∃R.D ∈ L(z′) and D ∈ L(yi).
構成上、D ∈ L(z′) と D ∈ L(yi) という概念がある。
0.79
In addition, if ∀R.D1 ∈ L(z′) and [∀-rule] is applied to z′ then D1 ∈ L(yi).
We show that D −→ Z or D1 −→ Z for each concept Z ∈ L(yi).
各概念 Z ∈ L(yi) に対して D − → Z または D1 − → Z を示す。
0.84
By construction, [⊔-rule] is not applied to yi (and any node from xi to yi).
構成上は、 yi(およびxi から yi までの任意のノード)には['-rule' は適用されない。
0.72
If Z = ¬E ⊔ F comes from an axiom E ⊑ F , then D −→ ⊤ −→ Z. If Z comes from some Z ⊓ Z ′ then we have to have already D −→ Z ⊓ Z ′ −→ Z or D1 −→ Z ⊓ Z ′ −→ Z. Hence, dY ∈L(yi) Y −→ ⊥ implies D ⊓ d∀R.Di∈L(z ′) Di −→ ⊥.
z が z ′ から来るならば、z は d −→ z ′ −→ z あるいは d1 −→ z ′ −→ z であり、したがって dy ∈l(yi) y −→ z である。 訳抜け防止モード: z が a の公理 e が f であるとき、z は a の公理 e から来る。 このとき、d −→ かつ −→ z である。 z」は「z」の意。 すると、既に d −→ z ′ −→ z である必要がある。 したがって、 dy ∈l(yi ) y −→ z は dy ∈l(yi ) y −→ z を意味する。
0.77
By (34) and (42), we obtain ∃R.D ⊓ d∀R.Di∈L(z ′) ∀R.Di −→ ⊥, and thus dZ∈L(z ′) Z −→ ⊥.
34) と (42) により、dzhtmll(z ′) z −→ が得られ、したがって dzhtmll(z ′) z −→ が与えられる。 訳抜け防止モード: 34 ) と (42 ) により、sR.D は、z ′ である。 したがって、dZ∂L(z ′ ) Z −→ は成り立つ。
0.72
英語（論文から抽出）
日本語訳
スコア
We add an object dX∈L(z ′) X and an arrow dX∈L(z ′) X −→ ⊥ to CchC0, Oi.
対象 dX・L(z ′) X と矢印 dX・L(z ′) X −→ > を CchC0, Oi に加える。
0.76
By using the same argument from z′ until xi, we add an object dX∈L(xi) X and an arrow dX∈L(xi) X −→ ⊥ to CchC0, Oi.
z′ から xi への同じ引数を用いることで、対象 dX・L(xi) X と矢印 dX・L(xi) X −→ を CchC0, Oi に加える。
0.82
We now show dX∈L (x) X −→ ⊥ where x is the disjunction node of xi, L
現在 dX・L (x) x −→ ] ここで x は xi, l の切断ノードである。
0.66
(x) = W ∪ {E ⊔ F }, L(x1) = W ∪ {E ⊔ F, E}, L(x2) = W ∪ {E ⊔ F, F }.
(x) = W > {E > F }, L(x1) = W > {E > F, E}, L(x2) = W > {E > F, F } である。
0.81
Due to (7), we have dV ∈W V ⊓ (E ⊔ F ) −→ (dV ∈W V ⊓ E) ⊔ (dV ∈W V ⊓ F ).
7) により、dV ∈W V > (E > F ) −→ (dV ∈W V > E) > (dV ∈W V > F ) となる。
0.78
Moreover, since dX∈L (xi) X −→ ⊥, we have dV ∈W V ⊓ E −→ dV ∈W V ⊓ (E ⊔ F ) ⊓ E −→ dX∈L(x1) X −→ ⊥ (we have (E ⊔ F ) ⊓ E −→ E due to (1) and (6)), and dV ∈W V ⊓ F −→ dV ∈W V ⊓ (E ⊔ F ) ⊓ F −→ dX∈L(x2) X −→ ⊥.
また、dX・L以来 (xi) X −→ > と、dV ∈W V > E −→ dV ∈W V > (E ) F > E −→ dX∂L(x1) X −→ (E ) F と (6) により、(E ) F −→ E と、dV ∈W V > F −→ dV ∈W V > (E ) F −→ dXが表示されている。
0.67
Therefore, if we add an object dV ∈W V ⊓(E⊔F ) to CchC0, Oi, we obtain an arrow dV ∈W V ⊓(E⊔F ) −→ ⊥ due to (7).
したがって、cchc0, oi に対象 dv ∈w v {\displaystyle dv ∈wv} を付加すると、 (7) により矢印 dv ∈w v {\displaystyle dv ∈wv} が成立する。
0.65
We can apply the same argument from x to the next disjunct node in T which is an ancestor of x according to (P2), and go upwards in T to find its parent and sibling.
同じ引数を x から (P2) に従って x の祖先である T の次の分節ノードに適用し、T を上向きにして親と兄弟を見つけることができる。
0.77
This process can continue and reach the root tree T0 of T. We get dX∈L(x0) X −→ ⊥ where x0 is the root node of T0.
この過程は T の根木 T0 に連続して到達することができる。
0.36
By construction, we have {C} ∪ {¬E ⊔ F | E ⊑ F ∈ O} ⊆ L(x0).
構成上、 {C} {\displaystyle {C} > {C} > {E > F | E > F ∈ O} > L(x0) が成立する。
0.62
Let X ∈ L(x0).
X ∈ L(x0) とする。
0.89
If X = ¬E ⊔ F for some axiom E ⊑ F ∈ O then C −→ ⊤ −→ ¬E ⊔ F .
ある公理 E に対して X = > E > F であれば、C − → > − → > E > F である。
0.68
Moreover, if X = E′ or X = F ′ with C = E′ ⊓ F ′ then C −→ E′ and C −→ F ′.
さらに、X = E′ または X = F′ が C = E′ のとき、C − → E′ と C − → F ′ が成り立つ。
0.92
This implies that C −→ dX∈L(x0) X −→ ⊥.
このことは、C − → dX∂L(x0) X − → ?
0.67
Hence, C −→ ⊥.
したがって、c −→ である。
0.67
Therefore, CchC0, Oi is an ontology category consisting of C −→ ⊥.
したがって、CchC0, Oi は C −→ > からなるオントロジー圏である。
0.73
This completes the proof of the lemma.
これは補題の証明を完結させる。
0.70
Proof of Theorem 2. “⇐=”.
定理2の証明。 “⇐=”.
0.45
Let CchC0, Oi be an ontology category.
CchC0, Oi をオントロジー圏とする。
0.62
Assume that there is an arrow C −→ ⊥ in CchC0, Oi.
CchC0, Oi に矢印 C −→ > が存在すると仮定する。
0.79
Every arrow X −→ Y added to CchC0, Oi must be one of following cases:
CchC0に付加されるすべての矢印 X − → Y に対し、Oi は以下の1つでなければならない。
0.60
(i) X ⊑ Y is an axiom of O. Thus, O |= X ⊑ Y .
(i)x,y は o の公理であり、したがって o |= x, y である。
0.70
(ii) X −→ Y is added by Definitions 4, 5, 6, 7, 8.
(ii) X −→ Y は定義 4, 5, 6, 7, 8 で加算される
0.89
Due to Theorem 1, we have O |= X ⊑ Y .
定理 1 により、O | = X > Y となる。
0.65
(iii) X −→ Y is obtained by transitivity from X −→ Z and Z −→ Y .
(iii) X −→ Y は X −→ Z および Z −→ Y からの推移性によって得られる。
0.78
It holds that O |= X ⊑ Z and O |= Z ⊑ Y imply O |= X ⊑ Y .
これは O |= X > Z かつ O |= Z > Y は O |= X > Y を暗示する。
0.85
Hence, if CchC0, Oi consists of an arrow C −→ ⊥, then O |= C ⊑ ⊥.
したがって、もし CchC0, Oi が矢印 C − → y から成っているなら、O | = C y である。
0.76
“=⇒”. A consequence of Lemma 11.
“=⇒”. 結果は11。
0.43
5 Reasoning in a sublogic of ALC
5 alcのサブロジーにおける推論
0.67
In this section, we identify a new sublogic of ALC, namely ALC∀, obtained from ALC with all the properties introduced in Definitions (4-8), except for Property (37) in Definition 8.
This sublogic cannot be defined under the usual set-theoretical semantics since Property (37) is not independent from Definition 7 and Property (36) in this setting.
Indeed, for every interpretation I it holds that if R′I ⊆ RI, dom(R′)I ⊆ ∀R.CI and x ∈ cod(R′)I , then x ∈ CI .
実際、すべての解釈 I に対して、R'I > RI, dom(R′)I および x ∈ cod(R′)I とすると、x ∈ CI となる。
0.87
First, we need to show the independence of Property (37), i.e. that it is not derived from the other properties introduced in Definitions (4-7) and from Property (36) in Definition 8.
By applying Definitions 2-7, we can add to Cch∀R.D, ∅i other arrows such as ∃R.
定義 2-7 を適用すれば、チェシュR.D や、シイR などの他の矢印に加えることができる。
0.62
¬D ⊓ ¬∃R. ¬D −→ ⊥, ⊤ −→ ∃R.
略称は「d」。 ^D −→ ^R, ^D −→ ^R。
0.34
¬D ⊔ ¬∃R. ¬D and cod(R(∃R.¬D)) −→ ¬D.
略称は「d」。 D と cod(R(\R.\D)) −→ > D である。
0.47
Let R′ be some object in Cch∀R.D, ∅i such that R′ −→ R and dom(R′) −→ ∀R.D. If we apply exhaustively Definitions 2-7 and Property (36) in Definition 8, they never add to Cch∀R.D, ∅i an arrow cod(R′) −→ D, which should be derived by Property (37) in Definition 8.
We can follow the same idea used in Definition 9 to introduce concept unsatisfiabil-
定義9で使われるのと同じ考え方に従い、概念の不満足をもたらすことができる。
0.59
ity for ALC∀ without referring to set interpretation.
集合解釈を参照せずに ALC に対して ity。
0.66
Definition 10 (Category-theoretica l unsatisfiability in ALC∀).
定義 10 (alc における圏論的不満足性)。
0.49
Let C be an ALC∀ concept, O an ALC∀ ontology.
C を ALC の概念、O を ALC オントロジーとする。
0.66
C is category-theoretical ly unsatifiable with respect to O if there is an ontology category CchC, Oi which has an arrow C −→ ⊥.
C {\displaystyle C} が O {\displaystyle O} に関して圏論的に到達できないのは、 C {\displaystyle C} のオントロジー圏 CchC が存在するときである。 訳抜け防止モード: C が圏であり、オントロジー圏 CchC が存在する場合、理論的には O に対して満足できない。 矢印は C − → n である。
0.55
In the sequel, we propose an algorithm for checking satisfiability of an ALC∀ concept C0 with respect to an ontology O. Similarly to the usual set theoretical-semantic s, we can define Negation Normal Form (NNF) NNF(C) of a concept object C, i.e. negations appear only in front of concept name object.
提案手法は,概念オブジェクトCの否定正規形式(NNF) NNF(C) を定義することができ,すなわち,概念名オブジェクトの前にのみ否定が現れる。 訳抜け防止モード: 続編では、オントロジー O に関して ALC の概念 C0 の満足度をチェックするアルゴリズムを提案する。 概念対象 C の否定正規形式 (NNF ) NNF(C ) を定義することができる。 i.e.否定は概念名オブジェクトの前にのみ現れる。
0.68
It is possible to convert polynomially a concept object to its NNF by using the following properties resulting from Lemma 6 and Definition 8.
A smallest set subhC0, Oi of subconcepts occurring in C0 and O is defined as follows:
C0 と O で発生する部分概念の最小集合 subhC0, Oi は次のように定義される。
0.75
1. C0 ∈ subhC0, Oi, and E, F ∈ subhC0, Oi for each axiom E ⊑ F ∈ O;
1. c0 ∈ subhc0, oi, and e, f ∈ subhc0, oi for each axiom e , f ∈ o; 訳抜け防止モード: 1 . C0 ∈ subhC0, Oi, E, F ∈ subhC0。 各公理 E に対する Oi は F ∈ O である。
0.86
2. If E ⊓ F or E ⊔ F ∈ subhC0, Oi then E, F ∈ subhC0, Oi;
2) E, F ∈ subhC0, Oi ならば、E, F ∈ subhC0, Oi である。
0.73
3. If ∃R.D or ∀R.D ∈ subhC0, Oi then D ∈ subhC0, Oi;
3. D ∈ subhC0, Oi, D ∈ subhC0, Oi である。
0.76
4. If C ∈ subhC0, Oi then NNF(¬C) ∈ subhC0, Oi.
4. C ∈ subhC0, Oi ならば NNF(\C) ∈ subhC0, Oi である。
0.86
To check satisfiability of an ALC∀ concept C0 with respect to an ontology O, we initialize an ontology category C hC0, Oi and saturate it by applying the saturation rules in Table 1 to CchC0, Oi until no rule is applicable.
オントロジー O に関する ALC の概念 C0 の満足度を確認するために、オントロジー圏 C hC0, Oi を初期化し、規則が適用されるまでテーブル 1 の飽和規則を CchC0, Oi に適用して飽和させる。
0.80
Each saturation rule in Table 1 corresponds to a property given in the definitions of constructor semantics.
表1のそれぞれの飽和規則は、コンストラクタ意味論の定義で与えられる性質に対応する。
0.72
Moreover, we adopt the following assumptions when designing the algorithm.
さらに,アルゴリズムの設計には以下の仮定を採用する。
0.78
1. The collections Ob(C ) and Hom(C ) of a category C built by the algorithm are
1.アルゴリズムによって構築されたカテゴリCの集合 Ob(C ) と Hom(C ) は、
0.88
considered as sets, i.e there are no duplicate in them.
集合と見なされ、その中に重複は存在しない。
0.71
英語（論文から抽出）
日本語訳
スコア
[⊥-rule] If X −→ NNF(¬C), X −→ C are arrows of Cc, and X −→ ⊥ is not an arrow of Cc, then we add an object C ⊓ NNF(¬C) and an arrow X −→ ⊥ to Cc.
[a-rule] X −→ NNF(シュC)、X −→ C が Cc の矢印であり、X −→ は Cc の矢印ではないなら、対象 C を Cc に NNF(シュC) と矢印を付加する。
0.74
[⊥m-rule] If there is an arrow E ⊓ F −→ ⊥ in Cc, and there is no arrow E −→ NNF(¬F ) or F −→ NNF(¬E) in Cc, then we add arrows E −→ NNF(¬F ) and F −→ NNF(¬E) to Cc.
[m-ルル] Cc に矢 E −→ NNF(シュフ) または F −→ NNF(シュフ) が存在しなければ、Cc に矢 E −→ NNF(シュフ) と F −→ NNF(シュフ) を加える。 訳抜け防止モード: [......-規則]もしも Cc には矢印 E > F −→ > が存在する。 そして、Cc には矢印 E −→ NNF(aF ) や F −→ NNF(aE ) は存在しない。 すると、矢印 E −→ NNF と F −→ NNF を Cc に加える。
0.79
[⊤-rule] If NNF(¬C) −→ X, C −→ X are arrows of Cc, and ⊤ −→ X is not an arrow of Cc, then we add an object C ⊔ NNF(¬C) and an arrow ⊤ −→ X to Cc.
c −→ x が cc の矢印であり、c −→ x が cc の矢印ではないなら、対象 c が nnf(\c) で矢印が −→ x を cc に追加する。 訳抜け防止モード: c − → x が cc の矢印であるなら、nnf(\c ) −→ x は c の矢印である。 x は cc の矢印ではない。 すると、対象 c を nnf(\c ) とし、矢印を cc に −→ x と加える。
0.63
[⊤m-rule] If there is an arrow ⊤ −→ E ⊔ F in Cc, and there is no arrow NNF(¬F ) −→ E or NNF(¬E) −→ F in Cc, then we add arrows NNF(¬F ) −→ E and NNF(¬E) −→ F to Cc.
] Cc にアローがあるならば、Cc にアロー NNF(シュF ) −→ E または NNF(シュE) −→ F が存在しないならば、アロー NNF(シュF ) −→ E と NNF(シュE) −→ F を Cc に付加する。
0.76
[¬-rule] If there is an arrow C −→ D in Cc and there is no arrow NNF(¬D) −→ NNF(¬C) in Cc, then we add objects NNF(¬C), NNF(¬D) and an arrow NNF(¬D) −→ NNF(¬C) to Cc.
Cc に矢印 C − → D が存在し、Cc に矢印 NNF(シュD) −→ NNF(シュC) が存在しない場合、対象 NNF(シュC)、NNF(シュD) と矢印 NNF(シュD) −→ NNF(シュC) を Cc に追加する。
0.76
[⊓-rule] If there is an object E ⊓ F of Cc and there are arrows E ⊓ F −→ E and E ⊓ F −→ F , then we add objects E, F and arrows E ⊓ F −→ E, E ⊓ F −→ F to Cc.
[a-rule] Cc の対象 E > F が存在し、矢 E > F − → E と E > F − → F が存在するなら、対象 E , F と矢 E > F − → E, E > F − → F を Cc に加える。
0.82
[⊓m-rule] If there is an object E ⊓ F and arrows X −→ E, X −→ F in Cc, and there is no arrow X −→ E ⊓ F in Cc, then we add an arrow X −→ E ⊓ F to Cc.
〔m-ルル〕 Cc に対象 E − F と矢印 X −→ E, X −→ F が存在し、Cc に矢印 X −→ E > F が存在しないなら、Cc に矢印 X −→ E > F を加える。
0.82
[⊔-rule] If there is an object E ⊔ F in Cc and there are not two arrows E −→ E ⊔ F and F −→ E ⊔ F , then we add objects E, F and arrows E −→ E ⊔ F , F −→ E ⊔ F to Cc.
もし cc に対象 e −→ e と f −→ e と f が存在しないならば、対象 e と f と矢印 e −→ e と f とを cc に加える。 訳抜け防止モード: もしも... Cc に対象 E > F が存在する そして、2つの矢印 E − → E {\displaystyle E} と F − → E {\displaystyle F} は存在しない。 すると、対象 E, F と矢印 E − → E > F を加える。 F−→E−F〜Cc。
0.81
[⊔m-rule] If there is an object E ⊔ F and arrows E −→ X, F −→ X in Cc, and there is no arrow E ⊔ F −→ X in Cc, then we add an arrow E ⊔ F −→ X to Cc.
〔m-ルル〕 Cc に対象 E > F と矢 E − → X が存在し、Cc に矢 E > F − → X が存在しないなら、Cc に矢 E > F − → X を加える。 訳抜け防止モード: [ >m - rule ] オブジェクト E > F が存在する場合 そして矢印 E −→ X, F −→ X in Cc, そして、Cc に矢 E > F − → X は存在しない。 すると、矢印 E は Cc に F − → X を加える。
0.84
[⊔dis-rule] If there are two objects C ⊓ (D ⊔ E) and W in Cc, and there is no arrow C ⊓ (D ⊔ E) −→ W in Cc, and check(Cc, C ⊓ (D ⊔ E), W ) returns “true”, then we add an arrow C ⊓ (D ⊔ E) −→ W to Cc.
] Cc に 2 つの対象 C , W が存在し、Cc に矢印 C , (D , E) − → W が存在しなければ、チェック(Cc, C , E) は "true" を返すので、Cc に矢印 C , (D , E) −→ W を加える。
0.67
[∃-rule] If there is an object ∃R.D of Cc, there is no object R(∃R.D) of Cr, then we add objects R(∃R.D), R, an arrow R(∃R.D) −→ R to Cr, and add to Cc objects D, cod(R(∃R.D)), dom(R(∃R.D)), arrows cod(R(∃R.D)) −→ D, dom(R(∃R.D)) ← [∃m-rule] If there is an object ∃R.D of Cc and an object R′ of Cr such that R′ −→ R and cod(R′) −→ D, and there is no arrow dom(R′) −→ dom(R(∃R.D)), then we add to Cc an arrow dom(R′) −→ dom(R(∃R.D)).
ヘールル] Cc の対象 R(、R.D) が Cc の対象 R(、R の対象 R(、R.D) が存在しないなら、R の対象 R(、R のオブジェクト R(、R.D) − → R を Cr に加え、Cc の対象 D, cod(R(、R.D)), dom(、R(、R.D)) −→ D, dom(R(、R.D))) , [、[、m-rule] が Cc の対象 R′ と Cr の対象 R′ が存在し、R′ − R と cod(R′) − D が存在しない。 訳抜け防止モード: ] Cc の対象 R.D が存在するなら、 Cr の対象 R(nR.D ) が存在しなければ、対象 R(nR.D ) を追加する。 R は Cr への矢印 R(nR.D ) − → R である。 そして Cc オブジェクト D, cod(R(\R.D ) ), dom(R(\R.D ) ) に追加する。 矢印 cod(R(、R.D ) ) −→ D, dom(R(、R.D ) ) . [ .m - rule ] Cc のオブジェクト R.D と Cr のオブジェクト R′ が存在して、R′ − → R と cod(R′ ) − → D が成り立つ。 矢印 dom(R′ ) −→ dom(R(\R.D ) ) は存在しない。 すると Cc に矢印 dom(R′ ) −→ dom(R(\R.D ) ) を加える。
0.86
[∀-rule] If there is an object ∀R.C in Cc and there are no arrows ∀R.C ← in Cc, NNF(¬∃R.¬C) to Cc.
[a-rule] Cc に対象 R.C が存在していて、Cc に矢が存在しない場合、Cc に NNF(nR.C) は存在しない。
0.64
[trans-rule] If there are objects X, Y, Z and arrows X −→ Y , Y −→ Z of Cc, there is no arrow X −→ Z of Cc, then we add an arrow X −→ Z to Cc.
[トランスルール] Cc の対象 X, Y, Z と矢印 X − Y , Y − → Z が存在していれば、Cc の矢印 X − → Z は存在しないので、矢印 X − → Z を Cc に追加する。
0.87
[dc-rule] (a) If R is an object of Cr, and X −→ ⊥ is an arrow of Cc for some X ∈ {dom(R), cod(R)}, and Y −→ ⊥ is not an arrow of Cc for some Y ∈ {dom(R), cod(R)}, then we add Y −→ ⊥ to Cc.
[dcルール] (a) R を Cr の対象とし、X−1 をある X ∈ {dom(R), cod(R)} に対して Cc の矢印とし、Y−1 をある Y ∈ {dom(R), cod(R)} に対する Cc の矢印とすると、Y −→ を Cc に追加する。 訳抜け防止モード: [dcルール] (a) R は Cr の対象である。 そして X −→ は、ある X ∈ { dom(R ) に対して Cc の矢印である。 cod(R ) }, and Y −→ > は、ある Y ∈ { dom(R ) に対して Cc の矢印ではない。 cod(R ) } ならば、Cc に Y −→ > を加算する。
0.85
(b) If R −→ R′ (X, Y ) ∈ n(cid:0)dom(R), dom(R′)(cid:1) ,(cid:0)cod(R), cod(R′)(cid:1)o, then we add to Cc an arrow X −→ Y
b) R − → R′ (X, Y ) ∈ n(cid:0)dom(R), dom(R′)(cid:1) ,(cid:0)cod(R), cod(R′)(cid:1)o の場合、矢印 X − → Y を Cc に加える。
0.93
then we add objects ∃R.NNF(¬C), NNF(¬∃R.¬C) and arrows ∀R.C ←
すると、オブジェクト を R.NNF に、NNF に、矢印 を R.C に、加える。
0.54
is an arrow of Cr and X −→ Y is not an arrow of Cc, for some
Cr の矢であり、X − → Y は Cc の矢ではない。
0.65
→ NNF(¬∃R.¬C)
→ nnf(\r.\c)
0.31
− − − → − −
− − − → − −
0.43
− → ∃R.D.
− 略称は「R.D.」。
0.33
− to Cc. − − −
− CCへ。 − − −
0.45
− − Table 1: Saturation rules
− − 表1:飽和規則
0.53
英語（論文から抽出）
日本語訳
スコア
Input Output: true or false
入力出力: true or false
0.81
: hC0, Oi where C0 is an ALC ∀ concept and O an ontology
: hC0, C0 が ALC > の概念であり、O がオントロジーである Oi
0.71
1 Initialize two categories Cc and Cr; 2 Add an object C0 to Cc; 3 foreach E ⊑ F of O do 4 5 end 6 while there is a saturation rule r that is applicable to Cc and Cr do
1 二つのカテゴリ Cc と Cr; 2 を初期化する; Cc に対象 C0; 3 を付加する; O do 4 5 end 6 に対して、Cc と Cr に適用される飽和規則 r が存在する間、O do 4 5 end 6 を許す。
0.75
Add objects E, F and an arrow E −→ F to Cc;
対象 E, F と矢印 E − → F を Cc に追加する。
0.82
Apply r to Cc and Cr;
r を Cc と Cr に適用する。
0.77
7 8 end 9 if there is an arrow C0 −→ ⊥ in Cc then 10 11 end 12 else
7 8 end 9 cc に矢印 c0 −→ s があるなら 10 11 end 12 である。
0.81
return false; 13 14 end
を返します。 1314回終了。
0.52
return true;
true を返します。
0.56
Algorithm 1: isSatisfiablehC0, Oi
アルゴリズム1:isSatisfiablehC0,O i
0.78
Input : hCc, (C1 ⊔ D1) ⊓ · · · ⊓ (Cn ⊔ Dn), W i where Cc is an category and
入力 Cc が圏である W i に対し、hCc は (C1 > D1) > · · · · · (Cn > Dn) である。
0.73
(C1 ⊔ D1) ⊓ · · · ⊓ (Cn ⊔ Dn) and W are objects of Cc
(C1, D1) · · · · · (Cn, Dn) および W は Cc の対象である
0.92
Output: true or false 1 Γ ← ∅; 2 foreach (X1, · · · , Xn) with Xi ∈ {Ci, Di} do 3
出力:真か偽か x1, · · · · · , xn) と xi ∈ {ci, di} do 3 を持つ 2 個のforeach (x1, · · · · · · , xn) 訳抜け防止モード: 出力:真か偽か 1 Γ ← ∅ ; 2 foreach ( X1, · · ·, xi ∈ { ci , di } do 3 を持つ xn )
0.58
if there is no object (Xi1 ⊓ · · · ⊓ Xik ) in Cc with 1 ≤ ij ≤ n such that there is an arrow (Xi1 ⊓ · · · ⊓ Xik ) −→ W in Cc then
1 ≤ ij ≤ n の Cc に対象 (Xi1 の · · · · の Xik ) が存在しないなら、Cc に矢印 (Xi1 の · · · · の Xik ) − → W が存在する。
0.84
4 5 end return false ;
4 5 終わり を返します。
0.54
6 end 7 return true ;
6 end 7 return true ;
0.43
Algorithm 2: checkhCc, (C1 ⊔ D1) ⊓ · · · ⊓ (Cn ⊔ Dn), W i
アルゴリズム2: checkhcc, (c1, d1) , · · · (cn, dn), w i
0.73
2. When the algorithm adds an object X to a category C , it adds also an identity arrow X −→ X, and ⊥ −→ X, X −→ ⊤ where ⊥, ⊤ are initial and terminal objects of C .
2. アルゴリズムが圏 C に対象 X を追加するとき、その対象 X − → X と、その元 X − → X , X − → X を加える。 訳抜け防止モード: 2 . アルゴリズムが圏 c に対象 x を追加するとき、 また、恒等矢印 x −→ x と、x −→ x, x −→ を加えている。 c の始終対象と終端対象である。
0.61
In particular, if an object X is added to a concept ontology category, it adds NNF(X) as well.
特に、オブジェクト X が概念オントロジー圏に追加されると、NNF(X) も追加される。
0.63
For the sake of simplicity, we will not mention explicitly these arrows in the rules described in Table 1.
単純さのため、表1に記載された規則では、これらの矢印を明示的に言及しません。
0.69
Lemma 12 (Complexity).
詳細はLemma 12を参照。
0.50
Let C be an ALC ∀ concept and O an ontology.
C を ALC > の概念とし、O をオントロジーとする。
0.69
Algorithm 1 runs in polynomial space for the input hC, Oi.
アルゴリズム1は入力hC, Oiの多項式空間で実行される。
0.81
Proof. Since there are at most two arrows between two objects, it suffices to determine the number of different objects added to Cc and Cr.
These two rules correspond to Definition 11.2, objects added to
この2つのルールは、定義 11.2 に対応する。
0.62
Cc are already part of subhC0, Oi, meaning there are O(n2) of them.
Cc は、既にsubhC0, Oi の一部であり、O(n2) が存在する。
0.86
3. [∃-rule]. Objects D added to Cc by this rule are already part of subhC0, Oi according to Definition 11.3, following the same reasoning as for the previous rules, we have O(n2) of them.
3.[オ・ルル]。 この規則によりccに追加されたオブジェクトdは、定義 11.3 に従って既に subhc0, oi の一部であり、以前のルールと同じ理由により、o(n2) を持つ。
0.66
Remaining objects to be added to Cc, namely cod(R(∃R.D)) and dom(R(∃R.D)), are not part of subhC0, Oi.
Cc に残すべきオブジェクト、すなわち cod(R(\R.D)) と dom(R(\R.D)) は、サブhC0, Oi の一部ではない。
0.75
However, they are only added once per each occurrence of object of the form ∃R.D in subhC0, Oi, i.e. the number of object added is bounded by 2k.
In total, this rule add a number of to Cc object smaller than 3k ≤ O(n2).
総じて、この規則は 3k ≤ O(n2) より小さい Cc オブジェクトに数を加えている。
0.80
We leave the number of objects added to CR for later.
CRに追加されたオブジェクトの数を後ほど残します。
0.77
4. [∀-rule]. From Definition 11.4, NNF(¬∀R.D) ←−−−−→ ∃R.NNF(¬D) is already part of subhC0, Oi.
4.[オ・ルル]。 定義 11.4 から NNF は、既に subhC0, Oi の一部となっている。
0.52
Only ∃R. ¬D isn’t part of Definition 11, however, it is linearly bounded by the number of object of the form ∀R.D which is smaller than k, hence this rule add at most 2k ≤ O(n2) objects to Cc in total.
These rules only add one object of the type C ⊓ NNF(¬C) or C ⊔ NNF(¬C) to Cc per object C, respectively.
これらの規則は、C の Cc に対して、C の型 C は NNF または C は NNF である。 訳抜け防止モード: これらのルールは、C型の1つのオブジェクトのみを追加する。 あるいは、C のオブジェクト C あたり C から Cc に NNF を割り当てる。
0.69
Assume that we have applied the rule once on a single X and added C ⊓ NNF(¬C) or C ⊔ NNF(¬C) to Cc.
1つの X に一度この規則を適用し、Cc に C > NNF(\C) または C > NNF(\C) を加えたと仮定する。
0.75
If there is an other Y such that Y −→ C and Y −→ NNF(¬C) or C −→ Y and NNF(¬C) −→ Y , we can apply the rules nonetheless, however, it won’t add another occurrence of C ⊓ NNF(¬C) or C ⊔ NNF(¬C) since we are dealing with sets so an object can appear one and only one time - and there’s already an occurrence of it since we have applied the rule before.
他の Y が存在して Y −→ C と Y −→ NNF(シュC) または C −→ Y と NNF(シュC) −→ Y が成り立つと、その規則を適用することはできるが、それ以外は C の NNF(シュC) や C の NNF(シュC) が現れることはない。 訳抜け防止モード: もしそのようなYが存在するなら Y −→ C と Y −→ NNF または C −→ Y と NNF と Y である。 それでもルールを適用することは可能ですが、C の NNF や C の NNF の別の発生は加えません。 物体が1回だけ現れるように 集合を扱います ルールを適用して以来、すでにそれが発生しています。
0.62
So the number of object added by these rules is bounded by k ≤ O(n2).
したがって、これらの規則によって加えられるオブジェクトの数は k ≤ o(n2) で区切られる。
0.67
6. [¬-rule].
6. (複数形 6.s)
0.53
If we have an arrow C −→ D in Cc, C and D are already in Cc, consquently NNF(¬C) and NNF(¬D) as well.
cc に矢印 c −→ d がある場合、c と d は既に cc に存在し、nnf(-c) と nnf(-d) も対応している。
0.59
Since we are dealing with sets, we are not adding any new objects.
For [∃-rule] the number of objects R(∃R.D) added to Cr is bounded by ℓ.
ルルルルル] に対し、Cr に加わった対象 R(nR.D) の数は l で有界である。
0.64
Objects R are only added to Cr once per role name appearing in T , it is also bounded by ℓ.
対象 R は T に現れるロール名に対して 1 度だけ Cr に付加されるが、l で有界である。
0.62
In summary, each rule adds to Cc a number of objects bounded by O(n2), the number of objects of Cr is also bounded by O(n2), thus Algorithm 1 runs in polynomial space.
まとめると、各規則は Cc に O(n2) で有界な多くの対象を追加し、Cr の対象の数は O(n2) で有界であるので、アルゴリズム1 は多項式空間で動く。
0.73
(cid:3) Lemma 13 (soundness and completeness).
(第3話) Lemma 13 (音と完全性)。
0.62
Let C0 be an ALC∀ concept and O an ontology.
C0 を ALC の概念とし、O をオントロジーとする。
0.66
Algorithm 1 returns “false” with the input hC0, Oi iff C0 is unsatisfiable with respect to O.
アルゴリズム1は入力 hC0 で "false" を返すが、Oi iff C0 は O に対して満足できない。
0.80
Proof. “⇐=”.
証明。 “⇐=”.
0.43
Let Cc be a category built by Algorithm 1 that returns “false”.
Cc を Algorithm 1 で構築されたカテゴリとして "false" を返す。
0.81
This implies that Cc has an arrow C0 −→ ⊥.
これは、Cc が矢印 C0 − → y を持つことを意味する。
0.64
First, we show that Cc satisfies all properties in Definitions 2-7 and Property (36) in Definition 8.
まず, cc が定義 2-7 のすべての性質と定義 8 のプロパティ (36) を満たすことを示す。
0.79
1. Definition 2. When a saturating rule in Table 1 adds a new concept (resp. role) object, it adds also an identity arrow and arrows between the object and ⊥ (resp. R⊥) and ⊤ (resp. R⊤).
1.定義 2. 表1の飽和規則が新しい概念(resp. role)オブジェクトを追加するとき、オブジェクトとオブジェクトの間に恒等矢印と矢印(resp. R. R.)と、(resp. R. R.)を追加する。
0.60
Thus, Properties 1 and 2 in Definition 2 hold in Cc.
したがって、定義 2 のプロパティ 1 と 2 は cc に格納される。
0.66
Moreover, when Algorithm 1 returns “true”, the loop from Line 6 terminates, and thus no rule is applicable.
さらに、アルゴリズム1が“true”を返すと、行6からのループが終了し、ルールは適用されない。
0.83
That means [trans-rule] is not applicable.
つまり[トランスルール]は適用されない。
0.73
This implies that Property 3 in Definition 2 holds in Cc.
これは、定義 2 のプロパティ 3 が Cc に保持されていることを意味する。
0.54
Analogously, [dc-rule] is not applicable when Algorithm 1 returns “true”.
アルゴリズム 1 が "true" を返すとき、[dc-rule] は適用できない。
0.75
Hence, Property 4 in Definition 2 is ensured in Cc, and thus in C ′ c.
したがって、定義 2 のプロパティ 4 は Cc で、したがって C ′ c で保証される。
0.81
2. Definition 3. By the assumption, for each object X added to Cc, there is also NNF(¬X) in Cc.
2.定義 3. 仮定により、Cc に追加された各対象 X に対して、Cc には NNF( ) が存在する。
0.83
In this case, non applicability of [⊥-rule] and [⊤-rule] guarantees that there are arrows NNF(¬X) ⊓ X −→ ⊥, ⊤ −→ NNF(¬X) ⊔ X in Cc.
Let C ⊓ X −→ ⊥ (resp. ⊤ −→ C ⊔ X) be an arrow in Cc.
C {\displaystyle C} を C c {\displaystyle C} の矢印とすると、 C {\displaystyle C} は X {\displaystyle X} の矢印となる。
0.48
Non applicability of [⊥m-rule] and [⊤m-rule] implies that there are arrows C −→ NNF(¬X), X −→ NNF(¬C) (resp.
非適用性は、矢印 C −→ NNF(シュX)、X −→ NNF(シュC) (resp) が存在することを意味する。
0.69
NNF(¬X) −→ C, NNF(¬C) −→ X) in Cc.
Cc における NNF(nX) −→ C, NNF(nC) −→ X)。
0.87
3. Definition 4. Let E, F and E ⊔ F be objects of Cc.
3.定義 4. E, F, E を Cc の対象とする。
0.74
Thanks to [⊔-rule], Cc has arrows E −→ E ⊔ F and F −→ E ⊔ F which ensure Property (1) in Definition
Cc の矢印は E − → E {\displaystyle E} と F − → E {\displaystyle F} であり、定義において性質 (1) を保証する。 訳抜け防止モード: Cc の矢印は E −→ E > F である。 そして F − → E {\displaystyle F} 定義におけるプロパティ(1 )を保証する
0.87
4. Let E −→ X and F −→ X be arrows in Cc, and E ⊔ F be an object of Cc.
4. E −→ X と F −→ X を Cc の矢印とし、E > F を Cc の対象とする。
0.86
Non-applicability of [⊔m-rule] ensures that there is an arrow E ⊔ F −→ X in Cc.
アームルルの非適用性は、Cc に矢印 E > F − → X が存在することを保証する。
0.68
Hence, Property (2) in Definition 4 holds.
したがって、Property (2) in Definition 4 は保持する。
0.78
4. Definition 5. Let E, F and E ⊓ F be objects of Cc.
4.定義 5. E, F および E > F を Cc の対象とする。
0.60
Thanks to [⊓-rule], we have arrows E ⊓ F −→ E and E ⊓ F −→ F which ensures Property (5) in Definition
E は F −→ E であり、E は F −→ F であり、定義において性質 (5) を保証する。
0.75
5. Assume that X −→ E and X −→ F be arrows in Cc, and E ⊓ F be an object of Cc.
5. X − → E と X − → F が Cc の矢印であり、E = F が Cc の対象であると仮定する。
0.85
Non-applicability of [⊓m-rule] ensures that there is an arrow X −→ E ⊓ F in Cc.
非適用性は、cc に矢印 x −→ e {\displaystyle x} が存在することを保証する。
0.59
Hence, Property (6) in Definition 5 holds.
したがって、定義 5 のプロパティ (6) は成立する。
0.78
Assume that C ⊓ (D ⊔ E), and (C ⊓ D) ⊔ (C ⊓ E) be objects in Cc.
C は(D ) E で、(C ) D は(C ) E で、(C ) E は Cc の対象であると仮定する。
0.79
Due to non-applicability of [⊔-rule], Cc has objects C ⊓ D, C ⊓ E and arrows C ⊓ D −→ (C ⊓ D) ⊔ (C ⊓ E) and C ⊓E −→ (C ⊓D)⊔(C ⊓E), i.e check(Cc, C ⊓(D⊔E), (C ⊓D)⊔(C ⊓E)) returns “true”.
Cc の非適用性のため、Cc は対象 C は D, C は E であり、矢印 C は D −→ (C ) D と (C ) E であり、C は E −→ (C ) D と (C ) E と (C ) D と (C ) E と (C ) E と (C ) E ) {\displaystyle (Cc,C )(D)E), (C )D ) は "true" を返す。
0.77
Due to non-applicability of [⊔dis-rule], Cc has an arrow C ⊓ (D ⊔ E) −→ (C ⊓ D) ⊔ (C ⊓ E).
5. Definition 6. Let C, NNF(¬C), C ⊓ NNF(¬C), C ⊔ NNF(¬C), C ⊓ X, C ⊔ X be objects of Cc.
5.定義 6. c, nnf(\c), c , nnf(\c), c . nnf(\c), c . nnf(\c), c . x, c . x を cc の対象とする。 訳抜け防止モード: 5.定義 6 . c, nnf(\c ), c , nnf(\c ) とする。 c(c) , c(c) , c(x) , c(x) は cc の対象である。
0.53
Due to non-applicability of [⊥-rule] and [⊤-rule], Cc has arrows C ⊓ NNF(¬C) −→ ⊥, ⊤ −→ C ⊔ NNF(¬C).
Cc の矢印 C は、[n-rule] と [n-rule] の非適用性のため、C の矢印 C は、(C) の矢印である。
0.65
Assume that Cc has an arrow C ⊓ X −→ ⊥ (resp. ⊤ −→ C ⊔ X).
Cc が矢印 C > X − → > (resp. > − → C > X) を持つと仮定する。
0.78
Due to non-applicability of [⊥m-rule] and
m-rule と in-applicability の非適用性のため
0.58
英語（論文から抽出）
日本語訳
スコア
[⊤m-rule], Cc has arrows C −→ NNF(¬X) (resp.
[n-rule], Cc は矢印 C −→ NNF(\X) (resp) を持つ。
0.74
NNF(¬X) −→ C).
NNF(nX) −→C)。
0.77
Hence, Properties (17)-(20) in Definition 6 hold.
したがって、定義6のプロパティ (17)-(20) は保持される。
0.81
6. Definition 7. Let ∃R.C be an object of Cc.
6.定義 7. c を cc の対象とする。
0.52
Due to non-applicability of [∃-rule], it follows that R(∃R.C), R are objects, and R(∃R.C) −→ R is an arrow of Cr; and dom(R(∃R.C)), cod(R(∃R.C)), C are objects, and dom(R(∃R.C)) ←−−−−→ ∃R.C, codR(∃R.C)) −→ C are arrows of Cc.
r(r.c) −→ r は cr の矢印であり、dom(r(sr.c)) cod(r(sr.c)) c はオブジェクト、dom(r(sr.c)) は cc の矢印である。 訳抜け防止モード: R(R.C) の非適用性から従う。 R は対象であり、R は Cr の矢印である。 と dom(R(、R.C ) )、cod(R(、R.C ) ) Cはオブジェクトです。 および dom(R(、R.C ) ) シュ−−−−−−→ シュR.C, codR(、R.C ) ) −→ C は Cc の矢印である。
0.85
Let R′ be an object of Cr such that R′ −→ R is an arrow of Cr, and cod(R′) −→ C is an arrow of Cc.
R′ を Cr の対象とし、R′ − → R を Cr の矢、cod(R′) − → C を Cc の矢印とする。
0.84
Due to non-applicability of [∃m-rule], it follows that dom(R′) −→ dom(R(∃R.C)) is an arrow of Cc.
非適用性のため、 dom(R′) −→ dom(R(\R.C)) は Cc の矢印である。
0.70
Hence, all properties in Definition 7 hold.
したがって、定義7のすべての性質は成立する。
0.70
7. Property (36) in Definition
7. 定義上の財産(36)
0.77
8. If there is an object ∀R.C occurring in Cc, it is converted in ¬∃R.
8. cc に _r.c がある場合、それは _r で変換される。 訳抜け防止モード: 8 . Cc で発生するオブジェクト ?R.C が存在する場合、 Rで変換される。
0.76
¬C due to the assumption that all objects of Cc are in NNF.
Cc のすべてのオブジェクトが NNF 内にあるという仮定のためである。
0.69
Hence, Property (36) holds.
したがって、プロパティ(36)が保持される。
0.63
We have showed that Cc satisfy all properties in Definitions 2-7 and Property (36) in Definition 8 except that Property 7 in Definition 5.
Indeed, if Cc has an object C ⊓ (D ⊔ E), it may not have an arrow C ⊓ (D ⊔ E) −→ (C ⊓ D) ⊔ (D ⊓ E) with object (C ⊓ D) ⊔ (D ⊓ E).
実のところ、cc が対象 c を成すならば、その矢印 c は対象 (c) が (c) で (d) −→ (c) (d) が (d) であるような矢印は持たないかもしれない。
0.62
To complete it, we define a category C ′
これを完遂するために、圏 C ′ を定義する。
0.50
c that is an extension of Cc by adding objects and arrows satisfying Property 7 in Definition 5, i.e if C ′ c has an object C ⊓ (D ⊔ E) then is has also an object (C ⊓ D) ⊔ (D ⊓ E).
c は、定義 5 でプロパティ 7 を満たすオブジェクトと矢印を加えることで cc の拡張であり、c ′ c が c ′ のオブジェクトを持つなら、c ′ d のオブジェクトも持つ。 訳抜け防止モード: 定義5でプロパティ7を満たすオブジェクトと矢印を追加することでCcの拡張です。 すなわち、C ′ c が対象 C > ( D > E ) {\displaystyle C\,} を持つなら、対象 ( C > D ) {\displaystyle (C > D ) \,} を持つ。
0.80
Then we apply saturation rules in Table 1 to C ′ c until no rule is applicable.
そして、規則が適用されない限り、表 1 の飽和規則を C ′ c に適用する。
0.76
We can use the same argument above to show that C ′ c satisfy all properties in Definitions 2-7 and Property (36) in Definition 8.
同じ議論を用いて、C ′ c が定義 8 における定義 2-7 と性質 (36) の全ての性質を満たすことを示すことができる。
0.80
Since Cc has an arrow C0 −→ ⊥, C ′ c does.
Cc は矢印 C0 −→ s を持つので、C ′ c は成り立つ。
0.79
According to Definition 10, C0 is unsatisfiable in ALC∀ with respect to O. “=⇒”.
定義 10 によれば、C0 は O. “= ” に関して ALC では満足できない。
0.81
Assume that CchC0, Oi, CrhC0, Oi are smallest concept and role ontology categories according to the definitions, i.e they have only necessary objects and arrows which satisfy the dfinition.
CchC0, Oi, CrhC0, Oi は定義に従って最小の概念とロールオントロジー圏であると仮定する。 訳抜け防止モード: CchC0, Oi, CrhC0, Oi は定義に従って最小の概念と役割オントロジー圏であると仮定する。 つまり 限界を満たす 必要な物と矢しか持たない。
0.76
By hypothesis, CchC0, Oi has an arrow C0 −→ ⊥.
cchc0 の仮説により、oi は矢印 c0 −→ s を持つ。
0.66
We use hCc, Cri to denote the concept and role ontology categories built by Algorithm 1.We define a function π from Ob(Cc) ∪ Ob(Cr) to Ob(CchC0, Oi) ∪ Ob(CrhC0, Oi).
Since CchC0, Oi and each Cc have objects C0, and E, F for all axiom E ⊑ F (Line 2 and the loop from Line 3), π can be initialized with π(C0) = C0 and π(E) = E, π(F ) = F .
CchC0, Oi および各 Cc は対象 C0, E, F を持つので、すべての公理 E に対して π(C0) = C0 と π(E) = E, π(F ) = F で初期化することができる。 訳抜け防止モード: CchC0 と Oi と各 Cc は対象 C0 を持つ。 と E, F はすべての公理 E, F ( 2 行) 3 行からのループは π(C0 ) = C0 で初期化できる。 そして π(E ) = E , π(F ) = F である。
0.84
Thus, the following properties hold for all current π.
したがって、以下の性質はすべての電流 π に対して成り立つ。
0.68
π(X) = X for each object X ∈ Ob(Cc) ∪ Ob(Cr) X −→ Y ⇐⇒ π(X) −→ π(Y )
π(X) = X for each object X ∈ Ob(Cc) ^ Ob(Cr) X −→ Y ^ π(X) −→ π(Y)) 訳抜け防止モード: 各対象 x ∈ ob(cc ) に対して π(x ) = x である。 π(x ) −→ π(y ) である。
0.67
(44) (45) We will extend π such that Properties (44) and (45) are preserved for each applica-
This implies that Properties (44) and (45) are preserved.
これは、特性 (44) と (45) が保存されていることを意味する。
0.62
英語（論文から抽出）
日本語訳
スコア
2. [⊓-rule] and [⊔-rule].
2. [-rule] と [-rule] である。
0.86
These rules are applied to objects C ⊓ D and C ⊔ D for adding to Cc the following arrows C ⊓ D −→ C, C ⊓ D −→ D, C −→ C ⊔ D, D −→ C ⊔ D. Since CchC0, Oi is an ontology category, it has π(C ⊓ D) −→ π(C), π(C ⊓ D) −→ π(D), π(C) −→ π(C ⊔ D), π(D) −→ π(C ⊔ D).
これらの規則は、Cc に C に C に C を付加する対象 C > D と C > D , C > D > D , C −→ C > D , D −→ C > D に対して適用される。CchC0, Oi はオントロジー圏であるため、π(C > D) −→ π(C) −→ π(D), π(C) −→ π(C > D), π(D) −→ π(C > D), π(D) −→ π(C > D) を持つ。
0.88
Thus, Properties (44)-(45) are preserved.
これにより、特性(44)−(45)が保存される。
0.70
3. [⊥m-rule]. Assume that Cc has an arrow E ⊓ F −→ ⊥ and it does not have an arrow E −→ NNF(¬F ) (or F −→ NNF(¬E)).
3回)。 Cc の矢印 E は、E − → NNF(\F ) (または F − → NNF(\E)) を持たないと仮定する。 訳抜け防止モード: 3回)。 Cc が矢印 E > F −→ > を持つと仮定する。 また、矢印 E −→ NNF(シュフ) ( または F −→ NNF(シュエ)) は持たない。
0.54
By the hypothesis on Property (44) and (45), CchC0, Oi has an arrow π(E ⊓ F ) −→ π(⊥).
In this case, [¬-rule] adds to Cc an arrow NNF(¬D) −→ NNF(¬C).
この場合、[a-rule] は Cc に矢印 NNF(nD) −→ NNF(nC) を付加する。
0.76
Since CchC0, Oi is an ontology category, it has an arrow π(NNF(¬D)) −→ π(NNF(¬C)).
CchC0, Oi はオントロジー圏であるから、矢印 π(NNF(\D)) −→ π(NNF(\C)) を持つ。
0.67
Thus, Properties (44)- (45) are preserved.
こうして、特性(44)−(45)が保存される。
0.69
6. [⊔m-rule]. Assume Cc has an object E ⊔F and two arrows E −→ X and F −→ X and it has no arrow E ⊔ F −→ X. By the hypothesis on Properties (44) and (45), there are arrows π(E) −→ π(X) and π(F ) −→ π(X).
6)であった。 cc が対象 e −→ x と 2 つの矢印 e −→ x と f −→ x を持ち、その矢印 e は性質 (44) と (45) の仮説により、π(e) −→ π(x) と π(f ) −→ π(x) が存在すると仮定する。 訳抜け防止モード: 6)であった。 Cc は対象 E > F と二つの矢 E −→ X と F −→ X を持つと仮定する。 性質仮説(44 )により、矢印 E > F −→ X は存在しない。 そして (45 ) の矢印は π(E ) −→ π(X ) である。 そして π(F ) −→ π(X ) である。
0.63
In this case, [⊔m-rule] adds to Cc.
この場合、['m-rule] は Cc に追加される。
0.74
Since CchC0, Oi is an ontology category, it has arrows E ⊔ F −→ X and π(E ⊔ F ) −→ π(X).
CchC0, Oi はオントロジー圏であるため、矢印 E は F − → X であり、π(E は F ) − → π(X) である。
0.77
7. [⊓m-rule].
7. (複数形 7.s)
0.56
Analogously. 8. [⊔dis-rule].
アナログ。 8. [アディスルル].
0.58
Assume that Cc has objects C ⊓ (D ⊔ E), W .
Cc が対象 C , (D , E) を持つと仮定する。
0.76
It holds that C ⊓ (D ⊔ E) can be rewritten as C ⊓ (D ⊔ E) = (C1 ⊔ D1) ⊓ · · · ⊓ (Cn ⊔ Dn).
It follows that CchC0, Oi has an arrow FXi∈{Ci,Di}(X1 ⊓ · · · ⊓ Xn) −→ π(W ) due to Definition 4, and an arrow π(C ⊓ (D ⊔ E)) −→ π(W ) due to Property 7 in Definition 5.
In this case, [⊔dis-rule] adds to Cc an arrows C ⊓ (D ⊔ E) −→ W .
この場合、[dis-rule] は Cc に矢印 C を付加する。
0.47
Thus, Properties (44) and (45) are preserved.
これにより、特性(44)と(45)が保存される。
0.76
9. [∃-rule].
9. [オ・ルル]。
0.35
Assume that Cc has an object ∃R.D. By the hypothesis on Properties (44) we have π(∃R.D) = ∃R.D. In this case, [∃-rule] adds to Cc a role object R(∃R.D), concept objects dom(R(∃R.D)), cod(R(∃R.D)) with arrows dom(R(∃R.D)) ←−−−−→ ∃R.D. Since CchC0, Oi is an ontology category, it has also R(∃R.D), concept objects dom(R(∃R.D)), cod(R(∃R.D)) with arrows dom(R(∃R.D)) ←−−−−→ ∃R.D. We can extend π with π(dom(R(∃R.D))) = dom(R(∃R.D)), π(dom(R(∃R.D))) = dom(R(∃R.D)), and π(R(∃R.D)) = R(∃R.D).
Assume that Cc has an object ∃R.D and a role object R′ such that R′ −→ R and cod(R′) −→ D. By the hypothesis on Properties (44) and (45) we have π(∃R.D) = ∃R.D, π(cod(R′)) = cod(R′), π(D) = D with π(cod(R′)) −→ π(D) and π(R′) −→ π(R).
R′ − → R と cod(R′) − → D が成り立つ対象 R′ と Cc が成り立つと仮定すると、性質 (44) と (45) 上の仮説により、π( π( π(cod(R′))) = cod(R′), π(D) = D と π(cod(R′)) −→ π(D) と π(R′) −→ π(R) が成り立つ。
0.85
In this case, [∃m-rule] adds to Cc an arrow dom(R′) −→
この場合、['m-rule] は矢印 dom(R′) −→ を Cc に追加する。
0.75
英語（論文から抽出）
日本語訳
スコア
dom(R(∃R.D)).
dom(r) である。
0.58
Since CchC0, Oi is an ontology category, it has π(dom(R′)) −→ π(dom(R(∃R.D))).
CchC0, Oi はオントロジー圏であるため、π(dom(R′)) −→ π(dom(R(\R.D))) を持つ。
0.82
Hence, Properties (44) and (45) are preserved.
したがって、プロパティ(44)と(45)が保存される。
0.78
11. [∀-rule].
11. [オ・ルル].
0.34
Assume that Cc has an object ∀R.C, and it has no arrows ∀R.C ←−−−−→ ¬∃R.
cc が r.c のオブジェクトを持ち、矢印が存在しないと仮定する。 訳抜け防止モード: Cc が対象 >R.C を持つと仮定し、 矢印は存在しない。
0.69
¬C. By the hypothesis on Properties (44) and (45) we have π(∃R.D) = ∃R.D. In this case, [∃m-rule] adds to Cc arrows ∀R.C ←−−−−→ ¬∃R.
(cid:3) The following theorem is a consequence of Lemmas 12 and 13.
(第3話) 次の定理は、Lemmas 12 と 13 の結果である。
0.59
Theorem 3. Satisfiability of an ALC∀ concept with respect to an ontology can be decided in polynomial space.
理論3。 オントロジーに対するアルキシュの概念の満足性は多項式空間において決定できる。
0.67
Example 3. Consider the following ALC∀ ontology :
例3。 以下の ALC オントロジーを考える。
0.53
O = {A ⊑ ∃R.C, A ⊑ ∀R.D, D ⊑ ¬C}.
O = {A > > R.C, A > > R.D, D > > C} である。
0.55
Let us check whether A is satisfiable with respect to O. According to Definition 10, A is not satisfiable with respect to O if there exists CchA, Oi that has an arrow A −→ ⊥.
定義 10 によれば、A が O に関して満足できないのは、もし CchA, Oi が存在して、矢印 A − → ... を持つならである。
0.73
For this, we derive from the definitions the arrows in the following blocks (I)-(V), and add them to CchA, Oi:
(V) dom(R(∃R.C)) −→ dom(R(∃R.¬D)) A −→ dom(R(∃R.¬D))
(v) dom(r(d)) −→ dom(r(r.d)) a −→ dom(r(r.d))
0.38
A −→ ¬dom(R(∃R.¬D))
a −→ イドム(r(r.d))
0.66
A −→ ⊥ Let’s check that CchA, Oi satisfies Definitions 2-7 and Property (36) in Definition 8 and it has an arrow A −→ ⊥.
a −→ である。 CchA, Oi は定義 8 の 2-7 とプロパティ (36) を満足しており、矢印は A − → ... である。
0.68
Indeed, the arrows in Block (I) are added to CchA, Oi by Definition 3; those in Block (II) added by Definition 6; those in Block (III) added by Definition 7; those in Block (IV) added by Definitions 8 and 7; and those in Block (V) added by Definitions 7 and 6.
実際、ブロック (i) の矢印は ccha, oi に定義3で、ブロック (ii) の矢印は定義6で、ブロック (iii) の矢印は定義7で、ブロック (iv) の矢印は定義8と7で、ブロック (v) の矢印は定義7と6で加算される。 訳抜け防止モード: 実際、Block (I ) の矢印は CchA に追加される。 Oi by Definition 3 ; Block (II ) Add by Definition 6 ; Block (III ) Add by Definition 7 ; Block (IV ) Add by Definitions 8 および 7 ; そして、Definitions 7 と 6 で追加された Block ( V ) に含まれるもの。
0.78
The other arrows that do not directly contribute to adding A −→ ⊥ are omitted.
a −→ を付加するに直接寄与しない他の矢印は省略される。
0.76
Now, we apply Algorithm 1 to (A, O) in order to find an arrow A −→ ⊥.
ここでは、(A, O) に対してアルゴリズム 1 を適用して、矢印 A − → ... を求める。
0.71
We omit most of objects and arrows that can be added by Algorithm 1, and we focus on those which lead to adding A −→ ⊥.
¬∃R. ¬D −→ ¬dom(R(∃R.¬D)) A −→ ¬dom(R(∃R.¬D)) (14)
だ。 シュD −→ シュドム(R(英語版)) A −→ シュドム(R(英語版)) (14)
0.48
A −→ ⊥ (15)
(15) で表される。
0.50
The rules never remove any arrow, thus the algorithm will always be able to find (line 9) the arrow A −→ ⊥ if it is added, hence the algorithm return false.
規則はいかなる矢印も削除しないので、アルゴリズムは常に矢印 a −→ s を付加されたときに見つけることができるので、アルゴリズムは偽を返します。
0.73
Since all rules are deterministic, there is no category without A −→ ⊥ that can be constructed.
すべての規則は決定論的であるから、構成可能な a −→ を含まない圏は存在しない。
0.64
Example 4. Consider the following ALC∀ concept C0 = (A ⊔ B) ⊓ (C ⊔ D) ⊓ (E ⊔ F ) and ontology :
例4 以下の alc の概念 c0 = (a と b と (c と d) と (e と f ) とオントロジー : を考える。
Let us check whether C0 is satisfiable with respect to O. As for the previous example, we have from Definition 10 that C0 is not satisfiable with respect to O if there exists CchC0, Oi that has an arrow C0 −→ ⊥.
前回の例では、c0 が o に関して満足できないという定義から、o に関して c0 が満たされないのは、c0 −→ が矢印である oi が存在する場合である。 訳抜け防止モード: C0 が O に関して満足できるかどうかを確かめよう。 定義 10 から C0 が O に関して満足できないのは、もし CchC0 , Oi が存在して、矢印 C0 − → y を持つならである。
0.86
We derive from the definitions the arrows in the following blocks (I)-(V), and add them to CchC0, Oi:
我々は、以下のブロック(I)-(V)の矢印の定義から派生し、それらをCchC0, Oiに追加する。
0.76
英語（論文から抽出）
日本語訳
スコア
(I) A ⊓ C −→ ⊥ B ⊓ D −→ ⊥
(I) A > C −→ > B > D −→ >
0.38
(II) C −→ ¬A D −→ ¬B
(II)C −→ >A D −→ >B
0.37
A ⊓ D −→ ⊥
a - d −→ である。
0.57
B ⊓ C −→ ⊥
b 「c −→」の意。
0.50
D −→ ¬A C −→ ¬B
D −→ c −→ \b である。
0.40
(III) A −→ A ⊔ B C −→ C ⊔ D A ⊓ C ⊓ E −→ C1 A ⊓ C ⊓ F −→ C1 A ⊓ D ⊓ F −→ C1
B −→ A ⊔ B F −→ E ⊔ F B ⊓ C ⊓ E −→ C1 B ⊓ D ⊓ E −→ C1 B ⊓ D ⊓ F −→ C1 C0 −→ C ⊔ D C0 −→ C1 A ⊓ C ⊓ E −→ A ⊓ C B ⊓ C ⊓ E −→ B ⊓ C A ⊓ D ⊓ E −→ A ⊓ D B ⊓ D ⊓ E −→ B ⊓ D A ⊓ C ⊓ F −→ A ⊓ C B ⊓ C ⊓ F −→ B ⊓ C A ⊓ D ⊓ F −→ A ⊓ D B ⊓ D ⊓ F −→ B ⊓ D
b −→ a , b f −→ e , f b , c , e −→ c1 b , d , e −→ c1 b , d , f − → c1 c0 −→ c , d c0 −→ c1 a , d c0 −→ c1 a , d a , d b , d b , d b , d b , d b , f −→ b , d a , d b , c b , c b , c b , c b , c b , c b , c b , c b , c b , c b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b および b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b , b, b など。
0.21
D −→ C ⊔ D E −→ E ⊔ F A ⊓ D ⊓ E −→ C1 B ⊓ C ⊓ F −→ C1 C1 −→ ⊥ C0 −→ E ⊔ F
D −→ C から D E −→ E から F A から D から E −→ C1 B から C から F −→ C1 C1 −→ から C0 −→ E まで。
0.76
(V) A ⊓ C ⊓ E −→ ⊥ B ⊓ D ⊓ E −→ ⊥ A ⊓ D ⊓ F −→ ⊥
(V) A > C > E −→ > B > D > E −→ > A > D > F −→ >
0.35
B ⊓ C ⊓ E −→ ⊥ A ⊓ C ⊓ F −→ ⊥ B ⊓ D ⊓ F −→ ⊥
B > C > E > > A > C > F > > B > D > F > > > B > D > F >
0.30
A ⊓ D ⊓ E −→ ⊥ B ⊓ C ⊓ F −→ ⊥ C0 −→ ⊥
a を d の e −→ のとき、b のとき、c のとき、f −→ のとき、c0 −→ となる。
0.41
The following object is obtained by applying Property (7) of Definition 5:
次のオブジェクトは,定義5のプロパティ(7)を適用して取得する。
0.76
C1 =(A ⊓ C ⊓ E) ⊔ (B ⊓ C ⊓ E) ⊔ (A ⊓ D ⊓ E)
c1 = (a , c , e) , (b , c , e) , (a , d , e)
0.34
⊔ (B ⊓ D ⊓ E) ⊔ (A ⊓ C ⊓ F ) ⊔ (B ⊓ C ⊓ F ) ⊔ (A ⊓ D ⊓ F ) ⊔ (B ⊓ D ⊓ F )
Indeed, the arrows in Block (I) are added to CchC0, Oi by Definition 3; those in Block (II) added by Definition 6; those in Block (III) added by Definition 4; those in Block (IV) added by Definitions 5; and those in Block (V) added by Definitions 2.
実際、ブロック(I)の矢印は定義3によってCchC0、ブロック(II)の矢印は定義6によって追加され、ブロック(III)の矢印は定義4によって追加され、ブロック(IV)の矢印は定義5によって追加され、ブロック(V)の矢印は定義2によって追加される。 訳抜け防止モード: 実際、ブロック(i)の矢印はcchc0に追加される。 oi by definition 3; if in block (ii ) added by definition 6 ; those in block (iii ) added by definition 4 ; those in block (iv ) added by definitions 5 ; そして、ブロック (v) に定義で追加されたもの。
0.80
As before, we apply Algorithm 1 to (C0, O) in order to find an arrow C0 −→ ⊥.
前述したように、アルゴリズム 1 を (c0, o) に適用して矢印 c0 −→ s を見つける。
0.78
英語（論文から抽出）
日本語訳
スコア
Applied rule Pre-requisite
Applied Rule Pre-Requisite
0.37
Arrows (and objects)
Arrows (複数形 Arrows)
0.84
[Initialisation] None. (Line 3 to 5)
[初期化]なし。 (3番から5番)
0.70
Algorithm 2 1st loop
アルゴリズム2 第1ループ
0.80
check(Cc, C0, ⊥) A ⊓ C ⊓ E
check(cc, c0, ]) a , c , e を検査する。
0.72
2nd loop B ⊓ C ⊓ E
第2ループ B は C は E である。
0.68
3rd loop A ⊓ D ⊓ E
第3ループ 略称は「e」。
0.55
4th loop B ⊓ D ⊓ E
第4回ループ B - D - E。
0.51
5th loop A ⊓ C ⊓ F
第5回ループ A は C の F である。
0.61
6th loop B ⊓ C ⊓ F
第6回ループ b 〜 c 〜 f 〜
0.53
7th loop A ⊓ D ⊓ F
第7回ループ f (複数形 fs)
0.59
8th loop B ⊓ D ⊓ F
8番ループ B - D - F。
0.61
added to Cc A ⊓ C −→ ⊥ (1) B ⊓ C −→ ⊥ (2) A ⊓ D −→ ⊥ (3) B ⊓ D −→ ⊥ (4)
Ccに追加される A > C > C > > B > C > > B > C > > A > D > > B > D > > B > D > > > (4)
0.50
C0 = (A ⊔ B) ⊓ (C ⊔ D) ⊓ (E ⊔ F )
c0 = (a と b) と (c と d) と (e と f ) である。
0.72
(1), [⊓-rule] and [trans-rule]
(1)、(2)、(2)、〔～〕、〔～〕
0.33
allow us to find A ⊓ C ⊓ E −→ ⊥
A > C > E −→ >
0.16
(2), [⊓-rule] and [trans-rule]
(2),[\-rule]及び[trans-rule]
0.41
allow us to find B ⊓ C ⊓ E −→ ⊥
B > C > E −→ > を発見できる。
0.65
(3), [⊓-rule] and [trans-rule]
(3)[\-rule]と[trans-rule]
0.40
allow us to find A ⊓ D ⊓ E −→ ⊥
を探せるようにして、a を d と e −→ と書かせておこう。
0.43
(4), [⊓-rule] and [trans-rule]
(4),[\-rule]及び[trans-rule]
0.42
allow us to find B ⊓ D ⊓ E −→ ⊥
では b を d と e −→ と書けるようにしよう。
0.56
(1), [⊓-rule] and [trans-rule]
(1)、(2)、(2)、〔～〕、〔～〕
0.33
allow us to find A ⊓ C ⊓ F −→ ⊥
A > C > F −→ > を発見できる。
0.62
(2), [⊓-rule] and [trans-rule]
(2),[\-rule]及び[trans-rule]
0.41
allow us to find B ⊓ C ⊓ F −→ ⊥
B > C > F −→ > を発見できる。
0.66
(3), [⊓-rule] and [trans-rule]
(3)[\-rule]と[trans-rule]
0.40
allow us to find A ⊓ D ⊓ F −→ ⊥
A > D > F −→ > を発見できる。
0.62
(4), [⊓-rule] and [trans-rule]
(4),[\-rule]及び[trans-rule]
0.42
allow us to find B ⊓ D ⊓ F −→ ⊥
B > D > F −→ > を発見できる。
0.66
End loop [⊔dis-rule]
終ループ 〔dis-rule〕
0.68
For 1 ≤ i ≤ 3, each vector (Xi, Yi, Zi) with Xi ∈ {A, B}, Yi ∈ {C, D}, Zi ∈ {E, D} gives an arrow Xi ⊓ Yi ⊓ Zi −→ ⊥.
1 ≤ i ≤ 3 に対して、Xi ∈ {A, B}, Yi ∈ {C, D}, Zi ∈ {E, D} を持つ各ベクトル (Xi, Yi, Zi) は、矢印 Xi = Yi − → Zi − → Zi を与える。
0.87
There is no arrow C0 −→ ⊥ and check(Cc, C0, ⊥) returns true.
矢印 C0 −→ t はなく、チェック(Cc, C0, t) は真を返す。
0.79
check returns true C0 −→ ⊥
返品確認 本当 c0 −→ である。
0.60
By the same arguments as the previous example, there is no category without C0
前回の例と同様の議論により、C0のない圏は存在しない。
0.59
←−−−−→ ⊥ that can be constructed, hence C0 is unstatisfiable.
←−−−−→ したがって、C0 は立証不能である。
0.37
6 Conclusion We have presented a rewriting of the usual set-theoretical semantics of ALC by using categorial language.
6 結論 分類言語を用いてalcの通常の集合論的意味論の書き直しを行った。
0.71
Thanks to the modular representation of category-theoretical semantics composed of separate constraints, we identify a sublogic of ALC, namely ALC∀, and show that it is strictly from ALC.
For instance, role functionality can be expressed as monic and epic arrows [5].
例えば、ロール機能は、モニック矢印とエピック矢印 [5] として表現できる。
0.74
英語（論文から抽出）
日本語訳
スコア
References 1. F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The Description Logic Handbook: Theory, Implementation and Applications, Second Edition, Cambridge University Press, 2010.
参考文献 1. F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The Description Logic Handbook: Theory, implementation and Applications, Second Edition, Cambridge University Press, 2010 訳抜け防止モード: 参考文献 1 F. Baader, D. Calvanese, D. L. McGuinness D. Nardi, P. F. Patel - Schneider (Eds ) 記述論理ハンドブック : 理論,実装,応用,第2版 ケンブリッジ大学出版局、2010年。
0.76
2. P. Patel-Schneider, P. Hayes, I. Horrocks, Owl web ontology language semantics and abstract
P. Patel-Schneider, P. Hayes, I. Horrocks, Owl web ontology Language semantics and abstract
0.46
syntax, in: W3C Recommendation, 2004.
syntax, in: W3C Recommendation, 2004。
0.47
3. B. Cuenca Grau, I. Horrocks, B. Motik, B. Parsia, P. Patel-Schneider, U. Sattler, Owl 2: The next step for owl, journal of web semantics: Science, services and agents, World Wide Web 6 (2008) 309–322.
3. B. Cuenca Grau, I. Horrocks, B. Motik, B. Parsia, P. Patel-Schneider, U. Sattler, Owl 2: The next step for owl, Journal of web semantics: Science, service and agent, World Wide Web 6 (2008) 309–322。 訳抜け防止モード: 3 B. Cuenca Grau, I. Horrocks, B. Motik B. Parsia, P. Patel - Schneider, U. Sattler, Owl 2 : フクロウの次のステップ Webセマンティクスのジャーナル:科学、サービス、エージェント、World Wide Web 6 (2008 ) 309–322。
0.82
4. W. Lawvere, An elementary theory of the category of sets, in: Proc.
4. w. lawvere, an elementary theory of the category of sets, in: proc.
0.43
Nat. Acad. Sci.
Nat! と。 Sci
0.31
(USA), 1964, p. 1506–1511.
(アメリカ) 1964年、p.1506-1511。
0.54
5. R. Goldblatt, Topoi - The categorial analisys of logic, Mathematics, Dover publications,
5. r. goldblatt, topoi - the categorial analisys of logic, mathematics, dover publications,
0.42
2006. 6. K. Schild, A correspondence theory for terminological logics: preliminary report, in: Proceedings of the 12th international joint conference on Artificial intelligence, 1991, p. 466–471.
2006. 6. K. Schild, A corresponding theory for terminological logics: preliminary report, in: Proceedings of the 12th International joint conference on Artificial Intelligence, 1991, pp. 466–471。 訳抜け防止モード: 2006. 6 . k. schild : 用語論理の対応論 : 予備報告 第12回人工知能国際合同会議の開催にあたって 1991年、p. 466-471。
0.56
7. F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
7. F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge 訳抜け防止モード: 7 F. Baader, I. Horrocks, C. Lutz, U. Sattler 説明論理入門 : ケンブリッジ大学
0.76
University Press, 2017.
2017年、大学出版。
0.73
8. M. Schmidt-Schauß , G. Smolka, Attributive concept descriptions with complements, Artifi-
8. M. Schmidt-Schauß , G. Smolka, Attributive concept descriptions with complements, Artifi-
0.45
cial Intelligence 48 (1) (1991) 1–26.
cial Intelligence 48 (1) (1991) 1–26。
0.45
9. F. Baader, J. Hladik, R. Pe˜naloza, Automata can show PSpace results for description logics, Information and Computation 206 (9) (2008) 1045–1056, special Issue: 1st International Conference on Language and Automata Theory and Applications (LATA 2007).
9. F. Baader, J. Hladik, R. Pe 'naloza, Automata は、説明論理、情報と計算 206 (9) (2008) 1045–1056, Special Issue: 1st International Conference on Language and Automata Theory and Applications (LATA 2007) のPSpace結果を示すことができる。
0.87
10. C. Le Duc, Category-theoretical semantics of the description logic alc, in: M. Homola, V. Ryzhikov, R. A. Schmidt (Eds.), Proceedings of the 34th International Workshop on Description Logics (DL 2021), Vol.
10. C. Le Duc, Category-theoretical semantics of the description logic alc, in: M. Homola, V. Ryzhikov, R. A. Schmidt (Eds.), Proceedings of the 34th International Workshop on Description Logics (DL 2021), Vol. 訳抜け防止モード: 10 . C. Le Duc, Category - 記述論理の理論的意味論 in : M. Homola, V. Ryzhikov, R. A. Schmidt (Eds .) 第34回国際説明論理ワークショップ(DL2021)の開催報告
0.80
2954 of CEUR Workshop Proceedings, CEUR-WS.org, 2021.
ceur workshop proceedings, ceur-ws.org, 2021を参照。
0.50
11. I. Horrocks, U. Sattler, S. Tobies, Practical reasoning for expressive description logics, in: Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 1999), Springer, 1999.
11. I. Horrocks, U. Sattler, S. Tobies, Practical reasoning for expressive description logics in: Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 1999), Springer, 1999 訳抜け防止モード: 11 . I. Horrocks, U. Sattler, S. Tobies, Practical reasoning for expressive description logics プログラミングのための論理に関する国際会議」の開催報告 人工知能と推論(LPAR 1999, Springer, 1999)。
0.83
12. D. I. Spivak, R. E. Kent, Ologs: a categorical framework for knowledge representation, PloS
13. M. Codescu, T. Mossakowski, O. Kutz, A categorical approach to networks of aligned on-
13. M. Codescu, T. Mossakowski, O. Kutz, アライメントオンネットワークの分類的アプローチ-
0.91
tologies, J. Data Semant.
トロジー、J.データセマント。
0.51
6 (4) (2017) 155–197.
6 (4) (2017) 155–197.
0.49
14. S. Mac Lane, I. Moerdijk, Sheaves in Geometry and Logic, Springer, 1992.
14. s. mac lane, i. moerdijk, sheaves in geometry and logic, springer, 1992年。
0.86
15. F. Baader, U. Sattler, Tableau algorithms for description logics, in: Proceedings of the International Conference on Automated Reasoning with Tableaux and Related Methods, Vol.
15. f. baader, u. sattler, tableau algorithms for description logics, in: proceedings of the international conference on automated reasoning with tableaux and related methods, vol. (英語) 訳抜け防止モード: 15 . f. baader, u. sattler, tableau algorithms for description logics, 第2回自動推論国際会議の開催にあたって
0.59
1847, Springer-Verlag, St Andrews, Scotland, UK, 2000, p. 118.
1847, Springer-Verlag, St Andrews, Scotland, UK, 2000, pp. 118。
0.49
16. I. Horrocks, U. Sattler, A tableau decision procedure for SHOIQ, Journal Of Automated
16. I. Horrocks, U. Sattler, A tableau decision procedure for SHOIQ, Journal of Automated