Математическая логика и автоматическое доказательство теорем, Чень Ч., Ли Р., 1983

Математическая логика и автоматическое доказательство теорем, Чень Ч., Ли Р., 1983.

   Книга посвящена детальному изложению всего круга проблем, связанных с так называемым методом резолюций. Этот метод наиболее известен и широко используется в современных работах по доказательству на ЭВМ математических теорем и вообще при построении систем «искусственного интеллекта». Описываются применения метода к таким, например, актуальным для всякого системного программиста задачам, как автоматический анализ и синтез программ В приложении описаны другие методы и некоторые результаты последних лет, знакомство с которыми необходимо при изучении проблематики автоматического доказательства теорем.




Искусственный интеллект, математическая логика и доказательство теорем.
После появления первых современных вычислительных машин машинная технология стала развиваться с фантастической скоростью. Сегодня мы видим, что машины используются не только для решения трудных вычислительных проблем таких, как выполнение быстрого преобразования Фурье или обращение матриц, высокого порядка. От них требуют выполнения и таких задач, которые были бы названы интеллектуальными, если бы их делали люди. Примерами таких задач являются программирование, создание систем, отвечающих на вопросы, и доказательство теорем. Искусственный интеллект — это область вычислительной математики, которая занимается такими задачами (Эрнст и Ньюэл [1]; Фейгенбаум и Фельдман [ 1]; Нильсон (1 ]; Слэйгл [1]).

Вторая половина 60-х годов в области искусственного интеллекта выделялась особым увеличением интереса к машинному доказательству теорем. Широкое распространение и интенсивность этого интереса вызываются не только растущим сознанием, что умение делать логические выводы есть неотъемлемая часть человеческого интеллекта, но, возможно, в большей степени являются следствием того статуса, который приобрела техника машинного доказательства теорем в конце 60-х годов. Основы машинного доказательства теорем были заложены Эрбраном в 1930 г. Его метод был неосуществим практически до изобретения электронных вычислительных машин. Только после основополагающей статьи Дж. А. Робинсона в 1965 г. и развития метода резолюций были сделаны важные шаги к созданию программ, реализующих доказательство теорем). После 1965 г. были предложены многочисленные усовершенствования метода резолюций.

