Rozdzielczość SLD - SLD resolution

Rozdzielczość SLD ( selektywna rozdzielczość klauzuli liniowej ) jest podstawową regułą wnioskowania używaną w programowaniu logicznym . To wyrafinowanie rozdzielczości , która jest zarówno dźwiękiem, jak i zupełnym zaprzeczeniem dla klauzul Hornu .

Reguła wnioskowania SLD

Biorąc pod uwagę klauzulę celu, przedstawioną jako zaprzeczenie problemu do rozwiązania:

z wybranym literałem i określoną klauzulą wejściową :

którego literał dodatni (atom) jednoczy się z atomem wybranego literału , rozdzielczość SLD wyprowadza kolejną klauzulę celu, w której wybrany literał jest zastępowany literałami ujemnymi klauzuli wejściowej i stosowane jest podstawienie ujednolicające :

W najprostszym przypadku, w logice zdań, atomy i są identyczne, a podstawienie unifikujące jest próżne. Jednak w bardziej ogólnym przypadku podstawienie ujednolicające jest konieczne, aby te dwa literały były identyczne.

Pochodzenie nazwy „SLD”

Nazwę „rozdzielczość SLD” nadał Maarten van Emden dla nienazwanej reguły wnioskowania wprowadzonej przez Roberta Kowalskiego . Jego nazwa wywodzi się od rozdzielczości SL, która jest zarówno słuszna, jak i pełna obalenia dla nieograniczonej klauzuli logiki. „SLD” oznacza „rozdzielczość SL z klauzulami definitywnymi”.

W obu, SL i SLD, „L” oznacza fakt, że dowód rozdzielczości można ograniczyć do liniowej sekwencji klauzul:

gdzie „górna klauzula” jest klauzulą ​​wejściową, a każda inna klauzula jest rozstrzygającą klauzulą, której rodzic jest klauzulą ​​poprzednią . Dowód jest obaleniem, jeśli ostatnia klauzula jest klauzulą ​​pustą.

W SLD wszystkie klauzule w sekwencji są klauzulami celu, a drugi rodzic jest klauzulą ​​wejściową. W rozdzielczości SL drugim rodzicem jest klauzula wejściowa lub klauzula przodka wcześniejsza w sekwencji.

Zarówno w SL, jak i SLD, „S” oznacza fakt, że jedynym literałem rozstrzygniętym w dowolnej klauzuli jest ten, który jest jednoznacznie wybrany przez regułę selekcji lub funkcję selekcji. W rozdzielczości SL wybrany literał jest ograniczony do tego, który został ostatnio wprowadzony do klauzuli. W najprostszym przypadku taką funkcję selekcji „ ostatni na wejściu, pierwszy na wyjściu” można określić przez kolejność, w jakiej literały są zapisywane, jak w Prologu . Jednak funkcja wyboru w rozdzielczości SLD jest bardziej ogólna niż w rozdzielczości SL i w Prologu. Nie ma ograniczeń co do literału, który można wybrać.

Obliczeniowa interpretacja rozdzielczości SLD

W logice klauzul, odrzucenie SLD pokazuje, że wejściowy zbiór klauzul jest niezadowalający. Jednak w programowaniu logicznym obalenie SLD ma również interpretację obliczeniową. Górną klauzulę można interpretować jako zaprzeczenie koniunkcji celów podrzędnych . Wyprowadzenie klauzuli z jest wyprowadzeniem, za pomocą rozumowania wstecznego , nowego zestawu podcelów przy użyciu klauzuli wejściowej jako procedury redukcji celu. Podstawienie jednoczące zarówno przekazuje dane wejściowe z wybranego celu podrzędnego do treści procedury, jak i jednocześnie przekazuje dane wyjściowe z początku procedury do pozostałych niewybranych celów podrzędnych. Klauzula pusta to po prostu pusty zbiór celów podrzędnych, który sygnalizuje, że początkowa koniunkcja celów podrzędnych w klauzuli górnej została rozwiązana.

Strategie rozdzielczości SLD

Rozwiązanie SLD niejawnie definiuje drzewo wyszukiwania alternatywnych obliczeń, w którym początkowa klauzula celu jest powiązana z korzeniem drzewa. Dla każdego węzła w drzewie i dla każdej określonej klauzuli w programie, której literał dodatni jednoczy się z wybranym literałem w klauzuli goal związanej z węzłem, istnieje węzeł potomny powiązany z klauzulą ​​goal uzyskaną przez rozwiązanie SLD.

Węzeł liścia, który nie ma dzieci, jest węzłem sukcesu, jeśli powiązana z nim klauzula goal jest klauzulą ​​pustą. Jest to węzeł niepowodzenia, jeśli powiązana z nim klauzula celu nie jest pusta, ale wybrany literał ujednolica bez dodatniego literału określonych klauzul w programie.

