Автоматическое доказательство - теорема
Cтраница 2
Гипотезы часто называют теоремами, отсюда и термин автоматическое доказательство теорем. Встречая этот термин, студенты путаются, полагая, что должно происходить автоматическое порождение некого нового аналитического доказательства. На самом деле подразумевается обыкновенный рекурсивный логический вывод, чаще всего при помощи резолюций. Результатом такого вывода являются Да или Нет в зависимости от того, удалось ли за разумное число шагов получить верное равенство или пустую формулу. [16]
Главной темой нашего обсуждения является, приложение методов автоматического доказательства теорем к различным классам задач, рассматриваемых в рамках искусственного интеллекта, особенно задачам, связанным с организацией мышления роботов. И именно в этой области становятся особенно очевидны недостатки узкого исчисления предикатов. [17]
Логическое программирование возникло главным образом благодаря успехам в автоматическом доказательстве теорем, в частности благодаря разработке принципа резолюции. [18]
Дедуктивные выводы в настоящее время хорошо изучены, и автоматическое доказательство теорем является старейшей ветвью искусственного интеллекта. Конечно, формальные, синтаксические методы дедуктивного вывода не способны обрабатывать сложные прикладные области с большим пространством поиска нужной информации. Необходимо разрабатывать эвристические методы управления таким поиском, применять ad hoc стратегии, которые использует человек при решении различных проблем. Таким образом, на первый план выдвигаются рассуждения здравого смысла, рассуждения, оперирующие с неполной, противоречивой, неточной, неопределенной информацией, где главную роль играет правдоподобный вывод. Но прежде чем переходить к основным методам правдоподобного вывода - абдукции и индукции, необходимо остановиться на основных особенностях данных и знаний, применяемых в интеллектуальных системах различного назначения. [19]
 |
Связь системы ПРИЗ с ОС ЕС. [20] |
ПРИЗ автоматический синтез программ, позволяющий использовать ее для автоматического доказательства теорем. [21]
Но этими же двумя свойствами обладает и программа для автоматического доказательства теорем и поэтому ее следует рассматривать с тех же позиций. Наличие первого качества неудивительно и проявляется в том, что обычно приходится затратить много труда на подготовительную работу. Наличие второго качества значительно интересней. Как видно из предыдущих разделов, программа использовалась для решения большого числа открытых проблем, причем использовалась в качестве помощника, а не просто как логический вычислитель. [22]
Эти языки возникли на основе многолетних исследований в области автоматического доказательства теорем и систем вопрос - ответ По сравнению с PLANNERoM они обладают большей степенью формализации. [23]
Итак, все более очевидно, что к программе для автоматического доказательства теорем можно относиться как к коллеге. [24]
Далее мы приведем теоретические положения, на которых базируется метод автоматического доказательства теорем на основе аналитических таблиц для логики предикатов 1-го порядка. Отметим, что вышеописанный алгоритм унификации играет в этом методе ключевую роль. [25]
Принцип резолюции или вариации этого принципа используются во многих системах по автоматическому доказательству теорем или для нахождения доказательства или проведения вывода. Отметим только, что хотя принцип резолюции очень простой, его практическое применение во многом зависит от того, каким образом уменьшить пространство перебора, когда мы пытаемся провести сравнение. Мы также отметим, что принцип резолюции тесно связан с графическим сравнением. Фактически мы можем представить предложение ( или дизъюнкты) с помощью ( модифицированной) семантической сети и провести логические выводы путем применения принципа резолюции к семантической сети. [26]
Главное, что нужно вынести из всего сказанного выше, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и. PROLOG, является системой опровержения резолюций. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается. [27]
Так как Робинсон специально выступает на нашем конгрессе с обзором, посвященным автоматическому доказательству теорем, мне не следует касаться этого материала. Однако несколько вопросов заслуживают упоминания, а ряд замечаний представляется уместным. [28]
Основная цель настоящей работы состоит в том, чтобы продемонстрировать возможность использования программы автоматического доказательства теорем в качестве интеллектуального партнера. [29]
Наша цель - написать книгу, содержащую введение в математическую логику и подробное обсуждение автоматического доказательства теорем и его приложений Книга состоит из трех основных частей. Главы 2 и 3 составляют введение в символическую логику, главы 4 - 9 вводят несколько методов, применяемых в автоматическом доказательстве теорем, а главы 10 и 11 показывают, как доказательство теорем можно применить в таких различных областях, как ответы на вопросы, решение задач, анализ программ и синтез программ. [30]
Страницы: 1 2 3 4