Студопедия

КАТЕГОРИИ:


Архитектура-(3434)Астрономия-(809)Биология-(7483)Биотехнологии-(1457)Военное дело-(14632)Высокие технологии-(1363)География-(913)Геология-(1438)Государство-(451)Демография-(1065)Дом-(47672)Журналистика и СМИ-(912)Изобретательство-(14524)Иностранные языки-(4268)Информатика-(17799)Искусство-(1338)История-(13644)Компьютеры-(11121)Косметика-(55)Кулинария-(373)Культура-(8427)Лингвистика-(374)Литература-(1642)Маркетинг-(23702)Математика-(16968)Машиностроение-(1700)Медицина-(12668)Менеджмент-(24684)Механика-(15423)Науковедение-(506)Образование-(11852)Охрана труда-(3308)Педагогика-(5571)Полиграфия-(1312)Политика-(7869)Право-(5454)Приборостроение-(1369)Программирование-(2801)Производство-(97182)Промышленность-(8706)Психология-(18388)Религия-(3217)Связь-(10668)Сельское хозяйство-(299)Социология-(6455)Спорт-(42831)Строительство-(4793)Торговля-(5050)Транспорт-(2929)Туризм-(1568)Физика-(3942)Философия-(17015)Финансы-(26596)Химия-(22929)Экология-(12095)Экономика-(9961)Электроника-(8441)Электротехника-(4623)Энергетика-(12629)Юриспруденция-(1492)Ядерная техника-(1748)

Постановка задачи. Тема 4. Автоматическое доказательство теорем

Тема 4. Автоматическое доказательство теорем

Автоматическое доказательство теорем – это основа логического программирования. Классическим методом АТД является метод резолюции.

Алгоритм, который проверяет отношение для формулы S, множества формул Г и теории называется алгоритмом автоматического доказательства теорем (АТД).

В общем случае такой алгоритм невозможен, т. е. не существует алгоритма, который для любых S, Г и выдавал бы ответ «ДА», если Г |- S и «НЕТ» в противном случае. Но в некоторых случаях можно построить алгоритм, который применим не ко всем формулам теории (т. е. частичный алгоритм). Для некоторых простых формальных теорий (например, теории высказываний) алгоритмы АТД известны.

Пример. Для исчисления высказываний известно, что теоремами являются тавтологии, т. е. можно проверить является ли формула тавтологией с помощью таблиц истинности. Этот пример является примером доказательства теорем в теории £, но не является алгоритмом автоматического поиска вывода теорем из аксиоматической теории £.

Наиболее известный классический алгоритм АТД называется методом резолюций (МР). Для любого прикладного исчисления предикатов 1 порядка он дает ответ «ДА», если Г |- S и «НЕТ» или не выдает ответа в противном случае.

<== предыдущая лекция | следующая лекция ==>
Приведенная форма представления предикатов | Доказательство от противного
Поделиться с друзьями:


Дата добавления: 2014-01-15; Просмотров: 263; Нарушение авторских прав?; Мы поможем в написании вашей работы!


Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет



studopedia.su - Студопедия (2013 - 2024) год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав! Последнее добавление




Генерация страницы за: 0.013 сек.