Pregledni rad
PRINCIP REZOLUCIJE KAO TEORIJSKA OSNOVA JEZIKA UMJETNE INTELIGENCIJE PROLOG
Mirko Čubrilo
; Faculty of Organization and Informatics, University of Zagreb, Varaždin, Croatia
Sažetak
Razvoj matematičke logike i teorije algoritama dao je tokom posljednjih desetljeća i niz rezultata primjenjivosti i ujedno teorijska ograničenja njihovih dometa. Kao jedno od glavnih dostignuća matematičke logike smatramo formulaciju računa predikata prvog reda. U okviru tog formalizma postala je moguća sintaktička i semantička analiza logičkog zaključivanja. Dokazani su strukturni metateoremi poput metateorema kompaktnosti i potpunosti itd. Radovi J. Herbranda pokazali su da je moguća mehanička procedura dokaza kontradiktornosti skupa izjava računa predikata prvog reda, ako je dani skup izjava uistinu kontradiktoran. Princip rezolucije poslužio je kao veoma efektivno pravilo izvoda praznog disjunkta. Razvoj teorije algoritama donio je niz međusobno ekvivalentnih formulacija intuitivnog pojma algoritma i dokaz algoritamske nerješivost računa predikata, što je dalo teorijska ograničenja mogućnosti primjene Herbrandove procedure. Na izloženim teorijskim osnovama izrastao je programski jezik PROLOG. U ovom članku izloženi su svi osnovni teorijski rezultati o računu predikata prvog reda , na kojima se zasniva PROLOG. To su: algoritam prevođenja izjave u standardnu (Skolemovu) formu, Herbrandova procedura, algoritam unifikacije i princip rezolucije. Većina pojmova i rezultata ilustrirana je najprije na primjerima iz računa sudova, a zatim na primjerima iz računa predikata.
Ključne riječi
Hrčak ID:
80361
URI
Datum izdavanja:
11.12.1987.
Posjeta: 1.071 *