ガード付きロジック

ガード付きロジックとは、結果が限定されている選択に関わる動的ロジックの選択集合のことである。

ガード付き論理の簡単な例は次のとおりです。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が論文「様相言語と述語論理の境界付きフラグメント」で初めて導入しました。彼らは、記述論理、様相論理、および時間論理の重要な特性を述語論理にうまく移しました。ガード付き論理の堅牢な決定可能性は、ツリー モデルの特性で一般化できることがわかりました。ツリー モデルはまた、ガード付き論理が様相論理の基本を保持する様相フレームワークを拡張していることを示す強力な証拠にもなり得ます。

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

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

一次ガード付き論理オブジェクトに加えて、二次ガード付き論理オブジェクトも存在する。これはガード付き二次論理と呼ばれ、 GSOと表記される。二次論理と同様に、ガード付き二次論理は、ガード付き関係の範囲が意味的に制限される範囲を量化する。これは、範囲が任意の関係に制限される二次論理とは異なる。^{[ 4 ]}

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

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

ii) τ構造A、特に部分構造A ⊆ Bは、その全体集合がA（B ）内のガード集合である場合にガードされている。

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

iv)タプル (b_1, ..., b_k) ∈ B^k は、その構成要素が互いに異なり、{b_1, ..., b_k} がガードされた集合である場合、 Bのガードされたリストである。空のリストもガードされたリストとみなされる。

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