| Термини | Номера на текстове, където са въведени |
|---|---|
| n-местен предикат | 3 |
| n-местен функционален символ | 4 |
| n-местна функция | 3 |
| n-местен предикатен символ | 4 |
| SLD-резолвента | 15 |
| SLD-резолюция | 15 |
| анонимна променлива | 5 |
| аргументи | 6 |
| асоциирана редица от субституции | 15 |
| атом | 6 |
| атомарна формула | 6 |
| безкванторна част | 46 |
| безкванторна формула | 35 |
| брой на аргументите | 4 |
| в сила | 14 |
| валиден дизюнкт | 28 |
| валидна | 14 |
| вариант на положителна хорнова клауза | 16 |
| верен | 28, 43 |
| втори случай на явна нерешимост | 18 |
| вярна | 7, 9, 36, 38 |
| генерализация | 35 |
| глава на положителна хорнова клауза | 14 |
| глобална променлива | 5 |
| действа | 18 |
| дизюнкт | 28 |
| дизюнкция на | 35, 40 |
| дистрибутивност на конюнкцията спрямо дизюнкцията и обратно | 44 |
| допустима дума | 2 |
| допустима редица | 32 |
| допълнена основна азбука на Пролог | 2 |
| дясна страна на еквиваленция | 45 |
| еднотипни атомарни формули | 17 |
| еквивалентна, еквивалентни | 44 |
| еквивалентни системи от уравнения между термове | 19 |
| еквиваленция | 45 |
| екзистенциализация | 35 |
| екзистенциална формула | 46 |
| екзистенциално затваряне | 39 |
| елиминация | 33 |
| Ербранов универсум | 24 |
| ербранова структура | 24 |
| ербранова структура, породена от дадена хорнова програма | 25 |
| задача за унификация | 17 |
| заключение | 14, 45 |
| заместване | 10, 47 |
| запитване | 14 |
| затворен дизюнкт | 28 |
| затворен литерал | 28 |
| затворен терм | 9 |
| затворена атомарна формула | 9 |
| затворена положителна хорнова клауза | 16 |
| затворена формула | 38 |
| заявка | 14 |
| знак за дизюнкция | 35 |
| знак за конюнкция | 35 |
| знак за отрицание | 28 |
| идемпотентна субституция | 18 |
| изводима | 25 |
| извършване на резолюция | 30 |
| изпълнена | 7, 9 |
| изпълнима | 7, 39 |
| изпълнимо | 7 |
| изпълнимо множество от затворени дизюнкти | 32 |
| импликация | 45 |
| интерпретация | 4 |
| интерпретиращо съответствие | 4 |
| канонична резолвентна редица | 23 |
| квантор за общност | 35 |
| квантор за съществуване | 35 |
| клаузи на хорнова програма | 14 |
| колизия на променливите | 42 |
| комутативност на конюнкцията и дизюнкцията | 44 |
| константа | 4 |
| конфигурация | 5 |
| конюнкция на | 35, 40 |
| литерал | 28 |
| лява страна на еквиваленция | 45 |
| матрица | 46 |
| метод на резолюцията | 30 |
| минимален ербранов модел за дадена хорнова програма | 25 |
| множество на истинност | 3 |
| модел | 14, 28, 41 |
| модификация на оценка | 5 |
| най-общ унификатор | 21 |
| най-обща SLD-резолвента | 22 |
| най-обща резолвента | 22 |
| най-общо решение на система от уравнения между термове | 18 |
| непосредствена SLD-резолвента | 15 |
| непосредствена резолвента | 15, 30 |
| носител | 4 |
| обедняване | 4 |
| обещаваща редица | 32 |
| обогатяване | 4 |
| оператор за присвояване | 12 |
| операционна семантика на Пролог | 26 |
| основен терм | 9 |
| основна азбука на Пролог | 2 |
| основна формула | 9 |
| отворена формула | 35 |
| отговор | 14 |
| отрицание | 28, 35 |
| отрицателен литерал | 28 |
| отстранима | 26 |
| оценка | 5 |
| положителен литерал | 28 |
| положителна хорнова клауза | 14 |
| правило на хорнова програма | 14 |
| празен дизюнкт | 28 |
| предикат на n променливи | 3 |
| предикатен символ | 4 |
| предпоставка | 14, 45 |
| представя | 43 |
| преименуваща субституция | 16 |
| пренексен вид | 46 |
| пренексна формула | 46 |
| пренексно представима формула | 49 |
| произведение на субституции | 11 |
| променлива | 5 |
| променливи на дизюнкт | 28 |
| променливи на литерал | 28 |
| променливи на положителна хорнова клауза | 16 |
| променливи на терм и на безкванторна формула | 8, 37 |
| променливи на хорново запитване | 14 |
| променливите на система от уравнения между термове | 18 |
| пропадащо хорново запитване | 27 |
| противоположни литерали | 28 |
| прочистване | 33 |
| първи случай на явна нерешимост | 18 |
| разделител | 2 |
| разширение | 4 |
| резолвента | 15, 30 |
| резолвентна редица | 15 |
| резолвентно изводим | 30 |
| резултат от елиминация | 33 |
| резултат от прилагането на субституция | 10, 14, 29, 42 |
| решена относно | 20 |
| решение на уравнение между термове и на система от такива уравнения | 17 |
| свободни променливи | 37 |
| свързани променливи на пренексна формула | 46 |
| се съдържа в | 4 |
| сигнатура | 4 |
| сигнатура | 4 |
| силно допустима дума | 2 |
| система в решен вид | 18 |
| скулемова нормална форма | 50 |
| скулемови функционални символи | 50 |
| следва | 7, 14 |
| стойност на затворена формула | 38 |
| стойност на терм и на формула | 7, 9, 36 |
| стойност на функция и на предикат | 3 |
| структура | 4 |
| субституция | 10 |
| съгласувана | 4 |
| съдържа | 4 |
| тавтологичен дизюнкт | 28 |
| тегло | 20 |
| терм | 6 |
| тривиално излишен дизюнкт | 33 |
| тъждествена система от уравнения между термове | 17 |
| тъждествена субституция | 10 |
| тъждествено вярна | 7 |
| тъждествено вярна формула | 39 |
| тяло на положителна хорнова клауза | 14 |
| удовлетворява | 7, 13, 14, 17 |
| указател за брой на аргументите | 4 |
| умножение на субституции | 11 |
| универсална формула | 46 |
| универсално затваряне | 39 |
| универсум | 4 |
| унификатор | 17 |
| унифицируеми | 17 |
| уравновесена дума | 2 |
| успех на хорново запитване | 27 |
| успяващо хорново запитване | 27 |
| участва | 33 |
| факт на хорнова програма | 14 |
| формули на предикатното смятане | 35 |
| функционален символ | 4 |
| функция на n променливи | 3 |
| хорнова заявка | 14 |
| хорнова програма | 14 |
| хорново запитване | 14 |
| частен случай | 11, 14, 17, 29, 42 |
| членове на конюнкция и на дизюнкция | 35 |
| явно нерешима система от уравнения между термове | 18 |
| явно нерешимо уравнение между термове | 18 |