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. ^[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ó:

$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 ^[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 $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

↑ 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.
↑ 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

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

[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

[1]

[2]