Оглавление.
От редактора перевода.
Предисловие.
Глава 1 Введение.
§1.1. Искусственный интеллект, математическая логика и доказательство теорем.
§1.2. Математические основы.
Литература.
Глава 2 Логика высказываний.
§2.1. Введение.
§2.2. Интерпретация формул логики высказываний.
§2.3. Общезначимость и противоречивость в логике высказываний.
§2.4. Нормальные формы в логике высказываний.
§2.5. Логические следствия.
§2.6. Применения логики высказываний.
Литература.
Упражнения.
Глава 3 Логика первого порядка.
§3.1. Введение.
§3.2. Интерпретации формул в логике первого порядка.
§3.3. Предваренные нормальные формы в логике первого порядка.
§3.4. Приложения логики первого порядка.
Литература.
Упражнения.
Глава 4 Теорема Эрбрана.
§4.1 Введение.
§4.2. Скулемовские стандартные формы.
§4.3. Эрбрановский универсум множества дизъюнктов.
§4.4. Семантические деревья.
§4.5. Теорема Эрбрана.
§4.6. Применение теоремы Эрбрана.
Литература.
Упражнения.
Глава 5 Метод резолюций.
§5.1. Введение.
§5.2. Метод резолюций для логики высказываний.
§5.3. Подстановка и унификация.
§5 4. Алгоритм унификации.
§5.5. Метод резолюций для логики первого порядка.
§5.6. Полнота метода резолюций.
§5.7. Примеры использования метода резолюций.
§5.8. Стратегия вычеркивания.
Литература.
Упражнения.
Глава 6 Семантическая резолюция и лок-резолюция.
§6.1. Введение.
§6.2. Неформальное введение в семантическую резолюцию.
§6.3. Формальные определения и примеры семантической резолюции.
§6.4 Полнота семантической резолюции.
§6.5. Гиперрезолюция и стратегия поддержки — частные случаи семантической резолюции.
§6.6. Семантическая резолюция с использованием упорядоченных дизъюнктов.
§6.7. Реализация семантической резолюции.
§6.8. Лок-резолюция.
§6.9. Полнота лок-резолюции.
Литература.
Упражнения.
Глава 7 Линейная резолюция.
§7.1. Введение.
§7 2 Линейная резолюция.
§7.3. Входная резолюция и единичная резолюция.
§7.4. Линейная резолюция, использующая упорядоченные дизъюнкты и информацию об отрезанных литерах.
§7 5 Полнота линейной резолюции.
§7.6. Линейный вывод и поиск в дереве.
§7.7. Эвристики поиска в дереве.
§7.8. Оценки для оценочных функций.
Литература.
Упражнения.
Глава 8 Резолюция с равенством.
§8.1. Введение.
§8.2. Невыполнимость в специальных классах моделей.
§8.3. Парамодуляция — правило вывода для равенства.
§8 4. Гиперпарамодуляция.
§8.5. Входная и единичная парамодуляции.
§8.6. Линейная парамодуляция.
Литература.
Упражнения.
Глава 9 Некоторые процедуры доказательства, основанные на теореме Эрбрана.
§9.1. Введение.
§9.2. Процедура Правица.
§9.3. Процедура V-резолюции.
§9.4. Псевдосемантические деревья.
§9.5. Процедура порождения замкнутых псевдосемантических деревьев.
§9.6. Обобщение правила расщепления, введенного Девисом и Патнемом.
Литература.
Упражнения.
Глава 10 Анализ программ.
§10.1. Введение.
§10.2. Неформальное обсуждение.
§10.3. Формальное определение программ.
§10.4 Логические формулы, описывающие исполнение программы.
§10 5. Анализ программ с помощью резолюции.
§10 6. Завершение работы и реакция программ.
§10.7. Стратегия поддержки и вывод стоп-дизъюнкта.
§10.8. Правильность и эквивалентность программ.
§10.9. Специализация программ.
Литература.
Упражнения.
Глава 11 Дедуктивный поиск ответов на вопросы, решение задач н синтез программ.
§11.1. Введение.
§11.2. Вопросы класса А.
§11.3. Вопросы класса В.
§11.4. Вопросы класса С.
§11.5. Вопросы класса D.
§11.6. Полнота резолюции для получения ответов на вопросы.
§11.7. Принципы синтеза программ.
§118. Примитивная резолюция и алгоритм А* (алгоритм синтеза программ).
§11.9. Правильность алгоритма А*.
§11.10. Применение аксиом индукции к синтезу программ.
§11.11. Алгоритм А (усовершенствованный алгоритм синтеза программ).
Литература.
Упражнения.
Глава 12 Заключительные замечания.
Литература.
Приложения.
Приложение А.
§A.1. Программа для ЭВМ, использующая единичную бинарную резолюцию.
§А.2. Краткий комментарий к программе.
§А.3. Текст программы.
§А.4. Иллюстрации.
Литература.
Приложение В. Доказательство леммы 82.
Дополнение Поиск вывода и автоматизация доказательств.
A.Теория поиска вывода и обратный метод. С.Ю. Маслов, Г.Е. Минц.
§1. Введение.
§2. Исчисления и задача поиска вывода.
§3. Идея метапеременных в локальных методах поиска вывода.
§4. Одна переформулировка обратного метода.
§5 Разрешимость формул вида (3x) М.
Литература.
Б. Алгоритм Британского музея может быть эффективнее метода резолюций В.П. Оревков.
B. О стратегиях метода резолюций и клаш-метода. С.Ю. Маслов.
Библиография.
Часть I.
Часть II.
Часть III.
Алфавитный указатель.



Бесплатно скачать электронную книгу в удобном формате, смотреть и читать:
Скачать книгу Математическая логика и автоматическое доказательство теорем, Чень Ч., Ли Р., 1983 - fileskachat.com, быстрое и бесплатное скачивание.

Скачать pdf
Ниже можно купить эту книгу по лучшей цене со скидкой с доставкой по всей России.Купить эту книгу


Скачать - pdf - Яндекс.Диск.




Теги: учебник по математике :: математика :: Чень :: Ли