Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Введение нелогических операторов обусловлено тем, что вычисления в чистом ПРОЛОГе требуют порой больших затрат времени. Обращаясь к реаль­ ному ПРОЛОГу, мы можем улучшить быстродействие и эффективность про­ граммы ценой отказа от обш,ей теоремы полноты. Коренное отличие логики предикатов от ПРОЛОГ а, как чистого, так и ре­ ального, проявляется в обраш,ении их с данными фактами и правилами (форму­ лами). Для логики предикатов не важен порядок их записи, ибо конъюнкция коммутативна. ПРОЛОГ упорядочивает данные в порядке их записи в про­ грамме. И даже порядок записи предикатов в теле правил сохраняется таким, как в записи программы. При этом время выполнения может суш,ественно раз­ личаться в зависимости от этого упорядочения. Если программа содержит правила вида: А:-А или А :-Bi,B2, (3.36) то обращение с запросом «? - А.» порождает, ввиду рекурсивного опреде­ ления А, бесконечный цикл, из которого программа сама по себе выйти не в со­ стоянии. Большинство случаев зацикливания ПРОЛОГ-программ возникает в связи с наличием в них данных вида (3.36). Реальный ПРОЛОГ, независимо от того, полон он или нет, получил широ­ кое распространение и является наиболее эффективным языком логического программирования. А что касается контроля правильности программы, - так это всегда было и остается уделом программистов и пользователей. Вопросы и темы для самопроверки 1. Определение логического следствия из данной пропозициональной фор­ мы (формулы логики высказываний). 2. Свойства логического следования. 3. Логическое следствие из множества формул логики высказываний. 4. Проблема дедукции логики высказываний. Решение проблемы дедукции с использованием противоречивости специальной формулы. 5. Литералы, контрарные литералы, дизъюнкты. 6. Бинарные резольвенты дизъюнктов логики высказываний. 7. Теорема о полноте метода резолюций. 8. Метод резолюций в логике высказываний. 9. Метод насыщения уровня. 10. Стратегии вычёркивания. 11. Лок-резолюция. Теорема о полноте метода лок-резолюций. Зависит ли результат лок-резолюции от изменения индексов литералов? 12. Метод резолюций для хорновских дизъюнктов. 13. Определение логического следствия для формул логики предикатов. 91