Автоматическое доказательство - теорема
Cтраница 1
Автоматическое доказательство теорем способно сейчас внести реальный вклад в исследования в различных областях. С использованием доказывающей программы были решены открытые проблемы в математике и в формальной логике. Но этим не исчерпываются возможные приложения. Есть реальные свидетельства практического использования таких программ, и успех в области проектирования схем и обнаружения отказов - один из примеров тому. [1]
Автоматическое доказательство теорем ведет свое начало от основополагающих работ Эрбрана, который еще в 30 - х годах XX в. В 60 - е годы усилиями Ньюэлла и Саймона был создан общий решатель проблем, доказывающий теоремы формальной логики, разработанной Расселом и Уайтхедом, которые считали, что для математики достаточно иметь формальный вывод теорем из основных аксиом. [2]
По поводу автоматического доказательства теорем часто задают один и тот же вопрос: когда, наконец, программы будут доказывать новые теоремы. Вопрос этот естественен и вполне осмыслен. Само название области вызывает соответствующий образ. К счастью, сейчас мы можем сказать: программы могут получать новые результаты и уже получили их достаточно много. [3]
При разработке методов автоматического доказательства теорем необходимо представить все формулы, как логики высказываний, так и логики предикатов первого порядка, в некотором стандартном виде. [4]
Важный прогресс в автоматическом доказательстве теорем был достигнут Цж А. Робинсоном в 1965 г. Он разработал единственное правило вывода - принцип резолюции, которое оказалось черезвычайно эффективным и легкодоступным для реализации на ЭВМ С тех пор было предложено много усовершенствований принципа резолюции. Автоматическое доказательство теорем прилагалось во многих областях таких, как анализ программ, дедуктивные системы ответов на волросы, системы решения задач и технология роботов. [5]
Очевидно, что программы автоматического доказательства теорем не всегда принимают оптимальные решения на различных этапах процесса доказательства. Для эффективного решения задач во многих случаях требуется дополнительная информация об исходном множестве дизъюнктов. Нами была сделана попытка создания мощной процедуры дедуктивного вывода, не требующей дополнительной информации для решения поставленной задачи. Для этого процедура дедуктивного вывода на графе связей была распараллелена. Кроме того, были разработаны эвристические функции оценки связи. [6]
В экспертных системах и автоматическом доказательстве теорем - способ рассуждений, при котором для доказательства истинности утверждения делается попытка доказать истинность утверждений, из которых оно непосредственно следует; процесс продолжается до тех пор, пока рассуждение не дойдет до известных фактов или не будет получено утверждение, для вывода которого нет правил. [7]
Конечно, доминирующий в автоматическом доказательстве теорем метод резолюции не является панацеей от всех бед, сопровождающих процедуры доказательства теорем, и мы вправе надеяться на появление более совершенных процедур дедуктивного вывода. Это касается и языка Пролог, неплохо зарекомендовавшего себя при решении логических проблем. Здесь можно согласиться с точкой зрения Н. Н. Непейводы, утверждавшего, что есть смысл использовать Пролог для кусков программ, обладающих исключительно сложной логикой при явном задании вариантов. [8]
Кратко обсуждены возможности и приложения автоматического доказательства теорем. Указаны некоторые трудности приложений и возможные направления дальнейших исследований. Во второй части работы детально описана конкретная универсальная система доказательства теорем, основанная не на принципе резолюции. [9]
 |
Программа, управляемая образцами, для автоматического доказательства теорем. [10] |
Программа, управляемая образцами, для автоматического доказательства теорем запускается при помощи цели пуск. Таким образом, для того чтобы дбказать при помощи этой программы некоторую теорему, мы транслируем ее отрицание в конъюнктивную нормальную форму, а затем запускаем революционный процесс. [11]
В этой главе даны основные положения автоматического доказательства теорем, наиболее развитой области искусственного интеллекта. [12]
Помимо потенциального вклада в расширение математического знания автоматическое доказательство теорем считалось также важным для тех аспектов искусственного интеллекта, которые связаны с обработкой знаний при помощи логического вывода. Здесь автоматическое доказательство теорем успешно применялось для выполнения таких заданий, как ответы на вопросы, игры, решение задач в пространстве состояний. [13]
Среди аргументов в пользу важности работ по автоматическому доказательству теорем для искусственного интеллекта приводятся и такие: вычислительные машины наделяются способностью выполнять формальные математические построения ( посредством логики), и соответствующие методы ( доказательства теорем) представляют интерес с точки зрения организации процессов мышления у роботов. Мы считаем, что методы, разработанные в этой области, как, впрочем, и любые методы, которые могут быть созданы на основе принятой в ней в настоящее время методологии ( столь удачно определяемой как вычислительная логика), бесполезны для обоих этих направлений, хотя в настоящей статье мы рассматриваем в основном второе. Мышление роботов составляет основу нашей концепции искусственного интеллекта - и как будто не должно быть сомнений что знание, как построить машину, способную рассуждать о реальном мире и действовать в нем, а также разговаривать о себе на естественном языке, необходимо ( но не достаточно. [14]
 |
Таблицы истинности основных логических операций. [15] |
Страницы: 1 2 3 4