Intellektual tizimlar

1.1.2. Teoreticheskiye prinsipы prologa. PROLOG yavlyayetsya yazыkom ischisleniya predikatov. Predikat – eto logicheskaya formula ot odnogo ili neskolkix argumentov. Mojno skazat, chto predikat – eto funksiya, otobrajayuщaya mnojestvo proizvolnoy prirodы v mnojestvo {lojno, istinno}.
Oboznachayutsya predikatы F(x), F(x, y), F(x, y, z) i t. d..
Odnomestnыy predikat F(x), opredelennыy na predmetnoy oblasti M, yavlyayetsya istinnыm, yesli u obyekta x yest svoystvo F, i lojnыm – yesli etogo svoystva net.
Dvuxmestnыy predikat F(x, y) yavlyayetsya istinnыm, yesli obyektы x i y naxodyatsya v otnoshenii F.
Mnogomestnыy predikat F(x₁ , x₂ , x₃ ,..., x_N ) zadayet otnosheniye mejdu elementami x₁, x₂, ..., x_N i interpretiruyetsya kak oboznacheniye vыskazыvaniya: “Elementы x₁, x₂, x_N naxodyatsya mejdu soboy v otnoshenii F”.
Pri razrabotke logicheskix programm predikatы poluchayut obыchno nazvaniya, sootvetstvuyuщiye semantike opisыvayemoy predmetnoy oblasti.
Primerы predikatov:
xiщnik (X)
suprugi (X,Y)
fio (X,Y,Z)
Predikatы, kotorыye nelzya razbit na otdelnыye komponentы, nazыvayut atomarnыmi. Slojnыye formulы stroyatsya putem kombinirovaniya atomarnыx predikatov logicheskimi soyedinitelyami I, ILI i NE.
Odnomestnыy predikat pri podstanovke v nego znacheniya peremennoy stanovitsya «nulmestnыm», t.ye. vыskazыvaniyem-predlojeniyem, kotoroye yavlyayetsya istinnыm ili lojnыm:
xiщnik (tigr).
Pri podstanovke v n-mestnыy predikat konkretnogo znacheniya yego mestnost stanovitsya ravnoy n–1. Takim obrazom, kajdoye vыskazыvaniye porojdayetsya nekotorыm predikatom, a kajdыy predikat sootvetstvuyet mnojestvu vыskazыvaniy.
Zadacha PROLOG – programmы zaklyuchayetsya v tom, chtobы dokazat, yavlyayetsya li zadannoye selevoye utverjdeniye sledstviyem iz imeyuщixsya faktov i pravil.
Reshayemaya zadacha predstavlyayetsya v vide sovokupnosti utverjdeniy (aksiom), sel zadachi takje zapisыvayetsya v vide utverjdeniya. Togda resheniye zadachi predstavlyayet soboy vыyasneniye logicheskogo sledovaniya iz aksiom
(A₁  A₂  A₃  ... A_n )→ V.
Na praktike udobno ispolzovat dokazatelstvo ot protivnogo, t. ye. dokazыvat nevыpolnimost. Yesli istinno, to lojno i lojno.
Na etom osnovan prinsip rezolyusii, kotorыy trebuyet predstavleniya formul ischisleniya predikatov v vide nabora diz’yunktov, svyazannыx operasiyey kon’yunksii [kon’yunktivnaya normalnaya forma (KNF)].
Pravilo rezolyusii imeyet vid

Pravilo rezolyusii pozvolyayet soyedinit dve formulы, iz odnoy udaliv A, a iz drugoy . V etom sluchaye govoryat, chto A i rezolviruyut.
Glavnaya ideya metoda rezolyusii zaklyuchayetsya v proverke togo, soderjit li mnojestvo diz’yunktov R pustoy (lojnыy) diz’yunkt. Pri polojitelnom otvete formula, sootvetstvuyuщaya R, nevыpolnima i sootvetstvuyuщyeye utverjdeniye protivorechivo. Takim obrazom, dokazav nevыpolnimost formulы

mojno sdelat vыvod, chto V istinno.
Rassmotrim primer ispolzovaniya metoda rezolyusii, primenyaya dokazatelstvo ot protivnogo.
Pust neobxodimo dokazat istinnost vыrajeniya

Dlya ispolzovaniya metoda rezolyusii nujno rassmotret kon’yunksiyu sovokupnosti posыlok i otrisaniya zaklyucheniya v kon’yuktivnoy normalnoy forme. Dlya etogo vыpolnyayetsya ryad shagov:
1. Privodim posыlki k normalnoy forme (bez → i ↔)

2. Zapisыvayem v normalnoy forme otrisaniye zaklyucheniya

3. Rassmatrivayem kon’yunksiyu pyati diz’yunktov

Pervыye dva diz’yunkta dayut , chto v sochetanii s tretim diz’yunktom dayet Q. Chetvertыy i pyatыy diz’yunktы dayut .
Takim obrazom, imeyem

Takim obrazom, dokazano

poskolku protivopolojnoye neverno.
Lyubuyu programmu na PROLOGe mojno rassmatrivat kak bazu dannыx. Mexanizm obrabotki zaprosov v PROLOGe nazыvayetsya unifikasiyey. Posle togo kak polzovatel vvodit zapros, interpretator pristupayet k analizu soderjimogo bazы dannыx, vыpolnyaya dopustimыye podstanovki faktov v selevoye utverjdeniye, chtobы obosnovat yego istinnost.