Математическая логика и теория алгоритмов

q a б в Рис. 3.1 В варианте а видно, что из истинности посылок следует истинность заключения. В вариантах б, в из истинности посылок не следует истинность заключения. § 12. Использование метода резолюций в языке ПРОЛОГ Язык программирования ПРОЛОГ существенно опирается на метод резолюций. Са:мо название ПРОЛОГ есть сокращение, озна­ чающее программирование в терминах логики. Вычисления на ПРОЛОГе можно рассматривать как доказательство теорем с исполь­ зованием метода резолюций и применением дизъюнктов специального вида - хорновских дизъюнктов. Отметим следующую принципиальную отличительную черту языка ПРОЛОГ. В языках программирования, таких как АЛГОЛ, ФОРТРАН, С++, описывается, как решать ту или иную задачу. Программирование на ПРОЛОГе указывает только то, что нужно (необходимо) сделать, т.е. указывается цель, а не процедура решения. Программист долисен дать определение ситуации и формулировать задачу, а система сама решает задачу. При решении задачи использу­ ется метод резолюций. Рассмотрим простейший пример. Пусть задано следующее дерево родственных отношений, изображенное на рис. 3.2. 117