Методы представления знаний Формальные языки и формальные системы



страница9/17
Дата15.01.2013
Размер1.11 Mb.
ТипЛекции
1   ...   5   6   7   8   9   10   11   12   ...   17

Универсум Эрбрана


Всякая модель есть пара , где - множество, - семейство отношений. Эту модель обычно называют универсумом.



Пусть задано некоторое множество формул . В этом множестве имеется некоторое множество констант (они встречаются в формулах ).



;

- множество функциональных символов на уровне i.
Пример.

Пусть дано - константы, - функциональный символ.






Объединение всех этих множеств называется универсумом Эрбрана:

(У Лорьера: ).

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

Теорема Эрбрана

Множество предложений невыполнимо тогда и только тогда, когда существует конечное множество подформул этого множества , невыполнимое на универсуме Эрбрана.

Теорема о резолюции

Пусть  (1),
где
- предложения; 1 удовлетворяет тем же условиям, что и . Тогда формула такова, что ( выводима из ).
Фактически это означает, что из выражения и выражения выводимо выражение . Это выражение называется резольвентой выражений gif" align=bottom> и , а выражения и называются родительскими дизъюнктами. получается как бы вычеркиванием контрарных пар и соединением дизъюнкцией оставшихся литералов.
Чтобы воспользоваться методом резолюций, надо формулу привести к виду (1). Для этого существуют специальные алгоритмы, рассмотренные ниже.
Но сначала рассмотрим примеры.

Пример 1

Пусть  (2)
Надо доказать, что эта формула невыполнима. Для этого надо найти родительские формулы и резольвенты. Найдя контрарные пары, будем иметь: , что и доказывает противоречивость формулы.

Имеем:

  • резольвируем дизъюнкты и . Получаем (вычеркнули контрарную пару )

  • резольвируем . Резольвента: .

  • дизъюнкт дает пустой дизъюнкт.


Таким образом, получили противоречие, то есть формула (2) невыполнима (или противоречива с точки зрения синтаксического вывода). Доказав невыполнимость исходной формулы, доказали выполнимость формулы (2)
, что означает , то есть доказали, что , то есть доказали выводимость из . Из истинности следует невыполнение 2.
Пример 2

Докажем корректность правила modus ponens (правило отделения):

Воспользуемся теоремой дедукции: если имеется формула, выводимая из другого множества формул, то формула является теоремой.
Докажем, что эта теорема доказуема в логике исчисления предикатов первого порядка. Преобразуем это выражение к дизъюнктивной нормальной форме2.





- проверяем ее невыполнимость:

Рассмотрим . Резольвента: .

дает нам пустой дизъюнкт.

Следовательно, формула невыполнима. То есть формула выводима, то есть является теоремой.
Этот алгоритм удобен для машинной реализации.

В последнем примере мы проделали некоторые преобразования, чтобы ее привести к нужному виду , где не содержат .
Для приведения формул к такому виду существуют специальные алгоритмы. Рассмотрим один из них.
1   ...   5   6   7   8   9   10   11   12   ...   17

Похожие:

Методы представления знаний Формальные языки и формальные системы iconРабочая программа дисциплины теория автоматов и формальных языков направление подготовки
Уметь: строить формальные грамматики, деревья вывода, распознающие автоматы; анализировать формальные языки
Методы представления знаний Формальные языки и формальные системы icon4. Введение в формальные (аксиоматические) системы 1 Формальные модели
Принципы построения формальных теорий. Аксиоматические системы, формальный вывод
Методы представления знаний Формальные языки и формальные системы iconЛекция 3 Исчисления. Формальные системы. Формальные грамматики. Автоматы
...
Методы представления знаний Формальные языки и формальные системы iconЛекция 4 Исчисления. Формальные системы. Формальные грамматики. Автоматы
...
Методы представления знаний Формальные языки и формальные системы icon1. Понятие информации. Виды информации. Роль информации в живой природе и в жизни людей. Язык как способ представления информации: естественные и формальные языки
Понятие информации. Виды информации. Роль информации в живой природе и в жизни людей. Язык как способ представления информации: естественные...
Методы представления знаний Формальные языки и формальные системы iconКодирование информации
Представление информации. Язык как способ представления информации: естественные и формальные языки. Дискретная форма представления...
Методы представления знаний Формальные языки и формальные системы iconБилет 1 Понятие информации. Виды информации. Роль информации и живой природе и в жизни людей. Язык как способ представления информации: естественные и формальные языки. Основные информационные процессы: хранение
Понятие информации. Виды информации. Роль информации и живой природе и в жизни людей. Язык как способ представления информации: естественные...
Методы представления знаний Формальные языки и формальные системы iconБилет 1 Понятие информации. Виды информации. Роль информации и живой природе и в жизни людей. Язык как способ представления информации: естественные и формальные языки. Основные информационные процессы: хранение
Понятие информации. Виды информации. Роль информации и живой природе и в жизни людей. Язык как способ представления информации: естественные...
Методы представления знаний Формальные языки и формальные системы iconЭкзаменационные билеты по информатике 9 класс
Понятие информации. Виды информации. Язык как способ представления информации. Естественные и формальные языки. Основные информационные...
Методы представления знаний Формальные языки и формальные системы iconФормальные модели программных агентов в задаче семантического индексирования документов
В работе рассматриваются формальные модели делиберативных агентов, т е агентов базирующихся на базируется на принципах и методах...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org