Ugrás a tartalomhoz

Szerkesztő:Bbr98/SLD rezolúció

A Wikipédiából, a szabad enciklopédiából

Az SLD rezolúció ( Selective Linear Definite clause resolution) a logikai programozásban alkalmazott alapvető következtetési szabály . Ez a rezolúció finomítása.

Az SLD következtetési szabály

[szerkesztés]

Adott egy goal klóz amely a megoldandó probléma tagadása:

kiválasztott literállal és egy meghatározott input klózzal :

akinek a pozitív literálja (atom) egyesül az atommal a kiválasztott literálból , Az SLD felbontás egy újabb goal klózt eredményez, amelyben a kiválasztott literál helyébe az input klóz negatív literáljai lépnek és az egyesítő helyettesítést alkalmazzák:

A legegyszerűbb esetben, a propozíciós logikában az atomok és azonosak, és az egyesítő helyettesítés üres. Általánosabb esetben azonban szükséges az egyesítő helyettesítés, hogy a két literál azonos legyen.

Az "SLD" név eredete

[szerkesztés]

Az "SLD-felbontás" nevet Maarten van Emden adta a Robert Kowalski által bevezetett meg nem nevezett következtetési szabályra. [1] Neve az SL rezolúcióból származik. Az "SLD" jelentése "SL felbontás határozott klózokkal".

Mind az SL, mind az SLD esetében az "L" azt a tényt jelenti, hogy a bizonyítás a klózok lineáris sorrendjére korlátozható:

ahol a "top klóz" egy input klóz, és minden más klóz olyan rezolvens, akinek egyik szülője az előző klóz . A bizonyítás cáfolat, ha az utolsó klóz az üres klóz.

Az SLD-ben a szekvencia összes klóza goal klóz, a másik szülő pedig input klóz. SL rezolúcióban a másik szülő vagy bemeneti klóz, vagy egy előd klóz a sorozat elején.

SLD felbontási stratégiák

[szerkesztés]

Az SLD rezolúciós implicit módon meghatározza az alternatív számítások keresési fáját, amelyben a kezdeti goal klóz a fa gyökeréhez kapcsolódik. A fa minden csomópontjához és a program minden olyan meghatározott klózhoz, amelynek pozitív literálja egyesül a kiválasztott literállal a csomóponthoz társított goal klózban, létezik egy gyermekcsomópont az SLD felbontásával kapott goal klózhoz.

A levél nélküli csomópont, amelynek nincs gyermeke, akkor sikeres csomópont, ha a hozzá tartozó goal klóz az üres klóz.

Az SLD rezolúció nem determinisztikus abban az értelemben, hogy nem határozza meg a keresési stratégiát a keresési fa felfedezéséhez. A Prolog először a fa mélységében kutat, egy-egy ágat, visszalépés segítségével, amikor egy hibacsomópontra bukkan. A mélységi keresés nagyon hatékony a számítási erőforrások felhasználásában, de hiányos, ha a keresési tér végtelen ágakat tartalmaz: a számítás nem fejeződik be. Más keresési stratégiák is alkalmazhatók, ideértve a szélességikeresés, a legjobbat először keresés, valamint az elágazás és kolátozás keresést. Ezenkívül a keresés történhet egymás után, egy-egy csomópont, vagy párhuzamosan sok csomópont egyszerre.

Az SLD rezolúció szintén nem determinisztikus a korábban említett értelemben, miszerint a kiválasztási szabályt nem a következtetési szabály, hanem egy külön döntési eljárás határozza meg, amely érzékeny lehet a program végrehajtási folyamatának dinamikájára.

Az SLD felbontású keresési tér egy vagy-fa, amelyben a különböző ágak alternatív számításokat képviselnek. A propozíciós logikai programok esetében az SLD általánosítható úgy, hogy a keresési tér egy és-vagy fa, amelynek csomópontjait egyetlen literálok jelölik, amelyek részcélokat képviselnek, és a csomópontokat összekapcsolják konjunkcióval vagy diszjunkcióval. Általános esetben, amikor a konjugált részcélok változókat osztanak meg, az és-vagy fa ábrázolása bonyolultabb.

Példa

[szerkesztés]

Adott a logikai program:

q :- p.
p.

és a legfelső szintű cél:

q.

a keresési tér egyetlen elágazásból áll, amelyben q p redukáljuk, amely a részcélok üres halmazává redukálódik, jelezve a sikeres számítást. Ebben az esetben a program olyan egyszerű, hogy nincs szerepe a kiválasztási funkciónak, és nincs szükség semmilyen keresésre.

Klauzális logikában a programot a tagok sora képviseli:

a legfelső szintű célt pedig a goal klóz képviseli egyetlen negatív literállal:

A keresési tér egyetlen cáfolatból áll:

ahol a az üres klózt jelenti.

Ha a következőklózt adnánk a programhoz:

q :- r.

akkor lenne egy további elágazás a keresési térben, amelynek levélcsomópontja r hibacsomópont. A Prologban, ha ezt a klózt hozzáadnák az eredeti program elejéhez, akkor a Prolog a klózok írási sorrendjét használná a keresési tér elágazásainak sorrendjének meghatározásához. A Prolog először ezt az új ágat próbálta ki, kudarcot vallott, majd visszalépett, hogy megvizsgálja az eredeti program egyetlen ágát, és sikeres legyen. Ha ez a klóz:

p :- p.

most hozzáadódna a programhoz, akkor a keresési fa egy végtelen ágat tartalmazna. Ha ezt a klózt próbálná ki először, akkor a Prolog végtelen ciklusba kerülne, és nem találná meg a sikeres elágazást.

Az SLDNF [2] az SLD rezolóció kiterjesztése, hogy kezelje a negációt, mint kudarcot . Az SLDNF-ben a goal klózok tartalmazhatnak tagadásokat hibás literálként, hívjuk az alakot -nek, amelyek csak akkor választhatók ki, ha nem tartalmaznak változót. Ilyen változó nélküli literál kiválasztásakor egy alszámítással próbálják megállapítani, hogy van-e SLDNF cáfolat a megfelelő nem negatív literálból kiindulva mint felső klóz. A kiválasztott részcél akkor sikerül, ha az alellenálló meghiúsul, és akkor is, ha az alellenálló sikerül.

Lásd még

[szerkesztés]
  • John Alan Robinson

Hivatkozások

[szerkesztés]
  1. Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, University of Edinburgh. 1973. Also in Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569-574.
  2. Krzysztof Apt and Maarten van Emden, Contributions to the Theory of Logic Programming, Journal of the Association for Computing Machinery. Vol, 1982 - portal.acm.org

Külső linkek

[szerkesztés]
  • [1] Definíció a számítástechnika ingyenes on-line szótárából