Математические основы
Преобразовать выражение в соответствии с операциями отрицания
Слова, задающие сущности изучаемого мира
Если для всех xÎM F оценивается как истина, то истиной является ("x)F(x)
Математическая индукция
Рекурсия
Компьютерное задание
Практические задания
Практические задания
Доказательство от противного
Скалемовская нормальная форма
В проверке содержит или не содержит S пустое предложение
По различию используемых символов
Стратегия предпочтения одночленов
Навигация
Скалемовская нормальная форма
Логическое и функциональное программирование
119487
знаков
12
таблиц
22
изображения
4.2.2.2 Скалемовская нормальная форма
Дальнейшее преобразование предполагает полное исключение из формулы кванторов. При этом необходимо сохранить семантику. Это достигается за счет введения скалемовских функций. Для описания этой функции рассмотрим следующий пример: ("x)($y)подсистема(x,y), для каждого x существует y такой, что x его подсистема.
Это означает, что если выделить конкретное x, то для этого x существует y, удовлетворяющее функции подсистема(x, y). Иными словами, y зависит от x, то есть, если задано x, то и существует соответствующее ему y. Отсюда следует, что y можно заменить на функцию f(x), которая задает отношение между x и y. Поскольку f(x) возникло из-за того, что переменная y квантифицирована $, при подстановке функции на место y, квантор $ уже не требуется. Таким образом, исходную логическую формулу можно переписать: ("x) подсистема(x, f(x).
Такая функция называется скалемовской.
Приоритетность действия кванторов, имеющихся в префиксной форме, определяется слева направо. Например: ("x)($y)("z)F(x, y, z) Þ ("x)("z)F(x, f(x), z). А для случая: ("x)("z)($y)F(x, y, z) Þ ("x)("z)F(x, f(x, y), z).
Таким образом, переменной, которая в логической формуле влияет на связанную квантором существования переменную, является любая переменная с квантором общности, которая стоит левее переменной из квантора существования. Если переменная связанная квантором существования является крайней слева, такую формулу можно заменить функцией без аргументов (константой):
($x)("y)подсистема(x, y) =подсистема.
Если проделать эту операцию для примера, получим:
В случае, когда в одной логической формуле имеется более двух связанных квантором существования переменных, то сколемовская функция также будет распадаться на различные функции.
("x)($y)("z)($w)F(x ,y ,z, w) = ("x)("z)F(x, f(x), z, g(x, z)).
Если подобным образом исключить связанные квантором существования переменные, то любые другие переменные будут связаны только квантором общности и не надо пояснять, что преременные связаны этим квантором. Следовательно, квантор общности можно исключить. Для примера получим:
Такое представление и есть сколемовская нормальная форма.
Теперь можем определить алгоритм получения сколемовской формы:
1. Составить список L переменных, связанных квантором общности. Сначала список L пуст.
2. Пусть Ci – рассматриваемое предложение, j – номер использующейся сколемовской функции Sij. Положим j = 1.
3. Удалить кванторы , начиная с самого левого и применяя в зависимости от необходимости правила а или б.
а. Если рассматривается квантор "x, то удалить его и добавить x к списку L.
б. Если рассматривается квантор $x, то удалить его и заменить x во всем предложении Ci термом Sij(x1, …, xk), где x1, …, xk переменные, находящиеся в этот момент в списке L. Увеличить j на 1.
Следующим шагом является переход к конъюнктивной нормальной форме, а затем к клаузальной форме, то есть форме предложений.
Приведение к конъюнктивной нормальной форме осуществляется заменой пока это возможно (AÙB)ÚC на (AÚC)Ù(BÚC). В результате получим выражения вида A1Ù … ÙAn, где Ai имеет вид (
, причем 
есть терм или атомарный предикат или атомарная формула или их отрицание. Целесообразно осуществить и минимизацию по следующим правилам:
Наконец, исключаем связку Ù, заменяя AÙB на две формулы A, B. В результате многократной замены получим множество формул, каждая из которых является предложением. Это и есть клаузальная нормальная форма.
4.2.2.3 Предложения Хорна
Все клаузальные формулы (предложения) представляют собой несколько предикатов, то есть:
Эти формулы в зависимости от k, l классифицируются по нескольким типам.
(1) Тип 1: k = 0, l = 1.
Предложение представляет собой единичный предикат, и оно может быть записано как ®F(t1, t2, …, tm), где t1, t2, …, tm – термы. В случае когда все термы представляют собой константы, они описывают факты, которые соответствуют данным из БД. Если термы содержат переменные, то они задают общезначимые представления, высказываемые для группы фактов. Например, таким представлением является:
® текучесть(x): все течет, все изменяется.
(2) Тип 2: k³1, l = 0.
Этот тип можно записать в виде:
F1ÙF2Ù…ÙFk®.
Обычно используется для описания вопроса. Причина, по которой данный тип предложения представляется вопросом, является то, что ответ на вопрос реализуется в виде процедуры доказательства, однако для этого доказательства используется метод опровержения, при котором создается отрицание вопроса и доказывается, что отрицание не выполняется.
(3) Тип : k³1, l=1.
Этот тип соответствует записи в форме «Если ___, то ____.».
F1ÙF2Ù…ÙFk®G1.
(4) Тип: k=0, l>1.
Этот тип имеет вид:
®G1ÚG2Ú…ÚGl
и используется при представлении информации, содержащей нечеткость. Обычно нечеткость возникает при неполноте информации. В этой формуле появляется неполнота информации в том смысле, что из нее нельзя определить, какой из предикатов G1, …, Gl является истиной.
(5) Тип: k³1, l>1.
Это наиболее общий тип.
В системе предложений Хорна среди всех перечисленных типов предложений допустимы типы предложений 1, 2, 3, а 4, 5 запрещены.
4.2.3Формализация процесса доказательств
Доказательство демонстрирует, что некоторая ППФ является теоремой на заданном множестве аксиом S (то есть результатом логического вывода из аксиом).
Положим, что S есть множество из n ППФ, а именно, A1, A2, …, An, и пусть ППФ, для которой требуется вычислить является ли она теоремой, есть B. В таких случаях можно сказать, что доказательство показывает истинность ППФ вида:
(A1Ù…ÙAn®B) (1)
при любой его интерпретации. Можно сказать по другому: это определение эквивалентно тому, что отрицание формулы:
(2)
не выполняется (ложно) при любой интерпретации.
Поскольку эта формула является ППФ, то ее можно преобразовать к клаузальной форме, используя для этого приведенный выше алгоритм. Пусть преобразованная ППФ есть S.
Основная идея метода, называемого методом резолюции, состоит:
Похожие работы
... программирование [application programming] — разработка и отладка программ для конечных пользователей, например бухгалтерских, обработки текстов и т. п. Системное программирование [system programming] — разработка средств общего программного обеспечения, в том числе операционных систем, вспомогательных программ, пакетов программ общесистемного назначения, например: автоматизированных систем ...
... разработки программ, но и разработку пакетов прикладных программ. Эти разработки должны обеспечивать высокое качество и вестись примерно так же, как и выпуск промышленной продукции. Достижения компьютерной техники 1. Универсальные настольные ПК Что такое настольный компьютер, объяснять никому не надо — это любимое молодежью устройство, чтобы красиво набирать тексты рефератов, а ...
... набор процедур и функций языков программирования Basic и Pascal, позволяют управлять графическим режимом работы экрана, создавать разнооборазные графические изображения и выводить на экран текстовые надписи. ГЛАВА 2. ГРАФИЧЕСКИЕ ВОЗМОЖНОСТИ ЯЗЫКА ПРОГРАММИРОВАНИЯ В КУРСЕ ИНФОРМАТИКИ БАЗОВОЙ ШКОЛЫ (НА ПРИМЕРЕ BASIC И PASCAL) 2.1 Разработка мультимедиа курса «Графические возможности языков ...
... информационных технологий, которое заключается как в совершенствовании методов организации информационных процессов, так и их реализации с помощью конкретных инструментов – сред и языков программирования. Итогом работы можно считать созданную функциональную модель вычисления неэлементарных функций. Данная модель применима к функциям, если она не задана одной формулой посредством конечного числа ...
0 комментариев