Логическое программирование Экспертный анализ

Еще в конце 1970-х годов стала отчетливо просматриваться тенденция к использованию в исследованиях в области искусственного интеллекта "формальных" методов, т.е. основанных на аппарате математической логики.

  • Под автоматическим формированием суждений (automated reasoning) понимается поведение некоторой компьютерной программы, которая строит логический вывод на основании определенных законов. Так, нельзя отнести к классу программ автоматического формирования суждений программу, которая моделирует подбрасывание монетки, чтобы определить, следует ли одна формула из набора других.
  • Ниже приведены все синтаксические правила, которые используются для конструирования правильно построенных формул (ППФ) в исчислении высказываний.
  • Для этого нужно анализировать пропозициональные символы в форме предикатов и аргументов, кванторов и квантифщированных переменных. Логика предикатов предоставляет нам набор синтаксических правил, позволяющих выполнить такой анализ, набор семантических правил, с помощью которых интерпретируются эти выражения, и теорию доказательств, которая позволяет вывести правильные формулы, используя синтаксические правила дедукции.
  • PROLOG — это не совсем обычный язык программирования, в котором программа состоит в основном из логических формул, а процесс выполнения программы представляет собой доказательство теоремы определенного вида. В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" (см. [Kowalski, 1979, р. 88-89]). Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций
  • Мощность резолюции обеспечивается тем, что в ней суммируется множество других правил. Это станет очевидно после того, как обычные правила будут представлены в конъюнктивной нормальной форме.
  • Резолюция представляет собой правило вывода, с помощью которого можно вывести новую ППФ (правильно построенную формулу) из старой. Однако в приведенном выше описании логической системы ничего не говорилось о том, как выполнить доказательство. В этом разделе мы обратим основное внимание на стратегические аспекты доказательства теорем. Проверить, может ли функция быть действительной частью некоторой аналитической функции , если да – восстановить ее, при условии . Справочный материал и примеры к выполнению контрольной работы по математике
  • Система PLANNER моделировала состояние некоторой области рассуждений в терминах ассоциативной базы данных, которая содержала как утверждения, так и теоремы, функционирующие как процедуры. Утверждения представляли собой списки типа "предикат-аргумент", подобные тем, что используются в LISP
  • Также было показано, что если записать это выражение таким образом, чтобы слева от оператора ":-" стоял единственный позитивный литерал, а справа — негативные литералы, то получится выражение, представляющее фразу Хорна в синтаксисе языка логического программирования PROLOG:
  • В языке PROLOG такое упорядочение называется правилом поиска слева направо.
  • Определенные факты (основные атомы — ground atoms) нужно разместить в базе данных раньше, чем правила, которые в качестве цели имеют соответствующие предикаты. Таким образом будут минимизированы издержки обращения к правилам. Например, утверждение
  • Имеет ли смысл выразить следующие цитаты с помощью логики предикатов?
  • Решение типовых задач по математике и физике