論文の概要、ライセンス

# (参考訳) カテゴリー意味論における記述論理alcの推論 [全文訳有]

Reasoning in the Description Logic ALC under Category Semantics ( http://arxiv.org/abs/2205.04911v1 )

ライセンス: CC BY 4.0
Ludovic Brieulle and Chan Le Duc and Pascal Vaillant(参考訳) 本稿では、分類言語を用いて記述論理$\mathcal{ALC}$の通常の集合論的意味論を一般的なTBoxで再構成する。 この設定では、$\mathcal{ALC}$ の概念はオブジェクトとして、概念は矢印として、メンバシップはオブジェクトとカテゴリの矢印上の論理量化子として表現される。 このようなカテゴリベースの意味論は$\mathcal{ALC}$のセマンティクスをよりモジュール化した表現を提供する。 このフィーチャにより、空間の指数的複雑性の原因となる存在的制約と普遍的制約の間の相互作用をなくすことで、$\mathcal{alc}$のサブ論理を定義することができる。 このような部分論理は通常の集合論的な意味論では定義できないが、多項式空間で実行される概念満足性をチェックする決定論的アルゴリズムを提案することにより、この部分論理は {\sc{PSPACE}} であることを示す。

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.
公開日: Tue, 10 May 2022 14:03:44 GMT

※ 翻訳結果を表に示しています。PDFがオリジナルの論文です。翻訳結果のライセンスはCC BY-SA 4.0です。詳細はトップページをご参照ください。

翻訳結果

    Page: /      
英語(論文から抽出)日本語訳スコア
2 2 0 2 y a M 0 1 2 2 0 2 y a m 0 1 である。 0.53
] O L . s c [ ] 略称はL。 sc [ 0.42
1 v 1 1 9 4 0 1 v 1 1 9 4 0 0.42
. 5 0 2 2 : v i X r a . 5 0 2 2 : v i X r a 0.42
Reasoning in the Description Logic ALC under 記述論理ALCにおける推論 0.64
Category Semantics Ludovic Brieulle, Chan Le Duc, and Pascal Vaillant カテゴリー意味論 Ludovic Brieulle, Chan Le Duc, Pascal Vaillant 0.55
Universit´e Sorbonne Paris Nord, LIMICS, INSERM, U1142, F-93000, Bobigny, France ソルボンヌ・パリ・ノルド大学, LIMICS, INSERM, U1142, F-93000, ボビニー 0.74
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. 抽象。 本稿では,一般的な TBox を用いた記述論理 ALC の集合論的意味論を分類言語を用いて再構築する。 0.59
In this setting, ALC concepts are represented as objects, concept subsumptions as arrows, and memberships as logical quantifiers over objects and arrows of categories. この設定では、ALCの概念はオブジェクトとして、概念は矢印として、メンバシップはオブジェクトとカテゴリの矢印上の論理量化器として表現される。 0.59
Such a category-based semantics provides a more modular representation of the semantics of ALC. このようなカテゴリベースのセマンティクスは、ALCのセマンティクスをよりモジュール化した表現を提供する。 0.54
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. この特徴により、空間の指数複雑性の原因となる存在的制約と普遍的制約の間の相互作用を排除し、ALCのサブ論理を定義することができる。 0.73
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. このような部分論理は通常の集合論的意味論では定義できないが、この部分論理は多項式空間で実行される概念満足性をチェックする決定論的アルゴリズムを提案することによってPSPACEであることを示す。 0.61
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. はじめに OWL [2], OWL2[3]のような記述論理(DL)[1]に基づく言語は、意味論に基づくアプリケーションにおけるオントロジーを表現するために広く使われている。 0.69
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. lawvere [4]による先駆的著作は、集合の圏の適切な公理化を、集合のメンバシップを関数の構成に置き換えた。 0.63
However, it was not indicated whether the categorical axioms are “semantically” equivalent to the axioms based on set membership. しかし、分類公理が集合のメンバーシップに基づく公理と同値であるかどうかは明らかにされなかった。 0.62
As pointed out by Goldblatt [5], this may lead to a very different semantics for negation. Goldblatt [5] が指摘しているように、これは否定のための全く異なる意味論につながる可能性がある。 0.64
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. 本稿では,概念と仮定をそれぞれ表現するために,圏論の2つの基本要素であるオブジェクトと矢印を用いて,alcの通常の集合論的意味論の書き直しを提案する。 0.71
It is well known that ALC with general TBoxes is EXPTIME-complete [6,7] while ALC without TBox is PSPACE-complete [8]. 一般的な TBoxes の ALC が EXPTIME-complete [6,7] であり、TBox の ALC が PSPACE-complete [8] であることはよく知られている。
訳抜け防止モード: 一般的な TBoxes を持つ ALC が EXPTIME - complete [ 6,7 ] TBox のない ALC は PSPACE - complete [ 8 ]
0.82
Hence, the interaction between existential and universal restrictions with general TBoxes would be responsible for an intractable space complexity if PSPACE(EXPTIME. したがって、PSPACE(EXPTIME) が成立すれば、存在制約と一般の TBox との相互作用が引き起こされる。 0.60
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. この研究の主な動機は、表現力の過剰さを損なうことなく推論の複雑さを低減できる一般的なtboxでalcのサブ論理を同定することにある。 0.72
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]. 通常の集合論的意味論の下で ALC を推論する際の空間複雑性を低減するため、TBox の表現性を周期公理を持つことを防止して抑制することができる[9]。 0.69
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. しかし、圏論的意味論の下では alc のサブ論理を見つけることができ、それは一般の tbox を完全に表現することができ、普遍的制約のセマンティクスの一部を取り下げるだけでよい。 0.61
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): 実際、alc の普遍的制限は、以下の2つの非公式な性質を用いて圏論的意味論の下で定義することができる(後述のセクション 4 の定義 8)。 0.73
(i) ∀R.C is “very close” to ¬∃R. (i)「R.C」は「非常に近い」。 0.75
¬C; and (ii) ∃R.C ⊓ ∀R.D is “very close” to ∃R. とCは言う。 (ii)「R」は「R」と「非常に近い」ものである。 0.58
(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. 以下に示すように(第5節)、この相互作用を普遍的制限の圏論的意味論から取り除くだけでよいなら、新しい論理、すなわちalc (alc) を得る。
訳抜け防止モード: 以下に示すように(第5節)、 この相互作用は 普遍的制限のカテゴリー的意味論から 取り除けるかもしれません 我々は新しい論理、すなわち ALC > を得るが、推論は空間において引き出すことができる。
0.76
The semantic loss caused by this removal might be tolerable in certain cases. この削除によって引き起こされる意味的損失は、特定のケースでは許容できる可能性がある。 0.53
We illustrate it with the example below. 私たち 以下の例で示してください。 0.70
Example 1. Consider for instance the following ALC TBox: 例1。 例えば、以下の alc tbox を考える。 0.71
HappyChild ⊑ ∃eatsFood.Dessert ⊓ ∀eatsFood.HotMeal Dessert ⊑ ¬HotMeal ハッピーチャイルド 〜eatsfood.dessert 〜 〜eatsfood.hotmeal desert 〜 〜hotmeal 0.47
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. 実際、最初の公理によれば、誰かがHappyChildなら、同時に(1)デッサートを食べ、(2)HotMealだけを食べなければならない。
訳抜け防止モード: 実際、最初の公理によると、誰かがHappyChildなら。 同時に) 1 ) 食べるデッサートがある。 そして (2 ) は HotMeal のみを食べるが、これは第2公理と矛盾する。
0.71
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. さて、第2の公理がセット理論のセマンティクスの下でTBoxから削除された場合、最初の公理は、誰かがHappyChildであるなら、HotMealを食べる。 0.71
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. 実際、第一のサブコンセプション(eatsfood.dessert)は、彼らが食べる食べ物が少なくとも1つ存在することを保証し、第二のサブコンセプション(eatsfood.dessert)は、必然的にこの食べ物がホットミールであることを保証する。
訳抜け防止モード: 実際、最初のサブコンセプション(sieatsFood . Dessert )は、それを保証します。 食べる食品は少なくとも1つあります そして2つ目は、この食品が必ずしもHotMealである、ということです。
0.77
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. この論文で定義するカテゴリ論的意味論の下では、最初の公理だけでは、誰かがHappyChildであるならHotMealを食べることを許さない。 0.67
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. これは、性質(ii)を表す普遍的量化の定義の要素が欠落し、集合論的意味論とは異なり、2番目の概念に対して拡張的な「支援」を提供する個人がもはや存在しないという事実によるものである。 0.81
The paper is organized as follows. 論文は以下の通り整理される。 0.65
We begin by translating semantic constraints related to each ALC constructor into arrows between objects. まず、各ALCコンストラクタに関する意味制約をオブジェクト間の矢印に変換する。 0.55
Then, we check whether the obtained arrows allow to restore usual properties. そして、得られた矢印が通常のプロパティを復元できるかどうかを確認する。 0.60
If it is not the case, we add new arrows and objects to capture the missing properties without going beyond the set-theoretical semantics. もしそうでなければ、セット理論のセマンティクスを超えることなく、失われたプロパティをキャプチャするために新しい矢印とオブジェクトを追加します。 0.62
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]. 例えば、否定の圏論的意味論を定義するのに十分ではない、なぜなら、この定義 [10] からc−−−−−−−−−− 〜c のような矢印を得ることができないからである。 0.57
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. 第5節では、まず alc の部分論理、すなわち alc を同定し、空間における難解な複雑さをもたらす普遍的制約の圏論的意味論からプロパティを落とします。 0.72
We show that this sublogic is strictly different from ALC and propose a PSPACE deterministic algorithm for checking concept satisfiability in ALC∀. 本稿では,このサブ論理がALCと厳密に異なることを示し,ALCにおける概念満足度をチェックするためのPSPACE決定アルゴリズムを提案する。 0.62
英語(論文から抽出)日本語訳スコア
2 Related Work In this section, we discuss some results on PSPACE algorithms for Description Logics that are slightly more expressive than ALC. 2 関連作業 本稿では, ALC よりも若干表現力が高い記述論理用 PSPACE アルゴリズムについて述べる。 0.73
A PSPACE algorithm [11] was presented for the logic SI (ALC with inverse and transitive roles) without TBox. tbox を使わずに論理 si (alc with inverse and transitive roles) に対して pspace アルゴリズム [11] を提示した。 0.73
Tableau method is used in this algorithm to build a tree to represent a model. Tableauメソッドはモデルを表現するツリーを構築するためにこのアルゴリズムで使用される。 0.85
Since TBox is not allowed, the depth of such trees is bounded by a polynomial function in the size of input. tbox は許容されないため、そのような木の深さは入力の大きさの多項式関数によって制限される。 0.72
When extending this method to a general TBox, the depth of such trees may be exponential. この手法を一般的なTBoxに拡張する場合、そのような木の深さは指数関数的である。 0.58
A more recent work [9] proposed an automata-based algorithm for SI with an acyclic TBox. より最近の研究[9]では、非巡回的TBoxを用いたSIのためのオートマタベースのアルゴリズムを提案した。 0.56
This algorithm tries to build a tree automaton to represent a model. このアルゴリズムはモデルを表現するためにツリーオートマトンを構築しようとする。 0.78
In this construction, the acyclicity of a TBox prevents the algorithm from building a tree automaton with an exponential depth. この構成において、TBoxの非巡回性は、指数的な深さを持つ木オートマトンを構築するアルゴリズムを防ぐ。 0.67
A common issue of these algorithms is that they need to store backtracking points in order to deal with nondeterminism. これらのアルゴリズムの一般的な問題は、非決定性に対処するためにバックトラッキングポイントを格納する必要があることである。
訳抜け防止モード: これらのアルゴリズムの共通の問題は 非決定論に対処するために バックトラッキングポイントを 保存する必要がある
0.75
When the depth is exponential, they have to use an exponential memory to store backtracking points. 深さが指数関数であれば、指数メモリを使用してバックトラッキングポイントを保存する必要がある。
訳抜け防止モード: 深さが指数関数的であれば 指数関数記憶を用いてバックトラッキングポイントを記憶する。
0.71
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. spivakら[12]はカテゴリ理論を用いて、推論の基本的な形式ではなく、知識表現のためのowl(dlsに基づく)に匹敵するハイレベルなグラフィカル言語を定義した。 0.66
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. このようなネットワーク上のすべてのグローバルな推論は、ネットワークに関わるオントロジーで使用される特定のDLに対する局所的な推論に還元できる。 0.79
As a consequence, the semantics of DLs employed in the ontologies continue to rely on set theory. その結果、オントロジーで使われるDLの意味論は集合論に依存し続けている。 0.64
3 Syntax and set-theoretical semantics of ALC 3 ALCの構文と集合論的意味論 0.72
We present syntax and semantics of the Description Logic ALC [1] with TBoxes and some basic inference problems. 本稿では,tbox を用いた記述論理 alc [1] の構文と意味について述べる。
訳抜け防止モード: 記述論理 ALC [1 ] の構文と意味論を TBoxes で示す。 基本的な推論の問題もあります
0.69
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 = h>I , ·Ii は空でない集合 ^I (ドメイン) と、 ^I の部分集合を各概念名に関連づける関数 ·I (解釈関数) と、各個人に ^I の要素と、各ロール名に ^I × ^I の部分集合を関連付ける。 0.68
英語(論文から抽出)日本語訳スコア
= ∆I = ∅ i = i である。 0.46
⊤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. これは、|sub(O)| が kOk によって多項式的に有界である、なぜなら、ある概念が文字列として表されるなら、部分概念は部分弦であるからである。 0.71
4 Category-theoretical semantics of ALC 4 ALCのカテゴリー論的意味論 0.66
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. alc の集合論的意味論は集合メンバーシップ関係に基づいているのに対し、一貫性や概念の仮定のようなオントロジ推論は集合包含物を含んでいる。 0.65
This explains why inference algorithms developed in this setting often have to build sets of individuals connected in some way for representing a model. この設定で開発された推論アルゴリズムが、モデルを表現するために何らかの方法で接続された個人のセットを構築する必要がある理由を説明する。 0.56
In this section, we use some basic notions in category theory to characterize the semantics of ALC. 本稿では、ALCのセマンティクスを特徴付けるために、圏論におけるいくつかの基本的な概念を用いる。
訳抜け防止モード: この節では、圏論においていくつかの基本的な概念を用いる。 ALCのセマンティクスを特徴づける。
0.53
Instead of set membership, in this categorical language, we use “objects” and “arrows” to define semantics of a given object. メンバシップを設定する代わりに、このカテゴリ言語では、与えられたオブジェクトのセマンティクスを定義するために“オブジェクト”と“矢印”を使用します。 0.64
Although the present paper is self-contained, we refer the readers to textbooks [5,14] 本論文は自己完結であるが,読者は教科書[5,14]を参照する。 0.70
on category theory for further information. さらなる情報のためのカテゴリー理論についてです 0.62
Definition 2 (Syntax categories). 定義 2 (シンタックスのカテゴリ)。 0.77
Let R and C be non-empty sets of role names and concept names respectively. r と c をそれぞれ役割名と概念名の空でない集合とする。 0.74
We define a concept syntax category Cc and a role syntax category Cr from the signature hC, Ri as follows: 概念構文カテゴリccと役割構文カテゴリcrを、署名hc,riから次のように定義する。
訳抜け防止モード: 概念構文カテゴリCcと役割構文カテゴリCrを署名hCから定義する。 理は以下のとおりである。
0.79
1. Each role name R in R is an object R of Cr. 1. R の各ロール名 R は Cr の対象 R である。 0.83
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 Cr の各対象 R に対して Cc の dom(R) と cod(R) が成立する。 0.86
(a) dom(R⊤) = ⊤, cod(R⊤) = ⊤, dom(R⊥) = ⊥ and cod(R⊥) = ⊥. (a) dom(r) = (r)、cod(r) = (r)、dom(r) = (r)、cod(r) = (r) は (r) である。 0.56
(b) if there is an arrow R −→ R′ in Cr then there are arrows dom(R) −→ (b) cr に矢印 r −→ r′ がある場合、矢印 dom(r) −→ が存在する。 0.80
dom(R′) and cod(R) −→ cod(R′). dom(R′) と cod(R) −→ cod(R′) である。 0.82
(c) if there are arrows R −→ R′ −→ R′′ in Cr then there are arrows dom(R) −→ (c) Cr に矢 R − → R′ −→ R′′ が存在するなら、矢 dom(R) −→ が存在する。 0.72
dom(R′′) and cod(R) −→ cod(R′′). dom(R′′) と cod(R) −→ cod(R′′) である。 0.74
(d) if there is an arrow dom(R) −→ ⊥ or cod(R) −→ ⊥ in Cc, then there is an (d) Cc に矢印 dom(R) −→ . または cod(R) −→ . があるなら、a が存在する。 0.82
arrow R −→ R⊥ in Cr. Cr の矢印 R − → R 。 0.84
For each arrow E −→ F in Cc or Cr, E and F are respectively called domain and codomain of the arrow. Cc または Cr における各矢印 E − → F に対して、E と F はそれぞれ矢印の領域と余領域と呼ばれる。 0.70
We use also Ob(C ) and Hom(C ) to denote the collections of objects and arrows of a category C . また、圏 C のオブジェクトと矢印の集合を表すために Ob(C ) と Hom(C ) も使用する。 0.71
Definition 3 provides a general framework with syntax elements and necessary properties from category theory. 定義3は、構文要素と圏論から必要な性質を持つ一般的なフレームワークを提供する。 0.61
We need to “instantiate” it to obtain categories which capture semantic constraints coming from axioms. 公理から生じるセマンティック制約をキャプチャするカテゴリを得るには、それを“検証”する必要があります。 0.53
The following definition extends syntax categories in such a way that they admit the axioms of an ALC ontology as arrows. 次の定義は、ALCオントロジーの公理を矢印として認めるように、構文圏を拡張している。 0.58
Definition 3 (Ontology categories). 定義3 (オントロジーのカテゴリ)。 0.74
Let C be an ALC concept and O an ALC ontology from a signature hC, Ri. C を ALC の概念とし、O を符号 hC, Ri から ALC オントロジーとする。 0.79
We define a concept ontology category CchC, Oi and a role ontology category CrhC, Oi as follows: 概念オントロジー圏 CchC, Oi とロールオントロジー圏 CrhC, Oi を次のように定義する。 0.62
1. CchC, Oi and CrhC, Oi are syntax categories from hC, Ri. 1. CchC、Oi、CrhC、OiはhC、Riの構文分類である。 0.76
2. C is an object of CchC, Oi. 2. C は CchC, Oi の対象である。 0.86
3. If E ⊑ F is an axiom of O, then E, F are objects and E −→ F is an arrow of 3. E > F が O の公理であれば、E, F は対象、E −→ F は矢印となる。 0.78
CchC, Oi. In this paper, an object of CchC, Oi and CrhC, Oi is called concept and role object respectively. CchC、Oi。 本稿では,CchC,Oi,CrhCの各対象を概念オブジェクト,役割オブジェクトと呼ぶ。 0.72
We transfer the vocabulary used in Description Logics to categories as follows. 記述論理で使われる語彙を以下のカテゴリに転送する。 0.71
A concept object C ⊔ D, C ⊓ D or ¬C is respevtively called disjunction, conjunction and negation object. 概念対象 C , D , C , D , C は可逆的に共役、否定対象 (disjunction, joint and negation object) と呼ばれる。 0.64
For an existential restriction object ∃R.C or universal restriction object ∀R.C, C is called the filler of ∃R.C and ∀R.C. 存在制限対象 sr.c または普遍制限対象 sr.c に対して、c は sr.c と sr.c のフィラーと呼ばれる。
訳抜け防止モード: 実数制限対象 (R.C) または普遍制限対象 (R.C) に対して C はフィラーと呼ばれる R.C.およびR.C.の略。
0.54
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. この補題では、プロパティ (3) と (4) は集合論におけるプロパティ (1) と (2) の書き換えである。 0.84
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. 集合論的な意味論の下では、結合に関する分断の分配的性質は独立ではない、すなわち、分断と連結の定義の帰結である。 0.75
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 (c)i(c)i(c)i(c)i(c)i )i(c)i(c)i(c)i)i(c)i (c)i(c)i(c)i)i(c)i(c )i)i(c)i(c)i(c)i(c)i )i(c)i(c)i(c)i(c)i)i (c)i(c)i(c)i(c)i(c)i )i(c)i(c)i(c)i)i(c(c )i)i(c)i)
訳抜け防止モード: (c)iはci、cはd)iはxはxである。 d)i(c)i(c)i(d)i(d)i( i) (c、d)、(c、e)i)
0.46
for all concepts C, D and E. すべての概念 C, D, E に対して。 0.79
(14) (15) (16) (14) (15) (16) 0.43
Proof. “⇐=”. 証明。 “⇐=”. 0.43
Due to (14) we have (U ⊓ V )I ⊆ U I ∩ V I. Let X ⊆ ∆I such that X = U I ∩ V I . 14) により、(U ) V ) I ) U I ) V I {\displaystyle VI} が成り立つので、X を X = U I ) V I {\displaystyle X=UI\,VI} とする。 0.56
This implies that X ⊆ U I and X ⊆ V I. From (15), we have X ⊆ (U ⊓ V )I . これは、X は U I であり、X は V I であり、 (15 から X は (U ) V ) I であることを意味する。 0.85
“=⇒”. From (C ⊓ D)I = CI ∩ DI we obtain (14). “=⇒”. は (c , d)i = ci , di から (14) を得る。 0.60
Moreover, if X ⊆ CI and X ⊆ DI then X ⊆ CI ∩ DI = (C ⊓ D)I by the hypothesis. さらに、X > CI かつ X > DI であれば、X > CI > DI = (C > D)I は仮説によって成り立つ。 0.72
Thus, (15) is proved. したがって (15) が証明される。 0.79
To prove (16), we use the hypothesis and the usual set-theoretical semantics as follows: (C ⊓ (D ⊔ E))I = CI ∩ (D ⊔ E)I = CI ∩ (DI ∪ EI) = (CI ∩ DI ) ∪ (CI ∩ EI ) = (C ⊓ D)I ∪ (C ⊓ E)I = ((C ⊓ D) ⊔ (C ⊓ E))I . (16) を証明するために、この仮説と通常の集合論的な意味論を用いる: (C ) (D ) E)I = CI シュ (D ) E)I = CI シュ (DI ) EI) = (CI ) DI ) シュ (CI ) EI ) = (C ) D)I シュ (C ) E)I = ((C ) D) シュ (C ) E)I . {\displaystyle (C )E)I=(C )E)I.} 。 0.73
With disjunction and conjunction, one could use the arrows C ⊓ ¬C −→ ⊥ and ⊤ −→ C ⊔ ¬C to define category-theoretical semantics of negation. 分断と結合により、矢印 c をネグレーションの圏論的意味論を定義するために使うことができる。
訳抜け防止モード: 分断と結合により、矢印 c を使わせることができる。 圏 (category) - 否定の理論的意味論(theory semantics of negation)。
0.62
However, such a definition does not allow to entail useful properties (cf. Lemma 6) which are available under set-theoretical semantics. しかし、そのような定義は集合論的な意味論の下で利用できる有用な性質(Lemma 6)を含まない。 0.72
Therefore, it is required to use more properties to characterize negation in category-theoretical semantics. したがって、カテゴリ理論のセマンティクスにおいて否定を特徴付けるためにより多くの特性を使う必要がある。 0.61
英語(論文から抽出)日本語訳スコア
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). (20) インフォーマルに、Property (19) は「最も大きい」オブジェクトが 17 を満たすオブジェクトである、Property (20) は「最も小さい」オブジェクトが 18 を満たすオブジェクトである、と教えてくれる。
訳抜け防止モード: (20) 非公式に、プロパティ (19 ) は "最大の" を満たすオブジェクト (17 ) である。 property (20 ) は "最小の" を満たすオブジェクト (18 ) であることを示している。
0.56
We now provide the connection between set-theoretical semantics of negation and the categorytheoretical one given in Definition 6. 現在、否定の集合論的意味論と定義6で与えられる圏論的意味論の関連性を提供する。
訳抜け防止モード: ネゲーションの理論的意味論と集合の関係を そして、定義 6 で与えられる圏論的なもの。
0.65
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: 第5回。 定義 6 で特徴づけられる「C」の圏論的意味論は、集合論的意味論 (set-theoretical semantics) の集合論的意味論(set-theoretical semantics)と互換性がある。 0.60
CI ∩ ¬CI ⊆ ⊥I and ⊤I ⊆ CI ∪ ¬CI imply CIは.................... .................... ................. 0.06
∀X, (C ⊓ X)I ⊆ ⊥I =⇒ X I ⊆ (¬C)I ∀X, ⊤I ⊆ (C ⊔ X)I =⇒ (¬C)I ⊆ X I (C)X,(C)X,(C)X,(C)X, (C)X,(C)X,(C)X,(C)X, (C)X)I,(C)X) 0.27
(21) (22) Proof. (21) (22) 証明。 0.49
Let x ∈ X I with (C ⊓X)I ⊆ ⊥I. x ∈ x i を (c,x)i,i とする。 0.75
Due to Lemma 4, we have (C ⊓X)I = CI ∩ X I. Therefore, x /∈ CI , and thus x ∈ (¬C)I . 補題4により、 (c , x)i = ci , x i であり、したがって x ∈ (c)i となる。
訳抜け防止モード: Lemma 4 により、(C は X)I = CI は X I となる。 x/∂ CI であり、したがって x ∈ ( >C)I である。
0.78
Let x ∈ (¬C)I with ⊤I ⊆ (C ⊔ X)I. x ∈ (、C ) I を、X ∈ (、C ) X)I で表す。 0.77
It follows that x /∈ CI. 以下は x の CI である。 0.62
Due to Lemma 1, we have (C ⊔ X)I = CI ∪ X I. Therefore, x ∈ X I. Lemma 1 により、(C > X)I = CI > X I となるので、x ∈ X I となる。 0.78
From Properties (17-20), we obtain De Morgan’s laws and other properties for the プロパティー (17-20) から、De Morgan の法則やその他の性質を入手する。 0.78
category-theoretical semantics as follows. カテゴリー理論的意味論は次のとおりである。 0.41
Lemma 6. The following properties hold. 第6回。 以下の性質がある。 0.65
C ←−−−−→ ¬¬C C −→ ¬D ⇐⇒ D −→ ¬C C ⊓ D −→ ⊥ ⇐⇒ C −→ ¬D (or D −→ ¬C) ¬(C ⊓ D) ←−−−−→ ¬C ⊔ ¬D ¬(C ⊔ D) ←−−−−→ ¬C ⊓ ¬D c-→−−−−−−−−→−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−c−−−d(c−−−d)−−−−−−−−−−−−−−−−−c−−d
訳抜け防止モード: C−−−−−−→ >C−→ >D−→ >D−→ >C−→ >D−→ >D−→ >C−→ >D。 または、D−→(C−−−−−−−→(C)−−−−−→(C)−−−−−→(C)−−−−−→(C)−D
0.40
(23) (24) (25) (23) (24) (25) 0.43
(26) (27) Proof. (26) (27) 証明。 0.49
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. 定義により、 (24) と (23) により、 (24) と (23) により、 シュ(C は D) と シュ(C は D) −→ C は シュ(C は D) −→ C は シュ(C は D) −→ C は シュD となる。 0.59
5. Analogously, we can prove (27) by starting with arrows ¬C ⊓ ¬D −→ ¬C and ¬C ⊓ ¬D −→ ¬D from the definition of conjunction. 5. 同様に、(27) の矢印を、結合の定義から始めれば、(27) を証明できる。
訳抜け防止モード: 5 . 同様に、(27 ) で証明できる。 矢印 (arrows) から始めれば、アロー (arrows) は、結合の定義から始まり、アロー (arrows) は、次のようになる。
0.36
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. 次の補題は、存在制限の集合-理論的意味論と定義 7 で与えられる圏-理論的意味論の間の関係を定めている。
訳抜け防止モード: 以下の補題は集合-存在制約の理論的意味論の間の関係を確立する そして、カテゴリ - 定義7で与えられる理論的カテゴリ。
0.66
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 第7回。 定義 7 で特徴づけられる ^R.C の圏論的意味論は ^R.C の集合論的意味論と互換性がある。 0.59
(∃R.C) ⊆ RI (~R.C) ~ RI 0.67
RI cod(R(∃R.C))I ⊆ CI RIコッド(R(シュR.C))I > CI 0.80
then the following holds: dom(R(∃R.C))I = {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ CI} iff このとき、次のことは成り立つ: dom(R(\R.C))I = {x ∈ >I | >y ∈ >I : hx, yi ∈ RI > y ∈ CI} フ 0.81
∀R′ ⊆ ∆I × ∆I , R′ ⊆ RI, cod(R′) ⊆ CI =⇒ dom(R′) ⊆ dom(R(∃R.C))I cod(r′) は dom(r′) は dom(r(r.c))i で、r′ は dom(r′) である。 0.53
(31) (32) (33) (31) (32) (33) 0.43
Proof. “⇐=”. 証明。 “⇐=”. 0.43
Let x′ ∈ dom(R(∃R.C))I . x′ ∈ dom(R(\R.C))I とする。 0.76
There is an element y ∈ cod(R(∃R.C))I such that hx′, yi ∈ RI (∃R.C) by definition. 定義により hx′, yi ∈ RI (nR.C) となるような元 y ∈ cod(R(\R.C))I が存在する。 0.85
Due to (32), we have y ∈ CI. 32) のため、y ∈ CI が成立する。 0.62
Analogously, due to (31), we have hx′, yi ∈ RI. 類似して、(31) により、hx′, yi ∈ RI が成り立つ。 0.71
Thus, x′ ∈ {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ CI}. したがって、x′ ∈ {x ∈ >I | >y ∈ >I : hx, yi ∈ RI > y ∈ CI} である。 0.81
Let x′ ∈ {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ CI}. x′ ∈ {x ∈ >I | >y ∈ >I : hx, yi ∈ RI > y ∈ CI} とする。 0.87
Thus, there is an element y ∈ CI such that hx′, yi ∈ RI. したがって、hx′, yi ∈ RI となる元 y ∈ CI が存在する。 0.74
Take an R′ ⊆ ∆I × ∆I such that R′ ⊆ RI, cod(R′) ⊆ CI with x′ ∈ dom(R′) and y ∈ cod(R′). x′ ∈ dom(R′) と y ∈ cod(R′) で R′ の RI と cod(R′) と cod(R′) と R′ の y ∈ cod(R′) が成り立つような R′ を R′ × RI とする。
訳抜け防止モード: R′ を RI とし、R′ を RI とする。 cod(R′ ) は x′ ∈ dom(R′ ) と y ∈ cod(R′ ) を持つ。
0.80
Due to (33), we have x′ ∈ dom(R(∃R.C))I . 33) により、x′ ∈ dom(R(\R.C))I となる。 0.75
“=⇒”. Let R′ ⊆ ∆I × ∆I such that R′ ⊆ RI, cod(R′) ⊆ CI . “=⇒”. R' を RI, cod(R′) を CI とし、R′ を yI × yI とする。 0.60
Let x′ ∈ dom(R′). x′ ∈ dom(R′) とする。 0.77
This implies that there is some y ∈ cod(R′) such that hx′, yi ∈ R′. これは、hx′, yi ∈ r′ となる y ∈ cod(r′) が存在することを意味する。 0.80
Hence, y ∈ CI and hx′, yi ∈ RI. したがって、y ∈ CI と hx′, yi ∈ RI が成り立つ。 0.85
Therefore, x′ ∈ {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ CI} = dom(R(∃R.C))I . したがって、x′ ∈ {x ∈ >I | >y ∈ >I : hx, yi ∈ RI > y ∈ CI} = dom(R(>R.C))I となる。 0.81
Lemma 8. The following properties hold: 第8回。 以下の特性がある。 0.65
C −→ ⊥ =⇒ ∃R.C −→ ⊥ C −→ D =⇒ ∃R.C −→ ∃R.D c −→,c −→,c −→,c −→,c -→,c -→,c -→ 0.39
(34) (35) Proof. (34) (35) 証明。 0.49
1. We have cod(R(∃R.C)) −→ C by definition. 1. cod(r(\r.c)) −→ c の定義による。 0.57
By hypothesis C −→ ⊥, we have cod(R(∃R.C)) −→ ⊥ due Definition 2 of cod. 仮説 c −→ s により、cod(r(r.c)) −→ s は cod の定義 2 である。 0.77
Again, due Definition 2 of cod, we have R(∃R.C) −→ R⊥. 再び cod の定義 2 により、r(r.c) −→ r が成り立つ。 0.72
Moreover, we have dom(R(∃R.C)) −→ ⊥ due Definition 2 of dom. さらに、dom(r(\r.c)) −→ かつ dom の定義 2 がある。 0.68
By Definition 7, we obtain ∃R.C −→ ⊥. 定義7により、r.c −→ s が得られる。 0.60
2. To prove (35) we consider two objects R(∃R.C) and R(∃R.D) in Cr. 2. (35) を証明するために、Cr において 2 つの対象 R(nR.C) と R(nR.D) を考える。 0.67
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: 第9回。 定義 8 で特徴づけられる「R.C」の圏論的意味論は「R.C」の集合論的意味論と互換性がある。 0.54
∀R.CI = {x ∈ ∆I | hx, yi ∈ RI =⇒ y ∈ CI} iff R.CI = {x ∈ >I | hx, yi ∈ RI = >y ∈ CI} のフ 0.84
∀R.CI = (¬∃R.¬C)I ∀R′ ⊆ ∆I × ∆I, R′ ⊆ RI, dom(R′) ⊆ ∀R.CI =⇒ R′ × R′ × RI, dom(R′) は、R′ の値である。 0.54
(38) (39) cod(R′)I ⊆ CI (38) (39) cod(R′)I > CI 0.43
Proof. “⇐=”. 証明。 “⇐=”. 0.43
We have {x ∈ ∆I | hx, yi ∈ RI =⇒ y ∈ CI} is the complement of {x ∈ ∆I | ∃y ∈ ∆I : hx, yi ∈ RI ∧ y ∈ ¬CI} = ∃R. 我々は {x ∈ yI | hx, yi ∈ RI = y ∈ CI} を {x ∈ >I | >y ∈ >I : hx, yi ∈ RI > y ∈ >CI} = >R の補集合とする。 0.89
¬CI . Hence, we have ∀R.CI = {x ∈ ∆I | hx, yi ∈ RI =⇒ y ∈ CI} from (38). という。 したがって、 (38) から sr.ci = {x ∈ si | hx, yi ∈ ri = s y ∈ ci} が成り立つ。 0.56
“=⇒”. Let R′ ⊆ RI with dom(R′) ⊆ ∀R.CI . “=⇒”. R′ > RI を dom(R′) > R.CI とする。 0.55
Let y ∈ cod(R′). y ∈ cod(R′) とする。 0.81
There is some x′ ∈ dom(R′) such that hx′, yi ∈ R′I . いくつかの x′ ∈ dom(R′) が存在し、hx′, yi ∈ R′I となる。 0.72
Since R′ ⊆ RI and dom(R′) ⊆ ∀R.CI , we have x ∈ ∀R.CI and hx′, yi ∈ RI. R′ と dom(R′) と dom(R′) とから、x ∈ R.CI と hx′, yi ∈ RI が成り立つ。 0.81
By hypothesis, y ∈ CI. 仮説では y ∈ CI である。 0.74
Lemma 10. The following properties hold. 背番号10。 以下の性質がある。 0.61
∀R.C ⊓ ∃R. ¬C −→ ⊥ C −→ D =⇒ ∀R.C −→ ∀R.D ∃R.D ⊓ ∀R.C −→ ∃R. 略称はR。 シュC −→ シュC −→ D = シュR.C −→ シュR.D シュR.D シュR.C −→ シュR。 0.44
(D ⊓ C) ∃R.C ⊔ ∃R.D ←−−−−→ ∃R. (D は C) はR.C はR.D は−−−−−−−−− は−R である。 0.38
(C ⊔ D) (40) (c:d) (40) 0.37
(41) (42) (43) (41) (42) (43) 0.42
Proof. 1. (40) is a consequence of (36) and (17). 証明。 1. (40) は (36) と (17) の結果である。 0.70
2. Due to (24), C −→ D implies ¬D −→ ¬C. 2. (24) により、C −→ D は >D −→ >C を意味する。 0.66
By (35), we obtain ∃R. 35) までには、R を得る。 0.70
¬D −→ ∃R. ¬C. D -→R。 略称はC。 0.35
Again, due to (24), we have ¬∃R. 繰り返しますが、 (24) のため、r があります。 0.62
¬C −→ ¬∃R. ¬D. 略称はc-→。 だ。 0.46
By definition with (36), it follows ∀R.C −→ ∀R.D. 定義は (36) で、r.c −→ sr.d である。 0.66
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. これは、cod(rx ) −→ cod(rx ) −→ cod(r(r.d)) が cr から cc への函手cod と dom(rx ) −→ r.c により、cod(rx ) −→ cod(rx ) −→ cod(r.d) となることを意味する。
訳抜け防止モード: 対象 RX を Cr において RX − → R(nR.D ) と定義する。 これはcod(RX ) −→ cod(RX ) −→ cod(R(\R.D ) ) が Cr から Cc への関手コッドのためであることを意味する。 定義上、cod(R(RX ) ) −→ D となる。 Arrow (37 ) と dom(RX ) −→ R.C, cod(RX ) −→ C となるので、cod(RX ) −→ C は D となる。 我々は dom(RX ) −→ > R を得る。
0.79
(D ⊓ C). 略称はc(c)。 0.61
英語(論文から抽出)日本語訳スコア
4. The arrow from left to right of (43) is a direct consequence of the the disjunction arrows (1), (2) and the existential property arrow (35). 4.(43)の左から右への矢は、差止矢(1),(2)及び存在財産矢(35)の直接的な結果である。 0.63
To prove the other direction, we make extensive use of the negation and its properties. 反対の方向を証明するために、否定とその性質を広範囲に活用する。 0.63
Let us write U the right part of the arrow and V the left part, we need to prove that the arrow U ⊓ ¬V −→ ⊥ exists. u を矢印の右部分、v を左部分と書くと、矢印 u が存在することを証明する必要がある。
訳抜け防止モード: U を矢の右側に、V を左に書きましょう。 矢印 U > > > V − → > が存在することを証明する必要がある。
0.72
Indeed, if U ⊓ ¬V −→ ⊥ holds, it follows that U −→ ¬¬V by the implication (19) in Definition 6. 実際、u が成立するならば、定義 6 の含意 (19) による u −→ sv が従う。 0.54
Thus, we obtain U −→ V due to Property (23) in Lemma 6. したがって、Lemma 6 における性質 (23) による U − → V が得られる。 0.75
For that, we need to rewrite V . そのため、Vを書き換える必要があります。 0.76
First, apply rule (23), then apply our version of De まずルールを適用(23)し、それからdeのバージョンを適用する。 0.69
Morgan’s rules (27). morgan’s rules (27)を参照。 0.82
Apply (36) to each member of the conjunction, then (23) again: 36)を接続の各メンバーに適用し、次に(23)を再度適用する。 0.73
From there, consider the concept object U ⊓ ¬V defined by そこから、定義する概念対象 U . . . . V を考える。 0.69
∃R.C ⊔ ∃R.D ←−−−−→ ¬(∀R.¬C ⊓ ∀R.¬D) シュ・R・C・D・シュ・R・D・シュ・−---→・シュ(シュ・R・シュ・シュ・R・シュ・D) 0.15
∃R. (C ⊓ D) ⊓ (∀R.¬C ⊓ ∀R.¬D) R。 (C、D、D、D、D、D、D) 0.29
Using the implied associative nature of ⊓, and Property (42) proved above, we can write 上記で証明した s と property (42) の暗黙の連想的性質を用いて 0.69
∃R. (C ⊔ D)⊓(∀R.¬C ⊓ ∀R.¬D) R。 (C、D、D、D、D、D、D) 0.29
−→ ∃R. (cid:16)(cid:0)(C ⊔ D) ⊓ ¬C(cid:1) ⊓ ¬D(cid:17) -→R。 (cid:16)(cid:0)(cid: 0)(c)(c)(d) は、c(cid:1) は、cid(cid:17)である。 0.40
The distributive property (7) of ⊓ and ⊔, the disjunction property (2), and Definition 2 of ⊥, allow us to make the following reduction 帰納的性質 (7) は s と s の分配的性質 (7) であり、断続的性質 (2) と s の定義 2 は、次の還元を可能にする。 0.65
(C ⊔ D) ⊓ ¬C −→ (C ⊓ ¬C) ⊔ (D ⊓ ¬C) (C→D)→→(C→D→C) 0.24
−→ ⊥ ⊔ (D ⊓ ¬C) −→ D ⊓ ¬C d → c) −→ d (c) − → d (c) −c である。 0.50
Thus, thanks to the commutative nature of ⊓ and (5) again, we have (D⊓¬C ⊓¬D) −→ (⊥ ⊓ C) −→ ⊥. したがって、再び s と (5) の可換な性質のおかげで、 (d, c) −→ (d, c) −→ ) が成立する。 0.73
Applying Properties (34) and (35) of Lemma 8 to the previous existential arrow, we obtain Lemma 8の特性(34)と(35)を既存の矢印に当てはめれば、我々は得られる。
訳抜け防止モード: Lemma 8 のプロパティ (34 ) と (35 ) を以前の存在矢印に適用する。 私たちは
0.82
which concludes the proof. ∃R. 証明を結論づけます R。 0.45
(C ⊔ D) ⊓ (∀R.¬C ⊓ ∀R.¬D) −→ ⊥ (c・d・d・d・d・d・d・d・d・d)-→ 。 0.35
Note that both CchC, Oi and CrhC, Oi may consist of more objects. なお、CchC, Oi と CrhC のどちらも、Oi はより多くの天体から構成されている可能性がある。 0.47
However, new arrows should be derived from those existing or by using the properties given in Definitions (2-8). しかし、新しい矢印は、定義 (2-8) で与えられた特性を用いて、存在するものから派生すべきである。 0.63
Adding to CchC, Oi a new arrow that is independent from those existing leads to a semantic change of the ontology. CchCに追加された新しい矢印は、既存の矢印とは独立しており、オントロジーのセマンティックな変更につながる。 0.67
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). Lemma 6, 8, 10 のすべての性質は、これらの定義で与えられた性質の結果であるので、派生した矢(すなわち独立でない矢印)を得るのに使うことができる。 0.66
Theorem 1 (Arrow and subsumption). 定理1 (arrow and subsumption)。 0.53
Let C0 be an ALC concept and O an ALC ontology. C0 を ALC の概念とし、O を ALC オントロジーとする。 0.76
Let CchC0, Oi be an ontology category. CchC0, Oi をオントロジー圏とする。 0.62
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). オントロジー圏cchc0, oiはシグネチャから任意に構築されたオブジェクトから成り得るので、定義9は、定義に与えられた矢印を適用することで新しい矢印を発見できるより大きなオントロジー圏を構築する可能性を提供する(4-8)。 0.64
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): 完了ツリーを構築するため、tableauアルゴリズムは木t0を初期化し、各衝突のない木tに以下の完了ルールを適用する(つまり、ノードが衝突を含まない)。 0.72
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) = 4] [n-rule] (x) がブロックされないとき、x は L(hx, x′i) = の辺 hx, x′i を持たない。 0.88
{R} and C ∈ L(x′) then it creates a successor x′ of x, and set L(x′) ← {C}, L(hx, x′i ← {R}; ここで {r} と c ∈ l(x′) は x の後継 x′ を生成し、l(x′) なる {c}, l(hx, x′i ) {r} を定める。 0.82
英語(論文から抽出)日本語訳スコア
5. [∀-rule] if ∀R.C ∈ L(x) and x has a successor x′ with L(hx, x′i = {R} then 5. ['-rule] (x) と x が L(hx, x′i = {R} を持つ後続 x′ を持つならば) 0.83
L(x′) ← L(x′) ∪ {C}. L(x′) > L(x′) > {C} である。 0.81
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. この結果はノードにコンプリートルールを適用する順序には依存しないので、この証明では、次の順序 [-rule], [-rule], [-rule], [-rule], [-rule], [-rule] が使われることを仮定し、適用すれば最も祖先のノードにコンプリートルールを適用するべきである。 0.79
Some properties are drawn from this assumption. この仮定からいくつかの性質が導かれる。 0.62
(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. この伝播は、完了木のノードから不連続なノードである祖先への2つの重要な通過、および完了木の切断ノードから、t の親完了ツリーの切断ノードへの遷移という2つの重要な種類の通過を通さなければならない。 0.44
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). さらに、r.d1 ∈ l(z′) と [-rule] が z′ に適用されるなら、d1 ∈ l(yi) である。 0.72
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. 本節では,定義8のプロパティ (37) を除いて,定義 (4-8) で導入されたすべての特性を持つ ALC から得られる ALC の新たなサブ論理,すなわち ALC を同定する。 0.88
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. プロパティ(37)は定義7とプロパティ(36)とは独立ではないので、このサブ論理は通常の集合論的意味論では定義できない。 0.75
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. まず、プロパティの独立性(37)、すなわち、定義で導入された他のプロパティ(4-7)と定義8でプロパティ(36)から導かれるものではないことを示す必要がある。 0.73
For this purpose, we present in Example 2 a category which verifies all properties from Definition 7, and Property (36), but not Property (37). この目的のために、例2において、定義7とプロパティ(36)から全てのプロパティを検証するカテゴリを提示するが、プロパティ(37)ではない。 0.71
Example 2. Every ontology category Cch∀R.D, ∅i that has an object ∀R.D has to consist at least of the following arrows : ∀R.D ←−−−−→ ¬∃R. 例2。 対象 R.D を持つ任意のオントロジー圏 Cch.R.D は、以下の矢印の少なくとも1つを構成する必要がある。 0.69
¬D, ∃R. ¬D ←−−−−→ dom(R(∃R.¬D)) 略称は「D」。 yD-−−−−− − dom(R(nR.nD)) 0.36
英語(論文から抽出)日本語訳スコア
where R and R(∃R.¬D) are objects of Crh∀R.D, ∅i. R と R は Crh'R.D の対象である。 0.69
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. R′ を R′ − → R と dom(R′) −→ > R.D の任意の対象とする。 定義 8 において排他的定義 2-7 とプロパティ (36) を適用すれば、定義 8 においてプロパティ (37) によって導かれるはずの Cch.R.D には加わらない。 0.82
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. Lemma 6 および Definition 8 から得られる以下の特性を用いて、多項式的に概念オブジェクトを NNF に変換することができる。 0.89
¬(C ⊔ D) ←−−−−→ ¬C ⊓ ¬D ¬(C ⊓ D) ←−−−−→ ¬C ⊔ ¬D ¬∀R.C ←−−−−→ ∃R. C-−−−−−−(C)−−−−−(C)−−−−−(C)−−−−(C)−−−−(C)−−(C)−−−(C)−(C)−(C)−(C)−(C)−(C)−(C)−(C)−(C)−(C)−(C)−(C)−(C)。 0.16
¬C ¬∃R.C ←−−−−→ ∀R. 略称はc.c.c.。 0.28
¬C ¬¬C ←−−−−→ C ¬⊤ ←−−−−→ ⊥ ¬⊥ ←−−−−→ ⊤ c------------------- -------------------- ---------c 0.05
Definition 11 (subconcepts). 定義 11 (サブコンセプト)。 0.81
Let C0 be an ALC concept and O an ALC ∀ ontology. C0 を ALC の概念とし、O を ALC > オントロジーとする。 0.74
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. 証明。 2つのオブジェクトの間には少なくとも2つの矢印があるため、ccとcrに追加された異なるオブジェクトの数を決定するのに十分である。 0.62
For this purpose, we analyse the behavior of each rule in Table 1 and determine the number of objects added by each such a rule. この目的のために、テーブル1における各ルールの振る舞いを分析し、各ルールが付加するオブジェクトの数を決定する。 0.81
Let n =(cid:13)(cid:13)hC0, Oi(cid:13)(cid:13) be the size of input, i.e. the number of bytes. n = (cid:13)(cid:13)hC0, Oi(cid:13)(cid:13) を入力のサイズ、すなわちバイト数とする。 0.84
By Definition 11, we write subhC0, Oi, the set of sub-concepts. 定義では11。 subhc0, oi, the set of sub-concepts と書く。 0.74
For Definition 11.1 to 3, they are sub- 定義 11.1 から 3 は、サブです。 0.81
英語(論文から抽出)日本語訳スコア
strings of hC, Oi, not all of sub-strings belongs to it, so we have at most ℓ ≤ n(n+ 1)/2 objects created from those first three properties. hc, oi, すべての部分文字列がそれに属するわけではないので、これらの最初の3つの性質から生成される最大 l ≤ n(n+ 1)/2 のオブジェクトが存在する。 0.70
From Definition 11.4, we simply double 定義 11.4 から単純に 2 倍にします 0.58
the number of those - note that NNF(¬¬C) is C - so in total(cid:13)(cid:13 )subhC0, Oi(cid:13)(cid:13) = 2ℓ = これらの数 - NNF(\C) が C であるので、合計 (cid:13)(cid:13)subh C0, Oi(cid:13)(cid:13) = 2l = 0.83
k ≤ O(n2). k ≤ o(n2) である。 0.69
It should be noted that every time we add a object to Cc, we also add its negation, we won’t mention it every time an object is added but it is done. ccにオブジェクトを追加する度に、そのネゲーションを追加する度に、オブジェクトが追加される度に、そのオブジェクトについて言及することはしませんが、完了します。 0.69
Hence why we reason on k instead of ℓ even when we index added objects on a object C of subhC0, Oi. したがって、subhC0, Oi の対象 C にオブジェクトをインデックス付けしても、なぜ k を l ではなく k に理由付けるのか。 0.72
1. [Initialisation](line 3-5). 1. [初期化](ライン3-5) 0.41
It is the first loop of the algorithm and corresponds to Definition 11.1, in the sense the only added objects by the algorithm at this stage これはアルゴリズムの最初のループであり、この段階でアルゴリズムによって追加された唯一のオブジェクトという意味で、定義 11.1 に対応する。
訳抜け防止モード: これはアルゴリズムの最初のループであり、定義 11.1 に対応する。 この段階では アルゴリズムによって 追加された唯一のオブジェクトは
0.85
are already part of subhC0, Oi, i.e. it cannot add more object than(cid:13)(cid:13) subhC0, Oi(cid:13)(cid:13) = つまり、(cid:13)(cid:13)subh C0, Oi(cid:13)(cid:13) = 以上のオブジェクトを追加することはできない。 0.80
k ≤ O(n2) to Cc. k ≤ O(n2) から Cc へ。 0.87
2. [⊓-rule], [⊔-rule]. 2. [-rule] [-rule], [-rule] 0.43
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. しかし、それらは、subhc0、oi、すなわち2kで割られたオブジェクトの数で表される sr.d という形のオブジェクトの出現ごとに1回だけ追加される。 0.68
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. Rのみ。 しかし、d は定義11の一部ではないが、k より小さい形の sr.d のオブジェクトの数によって線形に有界であるため、この規則は最大で 2k ≤ o(n2) 個のオブジェクトを cc に加算する。 0.74
5. [⊥-rule], [⊤-rule]. 5. [--rule], [--rule]. 0.32
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. 集合を扱うので、新しいオブジェクトを追加していません。 0.72
7. [trans-rule], [⊔m-rule], [⊓m-rule], [⊔dis-rule], [⊥m-rule], [⊤m-rule], 7. [トランスルール], [ジムルール], [ジムルール], [ジズルール], [ジムルール], [ジムルール], [ジムルール] 0.67
[∃m-rule], [dc-rule]. 【m-rule】〔dc-rule〕 0.39
These rules only deal with arrows and no objects are addedwe can ignore them. これらのルールは矢印のみを扱い、オブジェクトを追加せずに無視できる。 0.71
8. Algorithm 2 (check). 8. アルゴリズム2(チェック)。 0.68
This algorithm can be implemented such that it runs in polynomial space. このアルゴリズムは多項式空間で動作するように実装することができる。 0.73
For example, we can consider each vector (X1, · · · , Xn) as a binary number (b(X1), · · · , b(Xn)) where b(Xi) = 1 iff Xi = Ai. 例えば、各ベクトル (X1, · · · · · , Xn) を二進数 (b(X1, · · · , b(Xn)) とみなすことができ、ここで b(Xi) = 1 iff Xi = Ai となる。 0.91
In this case, the loop from Line 2 can take binary numbers from 0 to 2n − 1, from which it can determine the vector (X1, · · · , Xn). この場合、ライン 2 からのループは 0 から 2n − 1 への二進数を取ることができ、そこからベクトル (X1, · · · · , Xn) を決定することができる。 0.79
英語(論文から抽出)日本語訳スコア
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. この場合、[n-rule] と [n-rule] の非適用性は、Cc に矢印 NNF(n-rule) を NNF(n-rule) とすることを保証している。 0.64
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). dis-rule] の非適用性のため、cc は矢印 c , (d , e) −→ (c , d) , (c , e) を持つ。 0.68
Hence, Property (7) in Definition 5 holds. したがって、定義 5 のプロパティ (7) は成立する。 0.79
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. 我々は、Ccが定義8における定義2-7のすべてのプロパティとプロパティ(36)を満足していることを示しました。 0.69
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). アルゴリズム 1. によって構築された概念と役割オントロジーのカテゴリを表すのに hcc, cri を使い、関数 π を ob(cc) , ob(cr) から ob(cchc0, oi) に定義する。 0.64
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- (44) (45) プロパティ (44) と (45) が各 applica のために保存されるように π を拡張する。 0.55
tion of rules. Assume that these properties hold for the current π. ルールの義務。 これらの性質が現在の π に対して成り立つと仮定する。 0.61
1. [⊥-rule]. Assume that Cc has arrows X −→ NNF(¬C), X −→ C, but it does not have an arrow X −→ ⊥. 1.[オ・ルル]。 Cc が矢印 X − → NNF(aC)、X − → C を持つと仮定するが、矢印 X − → C は持たない。 0.69
By the hypothesis on Properties (44) and (45), we have π(X) = X, π(C) = C, π(NNF(¬C)) = NNF(¬C), π(X) −→ π(NNF(¬C)), π(X) −→ π(C). 性質 (44) と (45) の仮説により、π(X) = X, π(C) = C, π(NNF(\C)) = NNF(\C), π(X) −→ π(NNF(\C)), π(X) −→ π(C) が得られる。 0.76
In this case, [⊥-rule] adds to Cc objects C ⊓ NNF(¬C), and arrows X −→ ⊥ and . この場合、[\-rule] は cc オブジェクト c に nnf(\c) を付加し、矢印 x −→ s と s を付加する。
訳抜け防止モード: この場合、[ >-rule ] は Cc オブジェクト C > NNF(\C ) に追加する。 そして矢印は X −→ . . . .
0.77
Since and CchC0, Oi is an ontology category, it has π(C ⊓ NNF(¬C)) and π(X) −→ π(⊥). cchc0 および oi はオントロジー圏であるため、π(c ) nnf(\c) と π(x) −→ π(x) を持つ。
訳抜け防止モード: CchC0 と Oi はオントロジー圏であるため、π(C ) NNF(\C ) を持つ。 そして π(X ) −→ π(n ) である。
0.77
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 ) −→ π(⊥). 性質に関する仮説 (44) と (45) により、CchC0 により、Oi は矢印 π(E ) F ) −→ π( ) を持つ。 0.82
In this case, [⊥m-rule] adds to Cc an arrow E −→ NNF(¬F ) (or F −→ NNF(¬E)), and CchC0, Oi has an arrow π(E) −→ π(NNF(¬F )) (or π(F ) −→ π(NNF(¬E)). この場合、['m-rule] は Cc に矢印 E − → NNF(\F ) (または F −→ NNF(\E)) を追加し、CchC0, Oi は矢印 π(E) −→ π(\F(\F ))) (または π(F ) −→ π(\F(\F(\E)))) を持つ。 0.69
This implies that Property (44)-(45) are preserved. これは、プロパティ (44)-(45) が保存されていることを意味する。 0.65
4. [⊤-rule] and [⊤m-rule] Analogously. 4. [--rule] と [--rule] は類似している。 0.73
5. [¬-rule]. Assume Cc has an arrow C −→ D and it has no arrow NNF(¬D) −→ 5.[オ・ルル]。 Cc の矢印は C −→ D であり、矢印 NNF(\D) −→ を持たないと仮定する。 0.61
NNF(¬C). By the hypothesis on Properties (45) and (45), there is an arrow π(C) −→ π(D). NNF(英語版) 性質に関する仮説 (45) と (45) により、矢印 π(C) − → π(D) が存在する。 0.65
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). これは、C > (D > E) は C > (D > E) = (C1 > D1) · · · · (Cn > Dn) と書き換えることができるという。 0.68
For instance, if C is not a conjunction, then D, E and C take respectively C1, D1, and (C2 ⊔ D2) ⊓ · · · ⊓ (Cn ⊔ Dn). 例えば、C が連結でないならば、D と E はそれぞれ C1, D1 と (C2 ) D2) と (C2 ) D2) · · · · (Cn ) を取る。 0.86
Assume that check(Cc, C ⊓ (D ⊔ E), W ) returns “true”. check(Cc, C , (D , E) を仮定すると、W ) は "true" を返す。 0.88
This implies that for each vector (X1, · · · , Xn) with Xi ∈ {Ci, Di}, Cc has an arrow Xi1 ⊓ · · · ⊓ Xij −→ W . これは、Xi ∈ {Ci, Di} を持つ各ベクトル (X1, · · · · · , Xn) に対して、Cc は矢印 Xi1 · · · · Xij − → W を持つことを意味する。 0.82
By the hypothesis on Properties (44), CchC0, Oi has arrows π(Xi1 ⊓ · · · ⊓ Xij ) −→ π(W ), and thus X1 ⊓ · · · ⊓ Xn −→ π(W ). 性質 (44), CchC0 の仮説によれば、Oi は π(Xi1 ^ · · · · Xij ) −→ π(W ) であり、したがって X1 ^ · · · · Xn −→ π(W ) である。 0.82
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. cchc0, oi は、定義 4 による矢印 fxi gui{ci,di}(x1 · · · · xn) −→ π(w ) と、定義 5 における性質 7 による矢印 π(c , (d , e)) −→ π(w ) を持つ。
訳抜け防止モード: すると、CchC0, Oi は定義 4 による矢印 FXi∂{Ci, Di}(X1 > · · · ⋅ Xn ) −→ π(W ) を持つ。 そして、定義 5 のプロパティ 7 による矢印 π(C ) ( D ) E ) ) − → π(W ) である。
0.85
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). Cc が性質 (44) 上の仮説により π(シュR.D) を持つと仮定すると、 π(シュR.D) は Cc にロール対象 R(シュR.D) を付加するが、この場合、(シュルル) の概念対象 dom(R(シュR.D))、cod(R(シュR.D)) に矢印 dom(R(シュR.D)) を付加すると仮定すると、CchC0 から Oi はオントロジー圏であり、概念対象 dom(R(シュR.D)) 、cod(R.D) は矢印 dom(R.R.D)) で拡張できる。
訳抜け防止モード: Cc が対象 R.D. を持つと仮定する。 性質に関する仮説 (44 ) により、π(\R.D.) = πR.D. となる。 [ s-rule ] は Cc にロールオブジェクト R(\R.D ) を追加します。 概念オブジェクト dom(R(、R.D ) ) cod(、R(、R.D ) ) with arrows dom(R(、R.D ) ) 、−−−−−−−→ 、R.D. CchC0 であるため、Oi はオントロジー圏である。 また、R(nR.D )、概念対象 dom(R(nR.D ) )、cod(R(nR.D ) ) と矢印 dom(R(R(nR.D ) ) シュ−−−−−− − シュR.D を持つ。 π を π(dom(R(\R.D ) ) ) = dom(R(\R.D ) ) で拡張することができる。 π(dom(R(\R.D ) ) = dom(R(\R.D ) ) と π(R(\R.D ) ) = R(\R.D ) である。
0.72
Thus, Properties (44) and (45) are preserved. これにより、特性(44)と(45)が保存される。 0.76
10. [∃m-rule]. 10. [イム・ルール]。 0.84
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. 略称はC。 性質に関する仮説 (44) と (45) により、 π(\R.D) = >R.D が成り立つ。
訳抜け防止モード: 略称はC。 性質に関する仮説 (44 ) と (45 ) により、π(\R.D ) = πR.D. となる。 Cc の矢印に C-R.C--−−−−−− を加算する。
0.59
¬C. Since CchC0, Oi is an ontology category, it has and π(∀R.C) ←−−−−→ π(¬∃R.¬C). 略称はC。 CchC0, Oi はオントロジー圏であるから、π(nR.C) と π(nR.C) を持つ。 0.56
Hence, Properties (44) and (45) are preserved. したがって、プロパティ(44)と(45)が保存される。 0.78
12. [trans-rule], [dc-rule]. 12. [trans-rule], [dc-rule] 0.45
Analogously. According to Lemma 12, Algorithm 1 terminates. アナログ。 Lemma 12によると、アルゴリズム1は終了する。 0.62
Due to Properties (44) and (45), π is an injection. 性質 (44) と (45) により、π は注入である。 0.69
By hypothesis, Hom(CchC0, Oi) contains an arrow π(C0) −→ π(⊥). 仮説により、Hom(CchC0, Oi) は矢印 π(C0) −→ π( ) を含む。 0.76
By definition, the presence of π(C0) −→ π(⊥) must be due to the properties in Definitions 2-7 and Property (36) in Definition 8. 定義により、π(C0) −→ π(a) の存在は定義 2-7 における性質と定義 8 における性質 (36) に起因する。 0.86
By Properties (44) and (45) on the function π, Hom(Cc) contains an arrow C0 −→ ⊥, and thus Algorithm 1 return “false”. 函数 π 上の性質 (44) と (45) により、Hom(Cc) は矢印 C0 −→ > を含むので、アルゴリズム 1 は「偽」を返す。 0.85
This completes the proof. これが証明を完了します。 0.61
(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: このために、以下のブロック (i)-(v) 内の矢印の定義から派生し、ccha, oi: に追加する。 0.58
(I) A −→ ∃R.C (I) A −→ >R.C 0.36
D −→ ¬C d −→-c である。 0.46
(II) C ⊓ ¬C −→ ⊥ (II) C > > > > > > 0.35
C −→ ¬D c −→d である。 0.48
A −→ ∀R.D D ⊓ C −→ ⊥ A −→ >R.D 略称はc-→。 0.32
(III) ∃R.C ←−−−−→ dom(R(∃R.C)) (IV) ∀R.D ←−−−−→ ¬dom(R(∃R.¬D)) (iii)シュル・ドム(r(r.c)) (iv) シュル・ドム(d) シュ=−−−−−→ シュドム(r(r.d)) 0.40
cod(R(∃R.¬D)) −→ ¬D cod(R(+R.+D)) −→ ~D 0.30
cod(R(∃R.C)) −→ C ∃R. cod(r(r.c)) −→ c である。 0.64
¬D ←−−−−→ dom(R(∃R.¬D)) yD-−−−−− − dom(R(nR.nD)) 0.32
(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 −→ ⊥. アルゴリズム1で追加できるオブジェクトや矢印のほとんどを省略し、A −→ > を付加するオブジェクトに焦点をあてる。
訳抜け防止モード: アルゴリズム1で追加可能なオブジェクトや矢印のほとんどを省略します。 そして、a −→ ] を加えることに繋がるものに焦点を当てる。
0.75
英語(論文から抽出)日本語訳スコア
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
[¬-rule] 〔...-rule〕 0.65
[∃-rule] 〔...-rule〕 0.67
[∀-rule] 〔...-rule〕 0.55
[∃-rule] 〔...-rule〕 0.67
Arrow (3) is in Cc, but no arrow C −→ ¬D. Arrow (3) は Cc に属するが、矢印 C −→ >D は存在しない。 0.74
∃R.C in Cc, but no object R(∃R.C) in Cr. Cc では R.C となるが、Cr では R(nR.C) は存在しない。 0.61
∀R.D in Cc, but no arrow ∀R.D ←−−−−→ ¬∃R. しかし、Cc では、矢印 は R.D で、-−−−−−−−−−− は存在しない。 0.47
¬D. ∃R. ¬D in Cc, but no object R(∃R.¬D) in Cr. だ。 R。 しかし、Cc では shD となるが、Cr では R は存在しない。 0.44
[trans-rule] We have arrows (4) and (6). [経過規則] 矢印(4) と (6) がある。 0.64
[∃m-rule] [trans-rule] 【イムルール】 [トランスルール] 0.73
We have arrow (11) and arrow R(∃R.C) −→ R, but no arrow dom(R(∃R.C)) −→ dom(R(∃R.¬D)). 矢印 (11) と矢印 R(nR.C) −→ R があるが、矢印 dom(R(nR.C)) −→ dom(R(nR.nD)) は存在しない。 0.74
From arrow (1) to (5) and (1) to (12) successively. 矢 (1) から (5) へ、(1) から (12) へ続く。 0.65
From arrow (2) to (7). arrow (2) から (7) まで。 0.74
On arrow (9). [trans-rule] +[¬-rule] +[trans-rule] From arrow (2) to last arrow. 矢印(9)。 [trans-rule] +[\-rule] +[trans-rule] 矢印(2) から最後の矢印。 0.53
[⊥-rule] We have arrow (13) and (14), but no arrow A −→ ⊥. [-ルル]矢(13)と矢(14)があるが、矢(-→)は持たない。 0.56
added to Cc A −→ ∃R.C (1) A −→ ∀R.D (2) D −→ ¬C (3) C −→ ¬D (4) Ccに追加される a −→-r.c (1) a −→-r.d (2) d −→-c (3) c −→-d (4) 0.55
dom(R(∃R.C)) ←−−−−→ ∃R.C (5) dom(R(英語版)-(R.C))-(R.C)-(R.C) (5) 0.57
cod(R(∃R.C)) −→ C (6) ∀R.D ←−−−−→ ¬∃R. cod(R(nR.C)) −→ C (6) >R.D >−−−−−→ >R。 0.57
¬D (7) ∃R. ¬D (8) 第7回)。 R。 第8回)。 0.46
dom(R(∃R.¬D)) ←−−−−→ ∃R. dom(R)-(R)-(R)-(R)-) -(R)-(R)-(R)-(R)-(R) )。 0.42
¬D (9) cod(R(∃R.¬D)) −→ ¬D (10) cod(R(∃R.C)) −→ ¬D (11) 第9回)。 コード(R(n)) −→ シュD (10) コード(R(R.C)) −→ シュD (11) 0.63
dom(R(∃R.C)) −→ dom(R(∃R.¬D)) (12) dom(R(、R.C)) −→ dom(R(、R.、D)) (12) 0.39
A −→ dom(R(∃R.¬D)) (13) a −→ dom(r(d)) (13) 0.40
A −→ ¬∃R. ¬D A→→R。 うーん。 0.49
¬∃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 ) とオントロジー : を考える。 0.66
O = {A ⊓ C ⊑ ⊥, A ⊓ D ⊑ ⊥, B ⊓ C ⊑ ⊥, B ⊓ D ⊑ ⊥} o = {a ] c ] 〔a 〕 〔a 〕 〔a〕 〔a〕 〔a〕 〔a〕 〔a〕 〔b〕 〔b〕 〔b〕 〔b〕 〕 〔b〕 〔b〕 〔b〕 〔b〕 〔b〕 〔b〕 〔d〕 〕 〕. 0.27
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 (iii)a〜→a〜b〜c〜c〜d〜d〜c〜c〜c〜c〜c〜c〜c〜c〜c〜c〜c〜f〜→c1〜d〜f〜→c1〜 0.25
(IV) C0 −→ A ⊔ B (IV)C0 −→A > B 0.45
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 ) a) (a) (a) (a) (b) (b) (b) (b) (b) (b) (b) (b) (b) (b) (b) (b) (b)) (b) (b) (b)) (b) (b) (b)) (b) (b) (b) (b) は、f) の略語である。 0.27
we omit the intermediate arrows for the sake of clarity. 明確さのために中間の矢を省略する 0.48
Let’s check that CchC0, Oi satisfies Definitions 2-7 and Property (36) in Definition 8 and it has an arrow C0 −→ ⊥. cchc0, oi が定義 8 における 2-7 とプロパティ (36) の定義を満たし、矢印 c0 −→ {\displaystyle c} が成り立つことを確認しよう。
訳抜け防止モード: cchc0 と oi が 2 - 7 の定義を満たすことを確認しよう 定義 8 のプロパティ (36 ) は、矢印 c0 −→ s を持つ。
0.82
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. カテゴリー理論的意味論のモジュラー表現により, alc の部分論理,すなわち alc を同定し, alc から厳格に派生していることを示す。 0.70
We also proposed a PSPACE nondeterministic algorithm for checking concept unsatisfiability in ALC∀, which implies that ALC∀ is PSPACE. また, ALC における概念不適合性チェックのための PSPACE 非決定性アルゴリズムを提案し, ALC が PSPACE であることを示す。 0.62
For future work, we will investigate the question whether ALC∀ is PSPACE-complete. 今後の課題として, ALC が PSPACE 完全かどうかについて検討する。 0.61
This question is open because ALC∀ (with general TBoxes) may not be included in ALC without TBox. この質問は、alc が tbox なしでは alc に含まれない可能性があるため、オープンである。
訳抜け防止モード: この質問はオープンです ALC は(一般的な TBoxes の) ALC に TBox なしでは含まれない。
0.85
Moreover, we believe that category-theoretical semantics can be extended to more expressive DLs with role constructors. さらに、カテゴリ理論のセマンティクスは、役割コンストラクタを持つより表現力のあるDLにまで拡張できると考えている。 0.61
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 12.D.I. Spivak, R.E. Kent, Ologs:知識表現のための分類的フレームワークPloS 0.84
one 7 (1) (2012) e24274. one 7 (1) (2012) e24274。 0.87
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 0.47
Reasoning 39 (3) (2007) 249–276. 39(3)(2007年)249-276。 0.62
                                                         ページの最初に戻る

翻訳にはFugu-Machine Translatorを利用しています。