Stacks Image 10307

Metody programowania w logice

Stacks Image 10303
Algorytm = Logika + Sterowanie
Robert Kowalski

Opis kursu

Moduł wprowadzający w teoretyczne podstawy programowania w logice. Na wykładzie omawiane są zagadnienia związane z automatycznym dowodzeniem twierdzeń opartym na zasadzie rezolucji. Po omówieniu modeli Herbranda dla zbioru formuł logiki pierwszego rzędu i twierdzenia Herbranda prezentowana jest rezolucja i jej modyfikacje oraz strategie zwiększania ich efektywności. Na zakończenie wykładu prezentowana jest SLDNF-rezolucja stosowana w języku programowania Prolog oraz semantyka prologowych programów oparta na najmniejszym punkcie stałym operacji natychmiastowej konsekwencji.

Zasady zaliczenia

  • Ocena wystawiana z modułu jest średnią ważoną ocen osiągniętych przez studenta z wykładu (waga 60%) i z ćwiczeń (waga 40%), przy czym obie oceny muszą być pozytywne.
  • Wiedza oraz kompetencje społeczne sprawdzane są podczas kolokwium jakie odbywa się w ostatnim tygodniu zajęć (ocena z wykładu).
  • Umiejętności studenta sprawdzane są podczas ćwiczeń na kartkówkach (ocena z ćwiczeń).
  • Obecność na ćwiczeniach jest obowiązkowa. Trzy nieusprawiedliwione nieobecności skutkują oceną niedostateczną z ćwiczeń, a co za tym idzie, oceną niedostateczną z grupy kursów.
  • W ostatnim tygodniu zajęć prowadzący ćwiczenia wysyłają do wykładowcy oceny jakie osiągnęli studenci w ich grupach (nie można zaliczać ćwiczeń w czasie sesji - ocena z ćwiczeń musi być wystawiona w ostatnim tygodniu zajęć).
  • Wykładowca oblicza średnią ważoną z ocen z wykładu i z ćwiczeń a następnie wyliczoną średnią wpisuje studentowi do protokołu w JSOS.

Plan wykładu

Materiały do wykładu powstały na podstawie książek J.W. LLoyd [1], C.L.Chang i R.C.T Lee [2] i M. Wójcik [3] oraz wybranych artykułów naukowych.

  • Termy i termy cykliczne (2 g) Termy; reprezentacja termów; termy cykliczne; podstawienia; własności podstawień
  • Dopasowanie i unifikacja (2g) Algorytm unifikacji; własności algorytmu unifikacji; P-zupełność problemu unifikacji
  • Semiunifikacja (2g) Uogólnienie unifikacji; nierozstrzygalność semiunifikacji; zastosowania semiunifikacji
  • Interpretacja formuł logiki pierwszego rzędu (2g) Interpretacja; model; spełnialność, prawdziwość i sprzeczność
  • Postać normalna i skolemizacja (2g) Postać normalna; standardowa postać Skolema; skolemizacja
  • Procedura Herbranda (2g) Uniwersum Herbranda; drzewa semantyczne; twierdzenie Herbranda; implementacja procedury Herbranda
  • Zasada rezolucji (2g) Zasada rezolucji dla logiki pierwszego rzędu; pełność rezolucji; strategie usuwania
  • Rezolucja semantyczna (2g) Rezolucja semantyczna dla logiki pierwszego rzędu; pełność rezolucji semantycznej; implementacja rezolucji semantycznej
  • Rezolucja indeksowana (2g) Rezolucja indeksowana dla logiki pierwszego rzędu; pełność rezolucji indeksowanej; implementacja rezolucji indeksowanej
  • Rezolucja liniowa (2g) Rezolucja liniowa dla logiki pierwszego rzędu; pełność rezolucji liniowej; implementacja rezolucji liniowej
  • Strategie sterowania (2g) Heurystyczne funkcje oceny; estymacja funkcji oceny
  • Relacja równości (2g) Paramodulacja; E-rezolucja; Demodulacja; algorytm Knutha-Bendixa
  • SLD(NF)-rezolucja (2g) SLD-rezolucja; SLD-drzewo; negacja jako niepowodzenie; SLDNF-las
  • Najmniejszy model Herbranda (2g) Operator konsekwencji, punkt stały, najmniejszy model Herbranda
  • Podsumowanie wykładu (2g)

Ćwiczenia

Zadania zostały zaczerpnięte z książek J.W. Lloyd [1], U. Nilsson i J. Małuszyński [4] i innych materiałów dydaktycznych.

  • Lista 1: Termy (termin zaliczenia: pierwszy tydzień)
  • Lista 2: Podstawienia (termin zaliczenia: drugi tydzień)
  • Lista 3: Unifikacja (termin zaliczenia: trzeci tydzień)
  • Lista 4: Semi-unifikacja (termin zaliczenia: czwarty tydzień)
  • Lista 5: Interpretacja i model (termin zaliczenia: szósty tydzień)
  • Lista 6: Skolemizacja (termin zaliczenia: siódmy tydzień)
  • Lista 7: Procedura Herbranda (termin zaliczenia: ósmy tydzień)
  • Lista 8: Zasada rezolucji (termin zaliczenia: dziewiąty tydzień)
  • Lista 9: Rezolucja semantyczna (termin zaliczenia: jedenasty tydzień)
  • Lista 10: Specjalne przypadki rezolucji semantycznej (termin zaliczenia: dwunasty tydzień)
  • Lista 11: Rezolucja liniowa (termin zaliczenia: trzynasty tydzień)
  • Lista 12: Najmniejszy model Herbranda (termin zaliczenia: ostatni tydzień zajęć)

Przykłady programów

Literatura

[1] J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.
[2] C.L. Chang, R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, Ltd., 1973.
[3] M. Wójcik. Zasada rezolucji. Metoda automatycznego wnioskowania. PWN, 1991.
[4] U. Nilsson, J. Małuszyński. Logic, Programming and Prolog. John Wiley & Sons, 1995.