Основные теоремы ограничения на доказательства в формальных системах

Теорема Гёделя о неполноте (1931): Существуют формулы m, такие, что m и ù m не доказуемы.

Теорема Тарского (1935): Во всякой интерпретации формулы m найдутся выражения истинные, но не доказуемые.

Теорема Черча (1936): Не существует алгоритма для того, чтобы отличить теорему от не теоремы, т.е. существуют неразрешимые формальные системы.Неразрешимыми оказались:1) Исчисление предикатов первого порядка.2) Теории групп, колец, тел.

3) Теория вещественных чисел.

Теорема Тьюринга: В 1937 Тьюринг показал, что не существует ни рекурсивной процедуры, ни машины Тьюринга, которая позволяет определить, является или не является данная формула теоремой в заданном языке (формальной системе). Ограничения в равной мере относятся и к вычислительным машинам и к людям.

Алгоритм унификации. Применение теоремы к выражению связано с алгоритмом унификации. Этот алгоритм заключается в последовательной подстановке в выражение заданного множества правил продукции.

Доказать А® М

С точки зрения доказательства необходимо привести гипотезу Н к теореме. При этом во всяком выражении замещением являются свободные переменные. На них не действуют ограничения кванторами $ и ".

ПРИМЕР УНИФИКАЦИИ:Пусть есть гипотеза Н, выражение Е и теорема Т. Идея алгоритма унификации заключается в пересмотре выражения, например с лева на право. Выражение удобно рассматривать в виде дерева. Порядок просмотра носит префиксный порядок. Дерево рассматривается сверху в низ слева на право. x²+(y+ )²

При работе алгоритма просматривается 2 дерева: для выражения Е и для гипотезы Н. Причём пересмотр параллельный Текущие индексы е и h. Для доказательства необходимо совпадение всех символов с текущими индексами е и h.При этом необходимо отсечь те части алгоритма, которые ведут к бесконечным процедурам.

13. Системы понимания естественного языка (ЕЯ).Морфологический анализ.

Необходимость в общении с ЭВМ на естественном языке возникает в:

- диалоговых системах

- экспертных системах при формировании целей поиска и в процессе диалога

- создание запросов в Базах Данных

- системах автоматизированного перевода иностранных языков

- электронной почте (общение голосом)

- формирование запросов в поисковых системах.

Наличие естественно-языкового интерфейса считается признаком интеллектуальных систем.

Система INTELLECT написана Ларри Хариссом в области финансов. Давала консультации на естественном языке. Система NATURALINK (Харри Тенант) естественный языковой интерфейс к ЭВМ. ELIZA (Джозеф Вейценбаум) Электронный психиатр. ПОЭТ (Эдуард Попов) Естественный языковой интерфейс к промышленным системам. SHRDLU (Терри Виноград) Система понимания естественного языка.

Большинство создателей программ ориентированны на работу с текстом. Есть системы распознавания голоса. При работе с естественным языком задача сводится к анализу и интерпретации на внутренний машинный язык слов и предложений.

Существует два подхода: формальный и неформальный.

Неформальный подход основан не на анализе предложений, а на выявлении типичных строк, которые пользователь вводит формируя запрос.

Возможны 2 стратегии.

1) Основана на ключевых словах, которые выделяют из фразы и являются основой дальнейших действий..

2) Поиск сочетаний слов или шаблонов.

К неформальным методам относятся различные языковые меню, которые применяются в интерфейсах.

Формальные подходы основаны на лингвистическом анализе предложения с использованием формальных и естественно-языковых грамматик. Правила грамматики устанавливают порядок слов в предложениях и способы формирования различных модификаций слов (флексий).

Классификация фраз, которая не зависит от других фраз описывается контекстно-свободной грамматикой.

Анализ связного текста (дискурса) производится при помощи контекстно-зависимой грамматики.

Поиск по сайту: