====== AP13 Prolog ======

===== Zadání ====

(SLD-rezoluce, SLD-stromy, výpočetní mechanismus Prologu, základy programování v Prologu)

====== Vypracování ======
==== Rezoluce ====

**Rezoluce** –- dokazuje se nesplnitelnost formulí, jsou v KNF, v kořenu je □ a nebo dokazovaná formule C, v listech jsou jednotlivé klauzule S, ve vnitřních listech resolventy

**Lineární rezoluce** –- jde o posloupnost dvojic <math><C_{0}, B_{0}></math>, ... ,  <math><C_{n}, B_{n}></math> takovou, že <math>C = C_{n+1}</math>  a 
  - <math>C_{0}</math> a všechny <math>B_{i}</math> jsou z S anebo nějaké <math>C_{j}</math>, kde <math>j<i</math>
  - každé <math>C_{i+1}</math>, <math>i \leq n</math> je rezolventou <math>C_{i}</math> a <math>B_{i}</math> (vstupní klauzule S, boční <math>B_{i}</math> a střední <math>C_{i}</math>)
  * je korektní a úplná

**Lineární vstupní rezoluce** (LI) množiny <math>S=P \cup \{ G\}</math> je lineární vyvrácení S, které začíná klauzulí G, a bočními klauzulemi jsou jen klauzule z P. 
  *je úplná jen pro Hornovy klauzule

**Hornovy klauzule** (jsou v Prologu) = klauzule s nejvýše jedním pozitivním literálem (dají se reprezentovat jako implikace) 

Typy: 
  - programové –- **fakta** (bez negativního literálu. p.), **pravidla** (s aspoň 1 negativním literálem p:-q.)
  - **cíle** –- bez pozitivního literálu ?-p. (t.j. ekvivalent {neg p})

**LD rezoluce** –- už máme uspořádané klauzule a při rezoluci vkládáme dovnitř. LD rezoluční vyvrácení <math>P \cup \{ G\}</math> je postupnost <math><G_{0}, C_{0}></math>, ... , <math><G_{n}, C_{n}></math> uspořádaných klauzulí taková, že <math>G_{0}=G, G_{n+1}=</math>□, <math>C_{i} \in T</math> a každé <math>G_{i}</math>,  <math>1\leq i\leq n</math> je rezolventou uspořádaných klauzulí <math>G_{i-1}</math> a <math>C_{i-1}</math> 

==== SLD-rezoluce ====
**SLD rezoluce** -– lineární vstupní rezoluce se selekčním pravidlem (selekční pravidlo = libovolná funkce, která vybere literál z každé uspořádané cílové klauzule) 
  * úplnost SLD-rezoluce pro Prolog, t.j. pro Hornovy klauzule (umí to určitě vyvrátit, když je to možné)
  * pomocí selekčního pravidla algoritmizujeme výběr literálu z cílové klauzule, na které se bude rezolvovat
  * SLD-rezoluce je korektní a úplná pro Hornovy klauzule
  * budeme používat nejlevější literál

=== Význam SLD rezoluce ===
 : máme množinu klauzulí **P** a cílovou klauzuli <math>G=[\neg A_{1}(\vec{x}) \cdots \neg A_{n}(\vec{x})]</math>
  * dokazujeme nesplnitelnost <math>P \cup \lbrace G \rbrace</math>, tj. <math>P \wedge \forall \vec{x}(\neg A_{1}(\vec{x}) \cup \cdots \cup \neg A_{n}(\vec{x}))</math>
  * uvedená nesplnitelnost je ekvivalentní <math>P \vdash \neg G</math>, tj. <math>P \vdash \exists \vec{x}(A_{1}(\vec{x}) \wedge \cdots \wedge A_{n}(\vec{x}))</math>
  * zadáním cíle **G** tedy chceme zjistit, zda existují nějaké objekty, které na základě **P** splňují formuli <math>A_{1}(\vec{x})\wedge \cdots \wedge A_{n}(\vec{x})</math>
  * aplikujeme-li kompozici všech mgu postupně použitých při SLD-odvození na jednotlivé proměnné vektoru <math>\vec{x}</math>, získáme konkrétní případy zmíněných objektů splňujících danou formuli

<box 100% round blue|Příklad(1)>
{{:home:inf:logika_rezoluce1.jpg|}}
</box>

==== SLD-stromy ====

**SLD strom** pro program P a cíl G: v kořeni je G. Když je libovolný uzel označený G‘, tak jeho bezprostřední následníci jsou označení výsledkem rezoluce nejlevějšího literálu G‘ se všemi použitelnými klauzulemi z P. 
  * takto vznikne hodně cest, i ty neúspěšné, 
  * vždy v každém uzlu jsou všechny literály negované

