Logika transakcji

Transaction Logic to rozszerzenie logiki predykatów , które w czysty i deklaratywny sposób wyjaśnia zjawisko zmian stanu w programach logicznych i bazach danych . To rozszerzenie dodaje łączniki zaprojektowane specjalnie do łączenia prostych działań w złożone transakcje i zapewniania kontroli nad ich wykonaniem. Logika ma naturalną teorię modeli oraz solidną i kompletną teorię dowodową . Logika transakcji ma klauzulę Horna podzbiór, który ma zarówno semantykę proceduralną, jak i deklaratywną. Do ważnych cech logiki należą hipotetyczne i zatwierdzone aktualizacje, dynamiczne ograniczenia dotyczące wykonywania transakcji, niedeterminizm i aktualizacje zbiorcze. W ten sposób Transaction Logic jest w stanie deklaratywnie uchwycić szereg nielogicznych zjawisk, w tym wiedzę proceduralną w sztucznej inteligencji , aktywne bazy danych , czy metody z efektami ubocznymi w obiektowych bazach danych .

Logika transakcji została pierwotnie zaproponowana przez Anthony'ego Bonnera i Michaela Kifera , a później opisana bardziej szczegółowo w i. Najbardziej wyczerpujący opis znajduje się w.

W późniejszych latach Transaction Logic został rozszerzony na różne sposoby, w tym współbieżność , rozumowanie możliwe do pokonania , częściowo zdefiniowane działania i inne funkcje.

W 2013 roku oryginalny artykuł na temat logiki transakcyjnej zdobył nagrodę 20 -letniej próby czasu przyznawaną przez Association for Logic Programming jako najbardziej wpływowy artykuł z konferencji ICLP 1993 w ciągu ostatnich 20 lat.

Przykłady

Kolorowanie wykresów

Tutaj tinsert oznacza elementarną operację aktualizacji wstawiania transakcyjnego . Spójnik ⊗ nazywamy koniunkcją szeregową .

colorNode <- // pokoloruj prawidłowo jeden węzeł node(N) ⊗ ¬ kolorowy(N,_) ⊗ kolor(C) ⊗ ¬(przylegający(N,N2) ∧ kolorowy(N2,C)) ⊗ tinsert(kolorowy(N, C)). colorGraph <- ¬uncoloredNodesLeft. colorGraph <- colorNode ⊗ colorGraph.

Układanie piramidy

Podstawowa aktualizacja tdelete reprezentuje transakcyjną operację usuwania .

stos(N,X) <- N>0 ⊗ ruch(Y,X) ⊗ stos(N-1,Y). stos(0,X). ruch(X,Y) <- podnieś(X) ⊗ odłóż(X,Y). podnieś(X) <- wyczyść(X) ⊗ wł(X,Y) ⊗ ⊗ tdelete(w(X,Y)) ⊗ tinsert(wyczyść(Y)). putdown(X,Y) <- szerszy(Y,X) ⊗ clear(Y) ⊗ tinsert(on(X,Y)) ⊗ tdelete(clear(Y)).

Hipotetyczna egzekucja

Tutaj <> jest operatorem modalnym możliwości: Jeśli zarówno akcja1 , jak i akcja2 są możliwe, wykonaj akcję1 . W przeciwnym razie, jeśli możliwa jest tylko akcja 2 , wykonaj ją.

wykonaj <- <>akcja1 ⊗ <>akcja2 ⊗ akcja1. wykonaj <- ¬<>akcja1 ⊗ <>akcja2 ⊗ akcja2.

Filozofowie jedzenia

tutaj | jest spójnikiem logicznym koniunkcji równoległej współbieżnej logiki transakcji.

jadalniaFilozofowie <- phil(1) | fil(2) | fil(3) | fil(4).

Implementacje

Istnieje wiele implementacji logiki transakcji:

• Oryginalna realizacja.
• Implementacja logiki transakcji współbieżnych.
• Logika transakcji wzbogacona o tworzenie tabel . Implementacja logiki transakcji została również włączona jako część Flora-2 .

Wszystkie te implementacje są open source .

Linki zewnętrzne

• Witryna internetowa Flora-2 zawierająca dodatkowe artykuły na temat logiki transakcji