Szerkesztő:Bbr98/SLD rezolúció

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

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

$\neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}$

kiválasztott literállal $\neg L_{i}$ és egy meghatározott input klózzal :

$L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}$

akinek a pozitív literálja (atom) $L\,$ egyesül az atommal $L_{i}\,$ a kiválasztott literálból $\neg L_{i}\,$, 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 $\theta \,$ alkalmazzák:

$(\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta$

A legegyszerűbb esetben, a propozíciós logikában az atomok $L_{i}\,$ és $L\,$ azonosak, és az egyesítő helyettesítés $\theta \,$ ü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

Az "SLD-felbontás" nevet Maarten van Emden adta a Robert Kowalski által bevezetett meg nem nevezett következtetési szabályra. 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ó:

$C_{1},C_{2},\cdots ,C_{l}$

ahol a "top klóz" $C_{1}\,$ egy input klóz, és minden más klóz $C_{i+1}\,$ olyan rezolvens, akinek egyik szülője az előző klóz $C_{i}\,$ . A bizonyítás cáfolat, ha az utolsó klóz $C_{l}\,$ 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

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

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:

$q\lor \neg p$

$p\,$

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

$\neg q$

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

$\neg q,\neg p,{\mathit {false}}$

ahol a ${\mathit {false}}\,$ 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.

SLDNF

Az SLDNF 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 $not(p)\,$-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 $p\,$ mint felső klóz. A kiválasztott részcél $not(p)\,$ akkor sikerül, ha az alellenálló meghiúsul, és akkor is, ha az alellenálló sikerül.

Lásd még

• John Alan Robinson

Hivatkozások

• Jean Gallier, az SLD-felbontás és a logikai programozás 9. fejezete: A logika a számítástechnikához: Az automatikus tétel bizonyításának alapjai, 2003-as online változat (ingyenesen letölthető), eredetileg Wiley, 1986
• John C. Shepherdson, SLDNF-Resolution with Equality, Journal of Automated Reasoning 8: 297-306, 1992; meghatározza azt a szemantikát, amely tekintetében az SLDNF egyenlőségű felbontása szilárd és teljes

Külső linkek

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