<box 100% round blue|Příklad(2)>
EDIT: Tento příklad obsahuje chybu - doporučuji se podívat na interaktivní přednášku pana Popelínského:((https://is.muni.cz/auth/th/173318/fi_b/5726674/5726798/3-24.htm))
Chyba je hned na 1. řádku.
Ten má vypadat takto: <math>1. [P(x,y),\neg Q(x,z), R(z,y)]</math>
{{:home:inf:logika_rezoluce2.jpg|}}
</box>

==== Prolog ====
Prolog je logický programovací jazyk. Patří mezi tzv. deklarativní programovací jazyky, ve kterých programátor popisuje pouze cíl výpočtu, přičemž přesný postup, jakým se k výsledku program dostane, je ponechán na libovůli systému. Prolog se snaží o pokud možno abstraktní vyjádření faktů a logických vztahů mezi nimi s potlačením imperativní složky. Prolog je využíván především v oboru umělé inteligence a v počítačové lingvistice (obzvláště zpracování přirozeného jazyka, pro nějž byl původně navržen). 

==== Výpočetní mechanismus Prologu ====
  * úspěšné cesty v SLD-stromě jsou ty, které končí □, ostatní jsou neúspěšné.

Vyhodnocovací mechanizmus Prologu prochází SLD-strom do hloubky zleva doprava a hledá (první) úspěšnou cestu (backtracking) – případně projde celý strom a vyhlásí, že to není možné.

- zadání středníku (;) po úspěšném vyhodnocení čísla vynutíme backtracking a hledání alternativního důkazu
- odpověď „no“ systému znamená, že daný cíl není logickým důsledkem programu (případně že nemá alternativní důkaz) prologovská strategie prohledávání stavového prostoru (do hloubky) může vést k zacyklení (i v případě, že existují úspěšné větve) 

**Příklad programu, který vede k zacyklení, i když existují úspěšné větve:** 
''q:- r.''
''r:- q.''
''q.''
''?- q.''

==== Základy programování v Prologu ====
 
**Logické programování:**
  - logický program = libovolná konečná množina programových Hornových klauzulí
  - odvozování (dokazování) cílů založené na SLD-rezoluci
  - deklarativní (specifikace programu je přímo programem)
  - teoretický model, zachovává úplnost

**Prolog** 
  * konkrétní implementace logického programovacího jazyka 
  * ztráta úplnosti (možnost zacyklení)
  * vhodný na řešení problémů týkajících se objektů a vztahů mezi nimi, 
  * do značné míry využívá rekurzi


=== Syntax : datové objekty ===
  * Základem jsou **termy** (konstanty, proměnné, složené termy)
      - konstanty 
              - celá čísla (0, -12, ...)
              - desetinná čísla (1.0, 4.5E7, ...)
              - atomy ('ježek', [], ==, ...)
      - proměnné (N, VYSLEDEK, ...)
      - složené termy: 
              - funktor (jméno, arita)
              - argumenty (bod(X,Y,Z),tree(Value, tree(LV,LL,LR), tree(RV,RL,RR)))

=== Syntax: program ===
              - množina programových klauzulí
              - proměnné v lokální klauzuli
              - pravidla: **hlava:- tělo.**
                        - **date(D,M,Y):- day(D), month(M), year(Y).**
              - fakta: pravidla s prázdným tělem
              - cíle: klauzule bez hlavy, reprezentují dotazy
=== Poznámky ===
  * do značné míry využívá rekurzi
  * patří mezi deklarativní programovací jazyky

  * využíván v oboru umělé inteligence a zpracování přirozeného jazyka

  * založen na predikátové logice prvního řádu, zaměřuje se na Hornovy klauzule
              - seznamy 
                   - definovány induktivně
                   - [] - prázdný seznam
  * základní využívané přístupy jsou unifikace a rekurze

  * anonymní proměnná **_** (podtržítko), její hodnota není podstatná
              - používá se v pravidlech **je_dite(X):- dite(X,_).**
  * základ Prologu je databáze klauzulí (fakta a pravidla), nad kterou je možno klást dotazy formou tvrzení, kde Prolog vyhodnocuje jejich pravdivost
              - fakta - nejjednodušší klauzule, vypovídající o vlastnostech a vztazích mezi objekty, př. **dívka(monika)**
              - pravidla - odvozování nových dat pomocí aplikace **hlavička:- tělo.**
                         - hlavička - odvozovaný fakt
                         - tělo - podmínky
                         - př. **syn(A,B):- rodic(B,A), muz(A).**

====== Literatura ======
Wikipedia Prolog - [[http://cs.wikipedia.org/wiki/Prolog_%28programovac%C3%AD_jazyk%29]]
Slidy předmětu - [[http://www.fi.muni.cz/usr/popelinsky/lectures/bak_logika/]]
Vypracování otázek Elena Halicová - [[http://www.fi.muni.cz/~xhalic1/statnice/vypracovaneIM.doc]]


~~DISCUSSION~~