ガードされたロジック

ガード ロジックは、結果が制限されている選択に関係する動的ロジックの選択セットです。

ガード付きロジックの簡単な例は次のとおりです。Xが真であればY、そうでなければZは動的ロジックで(X?;Y)∪(~X?;Z)と表現できます。これはガード付き論理選択を示しています。Xが成り立つ場合、X?;YはYに等しく、~X?;Zはブロックされ、Y∪blockもYに等しくなります。したがって、Xが真の場合は、アクションの主な実行者はY分岐のみを実行でき、偽の場合はZ分岐を実行できます。^[1]

現実世界の例としては、パラドックスの考え方があります。つまり、何かが真と偽の両方であることはできないということです。慎重な論理的選択とは、真の変化がその後のすべての決定に影響を与える選択です。^[2]

ガード付き論理が使用される前は、様相論理を解釈するために 2 つの主要な用語が使用されていました。数学論理とデータベース理論(人工知能) は、第一階述語論理でした。どちらの用語も、第一級論理のサブクラスを見つけ、研究に使用できる解決可能な言語で効率的に使用されていました。しかし、どちらも様相スタイル論理への強力な固定小数点拡張を説明できませんでした。

その後、Moshe Y. Vardi ^[3]は、ツリーモデルが多くの様相スタイルの論理で機能するという推測を立てました。一階述語論理の保護フラグメントは、 Hajnal Andréka、István Németi、Johan van Benthemによって、論文「様相言語と述語論理の境界フラグメント」で初めて導入されました。彼らは、記述、様相、時相論理の主要な特性を述語論理にうまく移植しました。保護論理の堅牢な決定可能性は、ツリーモデルの特性を使用して一般化できることがわかりました。ツリーモデルは、保護論理が様相論理の基本を保持する様相フレームワークを拡張していることを強く示唆するものでもあります。

様相論理は一般に、双模倣の下での不変性によって特徴付けられます。また、双模倣の下での不変性は、オートマトン理論の定義に役立つツリーモデル特性の根源でもあります。

保護された論理には、多数の保護されたオブジェクトが存在します。最初のものは、様相論理の一階論理である保護されたフラグメントです。保護されたフラグメントは、量化の相対的なパターンを見つけることによって様相量化を一般化します。保護されたフラグメントを表すために使用される構文はGFです。もう 1 つのオブジェクトは、保護された固定小数点論理で、 μGFと表記され、保護されたフラグメントを最小の固定点から最大の固定点に自然に拡張します。保護されたバイシミュレーションは、保護された論理を分析するときにオブジェクトです。保護されたバイシミュレーションと一階定義可能でわずかに修正された標準リレーショナル代数内のすべての関係は、保護されたリレーショナル代数として知られています。これはGRA を使用して表記されます。

1階のガード付き論理オブジェクトに加えて、2階のガード付き論理オブジェクトがあります。これはガード付き2階論理として知られ、GSOと表記されます。2階論理と同様に、ガード付き2階論理は、ガードされた関係上の値域が意味的に制限されているかどうかを量化します。これは、値域が任意の関係に制限されている2階論理とは異なります。^[4]

B を、宇宙Bと語彙 τを持つ関係構造とします。

i)集合 X ⊆ B がB内で保護されているとは、 B内に基底原子 α(b_1, ..., b_k) が存在し、X = {b_1, ..., b_k} となる場合である。

ii) τ-構造A、特に部分構造 A ⊆ B は、その宇宙がA内（ B内）の保護された集合である場合に保護されます。

iii)タプル (b_1, ..., b_n) ∈ B^n がBでガードされている場合、あるガード付き集合 X ⊆ B に対して {b_1, ..., b_n} ⊆ X が成立する。

iv)タプル (b_1, ..., b_k) ∈ B^k は、そのコンポーネントがペアごとに異なり、{b_1, ..., b_k} が保護されたセットである場合、 B内の保護されたリストです。空のリストは保護されたリストと見なされます。

v)関係X⊆B^nは、ガードされたタプルのみで構成されている場合、ガードされている。 ^[5]

2 つの τ 構造AとBの間の保護された双模倣は、前後の条件が満たされるような AからBへの有限部分同型f: X → Yの空でない集合Iです。

戻る: I内の すべてのf: X → Yとすべての保護された集合Y` ⊆ Bに対して、 I内の部分同型g: X` → Y`が存在し、f^-1とg^-1はY ∩ Y`で一致します。

第四に、Iのあらゆるf: X → Yとあらゆる保護された集合X` ⊆ Aに対して、 Iの部分同型g: X` → Y`が存在し、fとgはX ∩ X`で一致する。