Loading article…
トランザクションロジックは述語論理の拡張であり、論理プログラムやデータベースにおける状態変化という現象を、明快かつ宣言的な方法で説明します。この拡張では、単純なアクションを複雑なトランザクションに組み合わせ、その実行を制御するために特別に設計された接続詞が追加されます。このロジックは、自然なモデル理論と健全かつ完全な証明理論を備えています。トランザクションロジックには、手続き的意味論と宣言的意味論の両方を持つホーン節のサブセットがあります。このロジックの重要な特徴には、仮説的更新とコミット済み更新、トランザクション実行に対する動的制約、非決定性、一括更新などがあります。このようにして、トランザクションロジックは、人工知能における手続き的知識、アクティブデータベース、オブジェクトデータベースにおける副作用のあるメソッドなど、多くの非論理的な現象を宣言的に捉えることができます。
トランザクションロジックは、1993 年にAnthony BonnerとMichael Kifer [ 1 ]によって最初に提案され、その後、An Overview of Transaction Logic [ 2 ]およびLogic Programming for Database Transactions [ 3 ]でより詳細に説明されました。最も包括的な説明は、1995 年の Bonner と Kifer の技術レポートに掲載されています[ 4 ] 。
後年、トランザクションロジックは、並行性[ 5 ] 、非単調推論[ 6 ]、部分的に定義されたアクション[ 7 ] 、その他の機能[ 8 ] [ 9 ]など、さまざまな方法で拡張されました。
2013年、トランザクションロジックに関するオリジナルの論文は、過去20年間でICLP 1993会議の議事録に掲載された論文の中で最も影響力のある論文として、論理プログラミング協会（APL）の20年賞（Test of Time Award）を受賞しました。
ここで、tinsert はトランザクション挿入の基本更新操作を表します。結合子⊗ は直列接続と呼ばれます。
colorNode <- // 1 つのノードを正しく着色する node(N) ⊗ ¬ colored(N,_) ⊗ color(C) ⊗ ¬(adjacent(N,N2) ∧ colored(N2,C)) ⊗ tinsert(colored(N,C))。 colorGraph <- ¬uncoloredNodesLeft. colorGraph <- colorNode ⊗ colorGraph。 基本的な更新操作であるtdeleteは、トランザクション削除操作を表します。
stack(N,X) <- N>0 ⊗ move(Y,X) ⊗ stack(N-1,Y). stack(0,X)。 move(X,Y) <- pickup(X) ⊗ putdown(X,Y). pickup(X) <- clear(X) ⊗ on(X,Y) ⊗ ⊗ tdelete(on(X,Y)) ⊗ tinsert(clear(Y)). putdown(X,Y) <- wide(Y,X) ⊗ clear(Y) ⊗ tinsert(on(X,Y)) ⊗ tdelete(clear(Y)) ここで、< >は可能性を表す様相演算子です。action1とaction2の両方が可能な場合は、action1を実行します。そうでない場合、action2のみが可能な場合は、action2 を実行します。
実行 <- <>アクション 1 ⊗ <>アクション 2 ⊗ アクション 1。 実行 <- ¬<>action1 ⊗ <>action2 ⊗ action2。 ここで|は、並行トランザクションロジックの並列結合の論理結合子です。 [ 5 ]
食事中の哲学者 <- phil(1) | phil(2) | phil(3) | phil(4). トランザクションロジックには、いくつかの実装例が存在する。
これらの実装はすべてオープンソースです。