1626434760-4c9f92f9ed5188f8fc024fed893742bb (844133), страница 2
Текст из файла (страница 2)
Fr=Т.В частности, всякая аксиома является теоремой.Использование исчисления предикатов для представления знанийбудет эффективным в том случае, если существует средство дляавтоматического доказательства теорем.15Формальные системыФормальные системы всегда представляют собой модель какой-тореальности (либо конкретной, либо математической).Интерпретация представляет собой распространение исходныхположений формальной системы на реальный мир.Интерпретация придает смысл каждому символу ФС иустанавливает взаимно однозначное соответствие междусимволами ФС и реальными объектами. Теоремы ФС, будучиоднажды интерпретированы, становятся после этогоутверждениями в обычном смысле слова, и в этом случае ужеможно делать выводы об их истинности или ложности.Если некоторая формула истинна при всех интерпретациях, то ееназывают общезначимой. Если формула содержит кванторы,общезначимость или ее отсутствие не всегда можно установить.Если некоторое множество формул не удовлетворяется ни прикакой интерпретации, то оно называется противоречивым (илиневыполнимым).16Формальные системыПервый вопрос, возникающий при задании формальной системы,состоит в том, чтобы определить, является данная формулаобщезначимой или нет, и как это доказать.В математике предполагается, что при задании формальнойсистемы существует хорошо определенный способ действий,который за конечное число шагов позволит получить ответ наданный вопрос.
Такой способ, если он существует, называетсяпроцедурой решения, а соответствующую формальную системуназывают разрешимой. Однако основная трудность заключается втом, что такие процедуры существуют далеко не всегдадаже для таких простых теорий, как исчисление предикатовпервого порядка.17Формальные системыВ 1930 г. Ж.Эрбран предложил метод доказательства теорем вформальных системах первого порядка, идея которого состоит вследующем: чтобы получить некоторое заключение C исходя изгипотез H1, H2,,..,Hn, т.е.
чтобы доказать теоремуT: H1 ∧ H2 ∧ ... ∧ Hn → C,достаточно доказать противоречивость формулыF: H1 ∧ H2 ∧ ... ∧ Hn ∧ ¬ C,в которой отрицание заключения добавлено к гипотезам.Такое доказательство может быть существенно проще прямоговывода.Был разработан метод доказательства теорем, базирующийся наописанной выше идее, который получил название метод резолюций.Кроме того, было доказано, что этот метод является исчерпывающимметодом доказательства теорем.Это значит, что если формула противоречива, то с помощью метода18резолюции всегда можно обнаружить это противоречие.Метод резолюций в логике высказыванийПонятие резольвенты.Рассмотрим следующие дизъюнкты (предложения)C1: PC2: ¬ P∨ QТогда C3: Q есть резольвента дизъюнктов C1 и C2 , полученнаякак дизъюнкция C1∨ C2 ,из которой вычеркнуты контрарныепары (P и ¬ P).Примеры.1) P∨ R¬ P∨ Q-------------R∨ Q2) ¬ P∨ Q∨ R¬ Q∨ S---------------¬ P∨ R∨ S3) ¬ P∨ Q¬ P∨ R---------------нет резольвенты19Метод резолюций в логике высказыванийТеорема.Пусть даны два дизъюнкта C1 и C2 .
Тогда резольвента Cдизъюнктов C1 и C2 есть логическое следствие C1 и C2.Определение (резолютивного вывода).Пусть S – множество дизъюнктов. Резолютивный вывод C из S естьтакая конечная последовательность дизъюнктов C1, C2, … Ck ,что каждый Ci либо принадлежит S, либо является резольвентойдизъюнктов, предшествующих Ci , и C= Ck .Вывод ∅ из S называется опровержением (доказательствомневыполнимости) S .Говорят, что C выводимо из S , если существует вывод C из S .20Метод резолюций в логике высказыванийПример.S = {¬ P∨ Q , ¬ Q , P }Дизъюнкты ¬ P∨ Q и ¬ Q дают ¬ P ,а P и ¬ P дают ∅ .Значит множество S невыполнимо (противоречиво) .21Использование метода резолюций длядоказательства теоремДоказательство ведется методом опровержения (от противного).Пусть даны 4 утверждения:(1) P → S(2) S → U(3) P(4) UДокажем путем опровержения, что U – логическое следствие (1), (2)и (3).Возьмем U с отрицанием и получим следующее множествоутверждений:22Использование метода резолюций длядоказательства теорем(1) P → S(2) S → U(3) P(4) ¬ U<преобразуем встандартную форму>(1) ¬ P ∨ S(2) ¬ S ∨ U(3) P(4) ¬ UДалее получим следующий резолютивный вывод:(1) ¬ P ∨ S(2) ¬ S ∨ U(3) P(4) ¬ U(5) S(резольвента (3) и (1) )(6) U(резольвента (5) и (2) )(7) ∅(резольвента (6) и (4) )23Использование метода резолюций длядоказательства теорем в логике 1-го порядкаПри доказательстве теорем в логике 1-го порядка необходимоиспользовать преобразование формулы в нормальную форму иподстановку (унификацию) переменных.Пример.Дано:(1) (∀x)( Человек(x) → Смертен(x) )(2) Человек(Сократ)Доказать:(3) Смертен(Сократ)Доказательство:(1) ¬Человек(x) ∨ Смертен(x)(2) Человек(Сократ)(3) ¬ Смертен(Сократ)Выполним подстановку θ = { x/Сократ)24Использование метода резолюций длядоказательства теорем в логике 1-го порядкаВыполнив подстановку θ = { x/Сократ), получим(1) ¬Человек(Сократ) ∨ Смертен(Сократ)(2) Человек(Сократ)(3) ¬ Смертен(Сократ)Далее получаем следующую последовательность резольвент:(4) Смертен(Сократ)(из (1) и (2) )(5) ∅ – противоречие(из (4) и (3) )25Использование метода резолюций длядоказательства теорем в логике 1-го порядкаДля того чтобы применить метод резолюции к произвольномумножеству формул, требуется представить эти формулы вспециальном удобном виде – в виде предложений.Любую правильно построенную формулу (п.п.ф.) исчисленияпредикатов можно представить в виде предложений, применяя кней следующую последовательность операций:1.
Исключение знаков импликации.Здесь используется подстановка:¬ A ∨ B вместо A → B, которая применяется столько раз, скольконеобходимо.26Использование метода резолюций длядоказательства теорем в логике 1-го порядка2. Уменьшение области действия знаков отрицания.Необходимо, чтобы знак отрицания (¬) применялся не более чем кодному предикатному символу.Для этого применяются следующие подстановки:¬ A∨ ¬ B вместо ¬(A ∧ B)¬ A ∧ ¬ B вместо ¬(A ∨ B)Aвместо ¬ ¬ A( ∃ x){ ¬ A} вместо ¬ (∀ x)A(∀ x){ ¬ A} вместо ¬ (∃ x)A27Использование метода резолюций длядоказательства теорем в логике 1-го порядка3.
Стандартизация переменных.В области действия любого квантора переменную, связываемую им,можно заменить другой переменной, и это не приведет кизменению значения истинности п.п.ф.Стандартизация переменных означает их переименование, с темчтобы каждый квантор имел свою собственную переменную.Так, вместо(∀ x) {P(x) → (∀ x) Q(x)}.следует написать(∀ x) {P(x) → (∀ y) Q(y)}.28Использование метода резолюций длядоказательства теорем в логике 1-го порядка4. Исключение кванторов существования.Рассмотрим п.п.ф.
(∀ y∃ x) {P(x,y)},которую можно интерпретировать следующим образом: «Для всехy существует такой x (возможно, зависящий от y), что x большеy».Пусть эта зависимость определяется явно с помощью некоторойфункции g(y), отображающей каждое значение y в x, который«существует».Такая функция называется функцией Сколема.Если вместо x, который «существует», взять функцию Сколема, томожно исключить квантор существования: (∀ y) {P(g(y),y)}.Функциональные буквы для функций Сколема должны быть«новыми», т.е.
не должны совпадать с теми буквами, которые29уже имеются в п.п.ф.Использование метода резолюций длядоказательства теорем в логике 1-го порядкаЗаметим, что при исключении кванторов существования переменные,которые не связаны никакими кванторами всеобщности,заменяются 0-местными функциями Сколема (т.е. константнымисимволами).Если в предыдущей п.п.ф. поменять местами кванторы, то получимформулу (∃ x∀ y) {P(x,y)},здесь переменная x связана только квантором существования,поэтому она может быть заменена на константу a:(∀ y) {P(a,y)}.30Использование метода резолюций длядоказательства теорем в логике 1-го порядка5.
Приведение к предваренной нормальной форме.Теперь можно перенести все кванторы всеобщности в начало п.п.ф.и считать областью действия каждого квантора всю частьп.п.ф., расположенную за ним.Про полученную в результате п.п.ф. говорят, что она имеетпредваренную нормальную форму.Предваренная нормальная форма для имеет вид(∀ x∀ y∀ z){ F(x,y,z)…}.31Использование метода резолюций длядоказательства теорем в логике 1-го порядка6. Приведение к конъюнктивной нормальной форме.Пользуясь законом дистрибутивности операций конъюнкции идизъюнкции, любую формулу можно представить в видеконъюнкции конечного множества дизъюнкций предикатов и(или) их отрицаний.Говорят, что такая формула имеет конъюнктивную нормальнуюформу:(∀ x∀ y∀ z){F1(x,y,z) ∧ F2(x,y,z) ∧ ... }.32Использование метода резолюций длядоказательства теорем в логике 1-го порядка7.
Исключение кванторов всеобщности.Так как все переменные, оставшиеся на данном этапе, относятся ккванторам всеобщности и порядок расположения кванторовнесуществен, то можно эти кванторы явным образом неуказывать.Теперь п.п.ф. имеет видF1(x,y,z) ∧ F2(x,y,z) ∧ ...33Использование метода резолюций длядоказательства теорем в логике 1-го порядка8. Исключение связок «и».Теперь можно исключить знак ∧ , заменяя А ∧ B двумя п.п.ф. A, B.Результатом многократной замены будет конечное множествоп.п.ф., каждая из которых представляет собой дизъюнкциюпредикатных символов или их отрицаний. (Такие формулыназывают предложениями.)Покажем теперь на примерах, как можно эффективно использоватьметод резолюции для доказательства теорем.34Использование метода резолюций длядоказательства теорем в логике 1-го порядкаПример 1.Посылка: Студенты суть граждане.Заключение: Голоса студентов суть голоса граждан.Пусть S(x), C(x) и V(x,y) означают «x - студент», «x - гражданин» и «xесть голос y» соответственно.Тогда посылка и заключение запишутся следующим образом:(∀ y){S(y) → C(y)}(посылка),(∀ x){(∃ y){S(y) ∧ V(x,y)} → (∃ z){C(z) ∧ V(x,z)}}(заключение).Преобразуя посылку в предложение, мы получим:¬ S(y)∨ C(y)(п.1),Далее, отрицая заключение, мы получим:¬ {(∀ x){(∃ y){S(y) ∧ V(x,y)} → (∃ z){C(z) ∧ V(x,z)}}} =35Использование метода резолюций длядоказательства теорем в логике 1-го порядка¬ {(∀ x){(∃ y){S(y) ∧ V(x,y)} → (∃ z){C(z) ∧ V(x,z)}}}= ¬ {(∀ x){(∀ y){¬ S(y) ∨ ¬ V(x,y)} ∨ (∃ z){C(z) ∧ V(x,z)}}}===(∃ x)(∃ y) {{S(y) ∧ V(x,y)} ∧ (∀ z){¬ C(z) ∨ ¬ V(x,z)}}==(∃ x)(∃ y)(∀ z) {{S(y) ∧ V(x,y)} ∧ {¬ C(z) ∨ ¬ V(x,z)}}== {{S(b) ∧ V(a,b)} ∧ {¬ C(z) ∨ ¬ V(a,z)}}.«Рассыпая» полученную формулу на предложения, получим:S(b)(п.2)V(a,b)(п.3)¬ C(z) ∨ ¬ V(a,z)(п.4)36Использование метода резолюций длядоказательства теорем в логике 1-го порядкаИтак, мы получили следующее множество дизъюнктов¬ S(y)∨ C(y)(п.1)S(b)(п.2)V(a,b)(п.3)¬ C(z) ∨ ¬ V(a,z)(п.4)Доказательство методом резолюций выглядит следующим образом:C(b)(п.5),из (п.1) и (п.2)¬ V(a,b)(п.6)из (п.5) и (п.4)∅(п.7),из (п.6) и (п.3)37Использование метода резолюций длядоказательства теорем в логике 1-го порядкаПример 2.Пусть верны посылки:1) Живые люди мыслят; 2) Иван – человек.3) Иван – живой.Используя метод резолюции, докажите, что Иван мыслит.Доказательство.Пусть Human(x), Alive(x) и Think(x) означают «x - человек», «x живой» и «x мыслит» соответственно.Тогда посылка и заключение запишутся следующим образом:Посылка: (∀ x){Human(x) ∧ Alive(x) → Think(x)} ∧ Human(Иван) ∧Alive(Иван)Заключение: Think(Иван)38Использование метода резолюций длядоказательства теорем в логике 1-го порядкаПреобразуя посылку{¬ Human(x) ∨ ¬ Alive(x) ∨ Think(x)} ∧ Human(Иван) ∧ Alive(Иван)получим три предложения :¬ Human(x) ∨ ¬ Alive(x) ∨ Think(x)Human(Иван)Alive(Иван)Отрицая заключение, мы получим:¬ Think(Иван)(п.1),(п.2),(п.3),(п.4).Далее резолютивный вывод дает следующий результат:¬ Alive(Иван) ∨ Think(Иван)(п.5) из п.1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