Rozdzielczość SLD jest niedeterministyczna w tym sensie, że nie determinuje strategii przeszukiwania drzewa poszukiwań. Prolog przeszukuje drzewo w pierwszej kolejności, po jednej gałęzi na raz, używając śledzenia wstecznego, gdy napotka węzeł awarii. Przeszukiwanie w głąb jest bardzo wydajne pod względem wykorzystania zasobów obliczeniowych, ale jest niekompletne, jeśli przestrzeń wyszukiwania zawiera nieskończone gałęzie, a strategia wyszukiwania przeszukuje je zamiast odgałęzień skończonych: obliczenia nie kończą się. Inne strategie wyszukiwania, w tym wszerz , najlepiej najpierw , a branch-and-bound wyszukiwania są również możliwe. Ponadto wyszukiwanie może odbywać się sekwencyjnie, po jednym węźle na raz lub równolegle do wielu węzłów jednocześnie.

Rozdzielczość SLD jest również niedeterministyczna w tym sensie, że wspomniano wcześniej, że reguła wyboru nie jest określana przez regułę wnioskowania, ale jest określana przez odrębną procedurę decyzyjną, która może być wrażliwa na dynamikę procesu wykonywania programu.

Przestrzeń poszukiwań rozdzielczości SLD to lub-drzewo, w którym różne gałęzie reprezentują alternatywne obliczenia. W przypadku programów logiki zdań, SLD można uogólnić tak, że przestrzeń poszukiwań jest drzewem i-lub , którego węzły są oznaczone pojedynczymi literałami, reprezentującymi cele cząstkowe, a węzły są łączone przez koniunkcję lub dysjunkcję. W ogólnym przypadku, gdy połączone cele cząstkowe mają wspólne zmienne, reprezentacja i - lub drzewo jest bardziej skomplikowana.

Przykład

Biorąc pod uwagę program logiczny:

q :- p.
p.

i cel najwyższego poziomu:

q.

przestrzeń poszukiwań składa się z pojedynczej gałęzi, w której q jest zredukowana do p której jest zredukowana do pustego zbioru celów podrzędnych, sygnalizujących pomyślne obliczenia. W tym przypadku program jest tak prosty, że nie ma roli funkcji selekcji i nie ma potrzeby wyszukiwania.

W logice klauzul program jest reprezentowany przez zbiór klauzul:

a cel najwyższego poziomu jest reprezentowany przez klauzulę goal z pojedynczym literałem ujemnym:

Przestrzeń poszukiwań składa się z jednego odparcia:

gdzie reprezentuje pustą klauzulę.

Jeśli do programu dodano następującą klauzulę:

q :- r.

wtedy w przestrzeni poszukiwań pojawiłaby się dodatkowa gałąź, której węzeł-liść r jest węzłem awarii. W Prologu, gdyby ta klauzula została dodana na początku oryginalnego programu, wówczas Prolog użyłby kolejności, w jakiej klauzule są zapisywane, aby określić kolejność, w jakiej badane są gałęzie przestrzeni wyszukiwania. Prolog najpierw wypróbuje tę nową gałąź, zakończy się niepowodzeniem, a następnie cofnie się w celu zbadania pojedynczej gałęzi oryginalnego programu i zakończy się powodzeniem.

Jeśli klauzula

p :- p.

zostały dodane do programu, wtedy drzewo wyszukiwania zawierałoby nieskończoną gałąź. Gdyby ta klauzula została wypróbowana jako pierwsza, Prolog wszedłby w nieskończoną pętlę i nie znalazłby pomyślnej gałęzi.

SLDNF

SLDNF jest rozszerzeniem rozdzielczości SLD, aby traktować negację jako awarię . W SLDNF klauzule celu mogą zawierać negację jako literały błędu, powiedzmy formy , którą można wybrać tylko wtedy, gdy nie zawierają zmiennych. Po wybraniu takiego literału wolnego od zmiennych podejmowana jest próba poddania (lub obliczenia podrzędnego) w celu określenia, czy istnieje obalenie SLDNF, zaczynając od odpowiedniego niezatwierdzonego literału jako klauzuli górnej. Wybrany cel podrzędny powiedzie się, jeśli dowód podrzędny się nie powiedzie, i nie powiedzie się, jeśli dowód podrzędny się powiedzie.

Zobacz też

Bibliografia

  1. ^ Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, University of Edinburgh. 1973. Również w Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, s. 569-574.
  2. ^ Robert Kowalski i Donald Kuehner, Rozdzielczość liniowa z funkcją wyboru sztucznej inteligencji, tom. 2, 1971, strony 227-60.
  3. ^ Krzysztof Apt i Maarten van Emden, Wkład do teorii programowania logicznego , Journal of the Association for Computing Machinery. Tom, 1982 - portal.acm.org

Linki zewnętrzne

  • [1] Definicja z Free On-Line Dictionary of Computing