Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 114
Текст из файла (страница 114)
]броме того, програмлш Агиа позволила найти ответ на многие открытые вопросы в нескольких областях математики [1621]. Программа автоматического доказательства теорем Бойера — Мура [165] применялась и дорабатывалась в течение многих лет, и ею воспользовался Натараджан Шанкар для получения первого полностью строгого формального доказательства теоремы Геделя о неполноте [!393].
Одним из самых строгих средств автоматического доказательства теорем является программа Огеег; она использовалась для решения некоторых открытых задач в области комбипаторной логики. Наиболее известные из них касаются 'ж алгебры Роббинса. В 1933 году Герберт Роббинс предложил простое множество аксиом, которые, на первый взгляд, могли служить для определения булевой алгебры, но ни одного доказательства этой гипотезы найти не удавалось (несмотря на напряженную работу нескольких выдающихся математиков, включая самого Альфреда Тарского). Наконец, 1О октября 1996 года после восьми дней вычислений программа БОР [одна из версий программы Огсег) нашла такое доказательство (1019].
Средства автоматического доказательства теорем могут также применяться для решения задач, связанных с Ъ. проверкой и 'дх синтезом как аппаратных, так и программных средств, поскольку для обеих этих проблемных областей могут быть предусмотрены правильные варианты аксиоматизации. Поэтому исследования доказательства теорем проводятся не только в искусственном интеллекте, но и в таких областях, как проектирование аппаратных средств, языки программирования и разработка программного обеспечения.
В случае программного обеспечения аксиомы определяют свойства каждого синтаксического элемента языка программирования. (Процесс формирования рассуждений о программах полностью аналогичен процессу формирования рассуждений о действиях в ситуационном исчислении.) Программный алгоритм проверяется путем демонстрации того, что его выходы соответствуют спецификациям для всех входов. Таким образом были проверены алго- Часть 1П. Знания и рассуждения ритм шифрования ВЯА с открытым ключом и алгоритм согласования строк Бойера— Мура [166].
В случае аппаратного обеспечения аксиомы описывают способы взаимодействия сигналов и элементов схемы (один из примеров приведен в главе 8). Программой Апта [!610] был проверен проект 16-битового сумматора. Системы формирования логических рассуждений, предназначенные специально для проверки аппаратных средств, оказались способными проверять целые процессоры, включая свойства синхронизации этих процессоров [1455]. Формальный синтез алгоритмов был одним из первых направлений использования средств автоматического доказательства теорем, как и было намечено Корпеллом Грином [591], который опирался на идеи, высказанные ранее Саймоном [1416].
Обший замысел состоит в том, что должна быть доказана теорема с утверждением, что "существует программа р, удовлетворяющая некоторой спецификации*'. Если удается ограничить это доказательство конструктивной формой, то появляется возможность извлечь из результатов доказательства требуемую программу. Хотя полностью автоматизированный Ж дедуктивный синтез, как стало называться это направление, еще не осуществим применительно к программированию задач обшего назначения, дедуктивный синтез, управляемый вручную, оказался успешным при проектировании нескольких новейших и сложнейших алгоритмов. Кроме того, активной областью исследования является синтез программ специального назначения.
В области синтеза аппаратных средств программа автоматического доказательства теорем Апта применялась для проектирования схем, оказавшихся более компактными по сравнению с разработанными во всех предыдуших проектах [1609]. Для многих проектов логических схем достаточно применить пропозициональную логику, поскольку множество интересующих высказываний является фиксированным благодаря конечным размерам множества схемных элементов. В наши дни применение пропозиционального логического вывода в аппаратном синтезе является стандартным методом, имеющим много крупномасштабных областей использования (см., например, работу Новика и др.
[1149]). Те же методы теперь начинают также применяться для проверки программного обеспечения с помощью таких систем, как программа проверки моделей Брш [672]. Например, с ее помощью была проверена до и после полета программа управления космическим аппаратом Кешоге Аяепг [633]. 9.6. РЕЗЮМЕ В этой главе приведен анализ логического вывода в логике первого порядка и многих алгоритмов его выполнения. ° В первом подходе используется правило логического вывода для конкретизации кванторов в целях преобразования задачи логического вывода в форму пропозициональной логики. Как правило, этот подход характеризуется очень низким быстродействием.
° Использование унификации для выявления подходящих подстановок для переменных позволяет устранить этап конкретизации в доказательствах первого порядка, в результате чего этот процесс становится гораздо более эффективным. 429 Глава 9. Логический вывод в логике первого порядка ° В поднятой версии правила отделения унификация применяется для получения естественного и мощного правила логического вывода — обобщенного правила отделения.
В алгоритмах прямого логического вывода и обратного логического вывода это правило применяется к множествам определенных выражений. ° Обобщенное правило отделения является полным применительно к определенным выражениям, но проблема логического следствия остается полуразрешимой. Для программ Оа1а!оя, состояших из определенных выражений без функций, проблема логического следствия разрешима. ° Прямой логический вьнод используется в дедуктивных базах данных, где он может сочетаться с реляционными операциями баз данных. Он также применяется в продукционных системах, которые обеспечивают эффективное обновление при наличии очень больших наборов правил. ° Прямой логический вывод для программ Оага!оа является полным и выполняется за время, определяемое полиномиальной зависимостью.
° Обратный логический вывод используется в системах логического программирования, таких как Рго!оя, в которых реализована сложная технология компиляции для обеспечения очень быстрого логического вывода. ° Недостатками обратного логического вывода являются излишние этапы логического вывода и бесконечные циклы; эти недостатки можно устранить путем запоминания. ° Обобщенное правило логического вывода на основе резолюции позволяет создать полную систему доказательства для логики первого порядка с использованием баз знаний в коньюнктивной нормальной форме. ° Сушествует несколько стратегий сокрашения пространства поиска д и систем с резолюцией без потери полноты.
Эффективные средства автоматического доказательства теорем на основе резолюции использовались для доказательства интересных математических теорем, а также для проверки и синтеза программных и аппаратных средств. БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕТКИ Логический вывод широко исследовался древнегреческими математиками. Аристотель тщательно исследовал один из типов логического вывода, называемый Ъ. силлогизмом, который представляет собой своего рода правило логического вывода. Силлогизмы Аристотеля включали элементы логики первого порядка, такие как кван- торы, но были ограничены унарными предикатами. Силлогизмы классифицировались по "фигурам" и "модусам", в зависимости от порядка термов (которые следовало бы назвать предикатами) в высказываниях и от степени обшности (которую теперь принято интерпретировать с помошью кванторов), применяемой к каждому терму, а также с учетом того, является ли каждый терм отрицаемым.
Наиболее фундаментальным силлогизмом является тот, который относится к первой фигуре первого модуса: Все 5 суть М. Все М суть Р. Следовательно, все Я суть Р. 430 Часть !1!. Знания и рассуждения Аристотель пытался доказать истинность других силлогизмов, "приводя" их к силлогизмам первой фигуры. Описание того, в чем должно состоять такое "приведение", оказалось гораздо менее точным по сравнению с описанием, в котором были охарактеризованы сами фигуры и модусы силлогизмов.
Готтлоб Фреге, который разработал полную логику первого порядка в 1879 году, основал свою систему логического вывода на большой коллекции логически правильных схем и единственном правиле логического вывода — правиле отделения (Модна Ропепз). Фреге воспользовался тем фактом, что результат применения любого правила логического вывода в форме "Из р вывести 0" можно моделировать путем применения к высказыванию Р правила отделения наряду с логически правильной схемой Р ~ Д. Такой "аксиоматическии'* стиль представления знаний, в котором наряду с правилом отделения использовался целый ряд логически правильных схем, был принят на вооружение после Фреге многими логиками; наиболее замечательным является то, что этот стиль использовался в основополагаюшей книге Рппс0ла МаГйетаГГса [1584].
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
