Cтраница 3
Доказательства невыполнимости логических формул очень важны в ИИ ( гл. Способы таких доказательств, основанные на принципе резолюций, выделяются среди прочих тем, что они дают возможность использовать средства автоматического доказательства, применяемые в логическом программировании ( гл. [31]
Существенный недостаток принципа резолюции заключается в формировании на каждом шаге вывода множества резольвент - новых дизъюнктов, большинство из которых оказываются лишними. В связи с этим предложены различные модификации принципа резолюции, использующие более эффективные стратегии поиска и различного рода ограничения на вид исходных дизъюнктов. [32]
Хотя большинство реализаций метода доказательства теорем выполнено на основе принципа резолюций, здесь мы рассмотрим реализацию этого метода с использованием аналитических таблиц, выполненную Фит-тингом, поскольку в последние годы указанный метод выбран как один из перспективных для доказательства теорем. [33]
Важный прогресс в автоматическом доказательстве теорем был достигнут Цж А. Робинсоном в 1965 г. Он разработал единственное правило вывода - принцип резолюции, которое оказалось черезвычайно эффективным и легкодоступным для реализации на ЭВМ С тех пор было предложено много усовершенствований принципа резолюции. Автоматическое доказательство теорем прилагалось во многих областях таких, как анализ программ, дедуктивные системы ответов на волросы, системы решения задач и технология роботов. [34]
В настоящее время известно огромное множество различных версий алгоритмов унификации. Ниже мы рассмотрим алгоритм унификации, введенный Робинсоном, для принципа резолюции, поскольку именно этот алгоритм выбран Фиттингом для реализации метода автоматического доказательства теорем на основе аналитических таблиц. [35]
Множество дизъюнктов S невыполнимо тогда и только тогда, когда существует вывод принципом резолюции из S пустого дизъюнкта. [36]
Ненамного эффективнее был метод Девиса и Патнема, с помощью которого были доказаны некоторые теоремы из логики предикатов первого порядка, не доказанные Гилмором. В 1964 - 1965 гг. независимо друг от друга появились обратный метод установления выводимости Маслова и принцип резолюции Робинсона. [37]
Способ обхода дерева, используемый для отыскания всех деревьев опровержения цели, зависит от реализации и не определяется принципом резолюции. Большинство систем используют поиск сначала вглубь. Аналогично условия остановки являются также системно-зависимыми. Некоторые системы, такие, как интерпретаторы Пролога, не используют каких-либо условий остановки вообще. В таких системах отсутствуют гарантии полноты; вопросы полноты и завершения решаются программистом. [38]
Важный прогресс в автоматическом доказательстве теорем был достигнут Цж А. Робинсоном в 1965 г. Он разработал единственное правило вывода - принцип резолюции, которое оказалось черезвычайно эффективным и легкодоступным для реализации на ЭВМ С тех пор было предложено много усовершенствований принципа резолюции. Автоматическое доказательство теорем прилагалось во многих областях таких, как анализ программ, дедуктивные системы ответов на волросы, системы решения задач и технология роботов. [39]
Привлекательность дизъюнктной формы с точки зрения автоматизации вывода состоит в том. Это правило, называемое принципом резолюции, впервые было применено Робинсоном. Принцип резолюции включает сравнение левой части одного дизъюнкта А с правой частью другого дизъюнкта В. Когда мы производим сравнение, осуществляется подстановка переменных, чтобы сделать атомы идентичными. [40]
Принцип резолюции является более эффективной процедурой, нежели процедура вывода Эрбрана. Но и он страдает существенными недостатками, заключающимися в формировании всевозможных резольвент, большинство из которых оказывается ненужными. Многочисленные модификации принципа резолюции направлены на нахождение более эффективных стратегий поиска нужных дизъюнктов. Желающие могут обратиться к комментарию в конце книги, где перечислена литература, описывающая эти модификации. [41]
Существенное продвижение в этом направлении предпринял Грин [11], продемонстрировавший в качестве генератора планов законченную систему доказательства теорем методом резолюции. Согласно этому подходу, начальная ситуация, целевая ситуация и результаты применения имеющихся операторов описываются в виде множества аксиом исчисления предикатов первого порядка. Далее с помощью принципа резолюции доказывается предположение, что существует ситуация, удовлетворяющая описанию цели. Побочным результатом успешно проведенного доказательства является план последовательного преобразования начальной ситуации в целевую. [42]
Принцип резолюции или вариации этого принципа используются во многих системах по автоматическому доказательству теорем или для нахождения доказательства или проведения вывода. Отметим только, что хотя принцип резолюции очень простой, его практическое применение во многом зависит от того, каким образом уменьшить пространство перебора, когда мы пытаемся провести сравнение. Мы также отметим, что принцип резолюции тесно связан с графическим сравнением. Фактически мы можем представить предложение ( или дизъюнкты) с помощью ( модифицированной) семантической сети и провести логические выводы путем применения принципа резолюции к семантической сети. [43]
В общем случае каждый шаг процедуры логического вывода на основе ПР состоит в нахождении двух дизъюнктов, один из которых содержит литеру, а другой - ее отрицание. На основании этого сравнения формируется новый дизъюнкт, называемый / езо / - вентой. Порождение новых дизъюнктов, или резольвент, является основой принципа резолюции. Пара литер, состоящая из некоторой литеры и отрицания этой литеры, называется контрарной, ими дополнительной, парой. Операция поиска и исключения контрарных, или дополнительных, пар литер называется операцией резолюции. [44]
Кратко обсуждены возможности и приложения автоматического доказательства теорем. Указаны некоторые трудности приложений и возможные направления дальнейших исследований. Во второй части работы детально описана конкретная универсальная система доказательства теорем, основанная не на принципе резолюции. [45]