A logikai programozás , SLD-felbontású (SLD jelentése a fentiekben kiválasztott , lineáris , definiált ) egy algoritmus bizonyítani elsőrendű logikában formula egy sor Horn kikötések . Lineáris felbontáson alapszik, a meghatározott tagmondatokon kiválasztási funkcióval. Az SLD felbontást jobban ismeri a kiterjesztése, az SLDNF (az NF jelentése negáció mint kudarc , az negáció mint kudarc ), amelyet a Prolog algoritmusnyelv használ .
A definiált tagmondat Horn-klauzula, amely pontosan egy pozitív literált tartalmaz . A fogalom tehát magában foglalja a szigorú Horn- és pozitív Horn-záradékokat. Az SLD-felbontás összefüggésében egy meghatározott tagmondat pozitív literálját fejnek , következtetésnek vagy célnak nevezzük . A negatív literálok disszjunkcióját, ha léteznek, testnek , előzményeknek vagy részcéloknak nevezzük . Például a Horn záradék
¬ a ∨ ¬ b ∨ c
logikailag egyenértékű:
( a ∧ b ) → c
vagy a következő Prolog-szabály:
c :- a, b.
Minden esetben c a következtetés, a és b az előzmények.
Adott egy program (egy sor Horn-tagmondat) és egy lekérdezés (a pozitív literálok együttese, amelyet igaznak akarunk bizonyítani a programból), az SLD-megoldás globálisan működik, mint a megoldás egyéb formái., Megkísérelve egyesíteni a Horn-mondatokat hozzon létre újakat, amíg ellentmondás nem születik, vagy új összefogás nem lehetséges.
Pontosabban, az SLD-felbontás a kérés tagadásának megalkotásával kezdődik (így negatív Horn-záradékot kapunk, amelyet a célok listájának fogunk nevezni ), majd ennek az tagadásnak az első elemét egyesíti a program záradékával. A kérdéses tagmondatot determinisztikusan keresik, a program első mondatának megkeresésével, amelynek feje a céllista első tagadásának pozitív párja.
Ha ellentmondást találnak, akkor a kérés tagadása nem egyeztethető össze a programmal, így a kérés sikeresen véget ér. Ha a céllista első negatív kifejezésére nem található egységesítés, akkor a lekérdezés sikertelen lesz. Ha ellentmondás nélküli egyesítés létezik, akkor az új céllista a régi és a kiválasztott klauzula együttesévé válik, és az SLD-felbontás újraindul (rekurzívan) az új céllistán. Ha egy részlekérdezés sikertelen, akkor a magasabb szintű egyesítés meghiúsul, és az algoritmus a (z) program többi részében egy másik egyesítést keres a célok listájának első kifejezésére. Ezt a lépést visszalépésnek nevezzük .
Vegyük példának a következő programot:
q ∨ ¬ o ovalamint a lekérdezés:
{ q }A célok listája egyetlen tagadásból áll {¬ q }, és a programban egy egységesíthető záradékot keresnek. Az első tagmondat megegyezik, ki van választva. A célok listájának a záradékkal való összekapcsolása a következőket adja:
( q ∨ ¬ p ) ∧ ¬ qVan:
¬ oAz algoritmus újbóli elindításával ezen új céllistán egységet találunk a program második mondatával, ami ellentmondáshoz vezet:
p ∧ ¬ pA (z) {¬ q } célok listája ezért nem kompatibilis a programmal, ezért a (z) { q } kérés sikeresen teljesül.
Megjegyzés: A Prologban az első tagmondatot írnák q :- p . Az algoritmust ezután a következőképpen írnánk le: „A bizonyításhoz qkeressen egy záradékot, amelynek qfeje van. Az első tagmondat egyezik, és pmeg kell mutatni. A második mondat ptehát qbebizonyosodik. "
Ha a következő záradék kerülne a program tetejére:
q ∨ ¬ rakkor az SLD-megoldó algoritmus először azt választaná ki, hogy egyesítéssel kapja meg a ¬ r- t, majd nem egyesíti a ¬ r-t . Ez visszalépéshez vezetne; az algoritmus újból megpróbálná egyesíteni ¬ q- t egy záradékkal a program többi részében. A q ∨ ¬ p tagmondatot választanák ki, és visszalépnénk az előző esetre.