Logika strzeżona - Guarded logic

Strzeżone logika jest zestaw wybór z dynamicznym logiki zaangażowanych w wybory, w których efekty są ograniczone.

Prosty przykład logiki chronionej jest następujący: jeśli X jest prawdziwe, to Y, w przeciwnym razie Z można wyrazić w logice dynamicznej jako (X?;Y)∪(~X?;Z). Pokazuje to strzeżony logiczny wybór: jeśli X jest spełnione, to X?;Y jest równe Y, a ~X?;Z jest zablokowane, a Y∪blok jest również równe Y. Stąd, gdy X jest prawdziwe, główny wykonawca akcji może wziąć tylko gałąź Y, a gdy jest fałszywa gałąź Z.

Przykładem ze świata rzeczywistego jest idea paradoksu : coś nie może być jednocześnie prawdą i fałszem. Strzeżony logiczny wybór to taki, w którym każda zmiana prawdy wpływa na wszystkie decyzje podejmowane w dalszej kolejności.

Historia

Przed zastosowaniem logiki chronionej istniały dwa główne terminy używane do interpretacji logiki modalnej. Logika matematyczna i teoria baz danych (sztuczna inteligencja) były logiką predykatów pierwszego rzędu. Oba terminy znalazły podklasy logiki pierwszej klasy i były skutecznie używane w językach rozwiązywalnych, które można wykorzystać do badań. Ale żadne z nich nie mogło wyjaśnić potężnych rozszerzeń stałoprzecinkowych do logiki stylu modalnego.

Później Moshe Y. Vardi wysunął przypuszczenie, że model drzewa będzie działał dla wielu logik stylów modalnych. Strzeżony fragment logiki pierwszego rzędu po raz pierwszy wprowadzili Hajnal Andréka , István Németi i Johan van Benthem w artykule Języki modalne i ograniczone fragmenty logiki predykatów. Z powodzeniem przenieśli kluczowe właściwości logiki opisu , modalnej i temporalnej do logiki predykatów. Stwierdzono, że niezawodną rozstrzygalność logiki chronionej można uogólnić za pomocą właściwości modelu drzewa. Model drzewa może również stanowić silną wskazówkę, że strzeżona logika rozszerza ramy modalne, które zachowują podstawy logik modalnych.

Logiki modalne generalnie charakteryzują się niezmiennością przy bisymulacji . Zdarza się również, że niezmienniczość przy bisymulacji jest korzeniem własności modelu drzewa, co pomaga w zdefiniowaniu teorii automatów .

Rodzaje strzeżonej logiki

W ramach Guarded Logic istnieje wiele strzeżonych obiektów. Pierwszy to strzeżony fragment, który jest logiką pierwszego rzędu logiki modalnej. Chronione fragmenty uogólniają kwantyfikację modalną poprzez znajdowanie względnych wzorców kwantyfikacji. Składnia używana do oznaczenia chronionego fragmentu to GF . Innym obiektem jest logika strzeżonego punktu stałego, oznaczona μGF, naturalnie rozciąga strzeżony fragment od punktów stałych od najmniejszego do największego. Bisymulacje strzeżone to obiekty, które analizując logikę strzeżoną. Wszystkie relacje w nieco zmodyfikowanej standardowej algebrze relacyjnej z strzeżoną bisymulacją i definiowalną w pierwszym rzędzie są znane jako strzeżona algebra relacyjna . Jest to oznaczone za pomocą GRA .

Wraz z chronionymi obiektami logiki pierwszego rzędu istnieją obiekty logiki chronionej drugiego rzędu. Jest znany jako Guarded Second-Order Logic i oznaczany jako GSO . Podobnie jak w przypadku logiki drugiego rzędu , strzeżona logika drugiego rzędu określa ilościowo, którego zakres nad strzeżonymi relacjami ogranicza go semantycznie. Różni się to od logiki drugiego rzędu, której zakres jest ograniczony do dowolnych relacji.

Definicje strzeżonej logiki

Niech B będzie strukturą relacyjną z wszechświatem B i słownikiem τ.

i) zbioru X ⊆ B jest chroniony w B , jeśli istnieje alfa ziemia atom (b_1, ..., b_k) w B taki, że X = {b_1, ..., b_k}.

ii) Struktura τ A , w szczególności podstruktura A ⊆ B, jest strzeżona, jeśli jej wszechświat jest zbiorem strzeżonym w A (w B ).

iii) Krotka (b_1, ..., b_n) ∈ B^n jest strzeżona w B, jeśli {b_1, ..., b_n} ⊆ X dla jakiegoś strzeżonego zbioru X ⊆ B.

iv) Krotka (b_1, ..., b_k) ∈ B^k jest listą strzeżoną w B, jeśli jej składowe są parami różne, a {b_1, ..., b_k} jest zbiorem strzeżonym. Pusta lista jest traktowana jako lista strzeżona.

v) Relacja X ⊆ B^n jest strzeżona, jeśli składa się tylko z krotek strzeżonych.

Strzeżona bisymulacja

Chroniony bisimulation pomiędzy dwoma τ strukturach A i B jest niepusty zestaw I skończonej częściowego izomorficznej f: X → Y od A do B , tak że warunki przodu i do tyłu są spełnione.

Wstecz: Dla każdego f: X → Y w I i dla każdego strzeżonego zbioru Y` ⊆ B , istnieje częściowy izomorficzny g: X` → Y` w I taki, że f^-1 i g^-1 zgadzają się z Y ∩ Tak .

Czwarty Dla każdego f: X → Y w I i dla każdego zestawu strzeżonym X` ⊆ A istnieje częściowy izomorficzne G: X` → Y` się , że taki sposób, f i g uzgodnić X ∩ X` .

Bibliografia