1.1.Основни понятия от предикатното смятане от първи ред
1.2.Клаузна форма
1.3.Метод на резолюцията
1.4.Преход към езика Пролог
ПРЕХОД КЪМ ЕЗИКА ПРОЛОГ Методът на резолюцията гарантира изводимост на празната клауза, ако дадено множество от формули е неудовлетворимо. Този метод определя начина за намиране на резолвентата на две клаузи, но не фиксира реда, в който клаузите се комбинират за подреждане на резолвента, нито реда, в който литералите се разглеждат като кандидати за унификация. Ако броят на клаузите в началното множество от клаузи е голям, броят на резолвентите, получени от тях, също може да бъде голям. Освен това всяка резолвента става пълноправен участник в следващите стъпки на резолюцията. Това води до допълнително увеличаване на броя на възможните комбинации на клаузите за получаване на резолвенти. Голяма част от създаваните резолвенти могат да бъдат без значение за доказателството. Стига се до изпълнение на излишни стъпки, които могат да забавят и даже да направят неосъществим извода на празната клауза. Прилагането на метода на резолюцията доведе до създаване на различни стратегии за извод, а също и до налагане на редица ограничения върху началното множество от клаузи. Синтактични ограничения а) Разглеждат се клаузи от специален вид, наречени клаузи на Хорн. Те съдържат най-много един положителен литерал. Пример: Следните клаузи: човек(петър). човек(Х):-човек(Y),майка(X,Y). ?-майка(вера,Х). са клаузи на Хорн. Това ограничение опростява процеса на унификация. Клаузите на Хорн не намаляват изразителната сила на клаузната форма. Произволна клауза може да се преобразува в клауза на Хорн като се преименуват предикатите й. Пример: В клаузата с_интелект(Х);неграмотен(Х):-човек(Х). положителният литерал неграмотен(Х) може да се изрази чрез отрицателния литерал ~грамотен(Х). Тогава тази клауза може да се запише във вид на клауза на Хорн: с_интелект(Х):-човек(Х),грамотен(Х). б)Разглеждат се само такива множества от клаузи на Хорн, в които всички клаузи с изключение на една се именувани. Дефиниция: Клауза на Хорн, която има положителен литерал се нарича именувана. Неименуваната клауза се интерпретира като целева формула, а именуваните - като предпоставки. Езикът Пролог може да се разглежда като система за доказателство на теореми, ограничена върху такива множества от клаузи на Хорн, в които всички клаузи, с изключение на една са именувани. Именуваните клаузи образуват пролог-програмата. Клаузите без дясна част се наричат факти. Именуваните клаузи с дясна част се наричат правила. Неименуваната клауза ?-А1,А2,...,An. се нарича въпрос (цел или целева клауза). Семантични ограничения а) Семантиката на езика Пролог се основава на т.нар. входна линейна резолюция Започва се с целевата клауза и се прави опит да се намери резолвентата й с някоя от началните клаузи. Ако опитът е успешен, прави се опит изведената клауза да се резолвира с някоя от началните. На следващата стъпка отново се прави опит току-що изведената клауза да се резолвира с накоя от началните и т.н. Така на всяка стъпка се резолвира клаузата, изведена на предишната стъпка, с една от началните клаузи. Входната линейна резолюция не допуска резолвиране на две клаузи, принадлежащи на началното множество, или на две клаузи, изведени в предишните етапи. Изведената резолвента съответства на предстоящата за удовлетворяване цел. б) Входната линейна резолюция се ограничава до селективна линейна резолюция (SL-резолюция) SL-резолюцията е линейна резолюция, допълнена с правила за селекция на литерали от целта за унификация. Редът, в който литералите от текущата цел се опитват да се унифицират, е строго определен - започва се винаги с първия литерал. Пример: Нека имаме клаузата сестра_на(Х,Y):-жена(Х),дете_на(X,Z,W),дете_на(Y,Z,W). и целта сестра_на(U,иван),сестра_ на(U,V). И двата литерала сестра_на(U,иван) и сестра_ на(U,V) допускат унификация с главата на клаузата сестра_на(Х,Y). В Пролог винаги се избира първия литерал. Така резолвентата им има вида ?-жена(U),дете_на(U,Z,W),дете_на(иван,Z,W),сестра_на(U,V). и става нова цел. в) Търсене в длбочина Възможно е целта да може да се резолвира с повече от една клауза на програмата. В Пролог е избрана стратегията търсене в дълбочина за селекция на клаузите. При тази стратегия за всяка цел се избира първата клауза от множеството от клаузи, с която тя може да се резолвира. Към следващата възможна клауза се преминава, когато направеният избор за останалите цели не води до успех. Освен тази стратегия има и стратегия за търсене в ширина. При нея се намират всички възможни клаузи, които могат да се резолвират с текущата. В резултат се получава не една, а множество от резолвенти, всяка от които се разглежда като цел. Стратегията търсене в ширина има предимство, че ако съществува решение, то непременно ще бъде намерено. Стратегията търсене в дълбочина позволява дадена цел да попадне в цикъл, недопускащ останалите алтернативи да бъдат изследвани. Този недостатък се компенсира от простотата на нейната реализация на конвенционалните компютри и по-ограничените изисквания към необходимата за работата й памет. Освен тези ограничения има и ограничения, и различия при унификацията в метода на резолюцията и съпоставянето в езика Пролог, които не са съществени.
