🗊Презентация Логическое следствие и метод резолюций

Логическое следствие Пусть А и В пропозициональные формы (формулы логики высказываний). Считается, что В логически следует из А, если для каждой совокупности значений пропозициональных букв, при которых А=1 форма В тоже принимает значение 1. В этом случае записывается и читается: «из А логически следует В» или «В является логическим следствием из А». Легко доказать следующую теорему: Теорема: Если и , то . Запись в логике высказываний означает, что А является тавтологией (общезначимой). Имеет место следующая теорема: Теорема: тогда и только тогда, когда .

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

Теоремы проблемы дедукции Теорема: Для произвольных формул логики высказываний , имеют место соотношения: , для любого i, 1≤ i≤ m. Теорема: Если формула является противоречием, тогда В является логическим следствием из , т.е.: . (3.5)

Следствия для заданного множества формул Для заданного множества формул А1, А2,…,Аm, m≥1, строим их конъюнкцию: С=А1&А2&…&Аm. Для С находим с.к.н.ф.: С= D1&D2&…&Dk, здесь Di, 1≤i≤k, элементарные суммы (дизъюнкты). Теперь по показанной выше теореме получаем, что каждый дизъюнкт Di, 1≤ i≤ k, а также их конъюнкции являются следствиями из А1, А2,…,Аm, m≥1, т. е. имеем: А1, А2,…,Аm╞ Di для любого i, 1≤ i≤ k; А1, А2,…,Аm╞ Ds1& Ds2&...& Dsr, для любого r, 1≤ r≤ k и любых s1, s2,…,sr, 1≤ s1, s2,…,sr ≤ k.

Резольвента дизъюнктов логики высказываний Пропозициональные буквы с отрицанием либо без отрицания, входящую в элементарную сумму (дизъюнкт), называют литералами (литерами) логики высказываний. Литеры L и называются контрарными. Так, например, в дизъюнктах и литеры P и контрарные. Также контрарные литеры Q и . Пусть для двух дизъюнктов D1 и D2 существует литера L1 в D1, которая контрарна литере L2 в D2. Вычеркнув L1 и L2 из D1 и D2 соответственно, построим дизъюнкцию оставшихся частей D1 и D2. Полученный таким образом дизъюнкт называется (бинарной) резольвентой D1 и D2, который часто обозначают через R.

Примеры резольвент 1. Пусть D1=P∨Q, , тогда R=Q∨T. 2. Пусть D1=P, (D2~P⇒Q), тогда R=Q, иначе из P и P⇒Q получаем Q. 3. Пусть (D1=P⇒Q), (D2=Q⇒T), тогда (R=P⇒T). Иначе из P⇒Q и Q⇒T получаем P⇒T Теорема: Пусть для дизъюнктов D1 и D2 существует резольвента R. Тогда R есть логическое следствие из D1 и D2

Метод резолюций в логике высказываний Рассмотрим задачу выяснения будет ли В логическим следствием из , то есть истинна ли следующая запись: Выше было показано, что эта задача сводится к выяснению невыполнимости формы Найдем для формулы С ее к.н.ф., то есть получим конъюнкцию дизъюнктов: . Каждое слагаемое дизъюнкта является литералом Множество дизъюнктов {D1,D2,…,Dk} считается невыполнимым тогда и только тогда, когда формула С невыполнима.

Метод резолюций Методом резолюций называется последовательное получение бинарных резольвент из данных дизъюнктов и вновь получаемых дизъюнктов. Пусть, например, даны дизъюнкты , , Используя D1 и D2 затем D1 и D3 , получим резольвенты D4=Т, D5=P. Затем из D3 и D4 получим пустой дизъюнкт. Пустой дизъюнкт будем обозначать через . Можно доказать следующую теорему Теорема (о полноте метода резолюций). Множество S дизъюнктов невыполнимо тогда и только тогда, когда существует вывод пустого дизъюнкта из S (имеется в виду, что выводом является применение метода резолюций). Существует много различных подходов к построению вывода с помощью метода резолюций. Рассмотрим некоторые из них: метод насыщения уровня, стратегию вычеркивания, лок-резолюцию и один метод для дизъюнктов специального вида.

Метод насыщения уровня Пусть имеем множество дизъюнктов . Процедура получения бинарных резольвент неоднозначна, ибо можно сравнивать D1 и D2, затем D1 и D3 или как-то иначе. Рассмотрим метод насыщения уровня. Он состоит в вычислении всех резольвент всех пар дизъюнктов из S, добавлении этих резольвент к множеству S, вычислении всех следующих резольвент и повторении этого процесса, до тех пор пока не найдется пустой дизъюнкт . Это значит, мы порождаем где , а Чтобы запрограммировать этот метод на ЭВМ, можно сперва записать дизъюнкты , затем вычислять резольвенты, сравнивая последовательно каждый дизъюнкт с каждым дизъюнктом , который расположен после . Когда резольвента вычислена, она присоединяется к концу списка, порожденного к этому времени.

Пример метода насыщения уровня Перейдем к реализации этого процесса для случая когда S={ P∨Q, , , }. : (1) P∨Q; (2) ; (3) ; (4) ; : (5) Q из (1) и (2); (6) P из (1) и (3); (7) из (1) и (4); (8) из (1) и (4); (9) из (2) и (3); (10) из (2) и (3); (11) из (2) и (4); (12) из (3) и (4); : (13) P∨Q из (1) и (7); (14) P∨Q из (1) и (8); (15) P∨Q из (1) и (9); (16) P∨Q из (1) и (10); (17) Q из (1) и (11); (18) P из (1) и (12); (19) Q из (2) и (6); (20) из (2) и (7); (21) из (2) и (8); (22) из (2) и (9); (23) из (2) и (10); (24) из (2) и (12); (25) P из (3) и (5); (26) из (3) и (7); (27) из (3) и (8); (28) из (3) и (9); (29) из (3) и (10); (30) из (3) и (11); (31) из (4) и (5); (32) из (4) и (6); (33) из (4) и (7); (34) из (4) и (8); (35) из (4) и (9); (36) из (4) и (10); (37) Q из (5) и (7); (38) Q из (5) и (9); (39) из (5) и (12)

Недостаток метода насыщения уровня Было порождено много не относящихся к делу и лишних дизъюнктов. Например, (7), (8), (9) и (10) – тавтологии. Так как тавтология всегда истинна, то если можно вычеркнуть тавтологию из невыполнимого множества дизъюнктов, оставшееся множество все еще должно быть невыполнимо. Следовательно, тавтология есть не относящийся к делу дизъюнкт и не должна порождаться. Если же она порождается, то (за исключением очень немногих случаев) ее следует вычеркнуть. Далее дизъюнкты P, Q, , порождаются неоднократно. Также имеются другие повторяющиеся дизъюнкты, см. (13) – (16), (20) – (23), (26) – (29) и (33) – (36). На самом деле, чтобы получить доказательство для S, нужно породить дизъюнкты (5), (12) и (39).

Стратегия вычеркивания Дизъюнкт D называется поддизъюнктом (или D поглощает ) если D является некоторой частью дизъюнкта . При этом называется наддизъюнктом для D. Пример. Пусть D=P, , Ясно, что D поддизъюнкт для дизъюнкта D*, а D* - наддизъюнкт для D. Стратегия вычеркивания зависит от того, как вычеркиваются тавтологии и наддизъюнкты. Стратегия вычеркивания будет полной, если ее использовать вместе с методом насыщения уровней следующим образом: сперва выписываются дизъюнкты () по порядку; затем вычисляются резольвенты путем сравнения каждого дизъюнкта с дизъюнктом , который стоит после Di. Когда резольвента вычислена, она записывается в конце списка, как только она порождается, если она не тавтология и не поглощается каким-нибудь дизъюнктом из списка. В противном случае она вычеркивается. Очевидно, что при этом не выписывается повторно один и тот же дизъюнкт.

Пример стратегии вычёркивания Применим стратегию вычеркивания к рассмотренному выше примеру и получим следующий список: : (1) P∨Q; (2) ; (3) ; (4) ; : (5) Q из (1) и (2), (6) P из (1) и (3), (7) из (2) и (4), (8) из (3) и (4), : из (5) и (8).

Недостатки стратегии вычёркивания Ясно, что необходимые вычисления не уменьшаются, а увеличиваются. Чтобы использовать стратегию вычеркивания, необходимо уметь определять, является ли полученный дизъюнкт тавтологией или является ли один из дизъюнктов поддизъюнктом другого. Метод резолюций позволяет автоматизировать доказательство теорем. Показано, что неограниченное применение резолюции может порождать много лишних и ненужных дизъюнктов наряду с полезными. Хотя можно использовать стратегию вычеркивания, чтобы выбросить некоторые из этих ненужных и бесполезных дизъюнктов после того, как они порождены, на их порождение уже потеряны ресурсы. Далее, если порождены бесполезные дизъюнкты, то нужны ресурсы для того, чтобы определить, что эти дизъюнкты действительно лишние и ненужные. Поэтому для получения эффективных процедур доказательства теорем необходимо не допускать порождения большого числа бесполезных дизъюнктов. Имеются различные подходы к уменьшению вычислений, среди них: метод семантической резолюции; лок-резолюция; линейная резолюция и др. методы.

Лок-резолюция Идея лок-резолюции состоит в использовании индексов для упорядочения литер в дизъюнктах из данного множества S дизъюнктов. Иными словами она включает введение индексов для каждого вхождения литеры в S некоторым целым числом; разные вхождения одной и той же литеры могут быть индексированы по-разному. После этого отрезать (удалять) разрешается только литеры с наименьшим индексом в каждом из дизъюнктов. Литеры в резольвентах наследуют свои индексы из посылок. Если литера в резольвенте может унаследовать более одного индекса, то ей ставится в соответствие наименьший индекс.

Лок-резолюция, пример 1 Рассмотрим следующие два дизъюнкта P∨Q, . Введем индексы, которые будем писать слева снизу от литеры: (1) , (2) . Так как индекс 1 в 1P меньше чем индекс 2 в 2Q, то разрешается отрезать 1P. В разрешается отрезать , так как 3<4. Таким образом, применяя правило резолюции к дизъюнктам (1) и (2) по 1P и мы получаем следующий дизъюнкт: (3) 2Q∨4Q Литера 2Q и 4Q одна и та же. Так как 2<4, то Q получает индекс 2, поэтому получаем (4) 2Q. Дизъюнкт (4) и является лок-резольвентной дизъюнктов (1) и (2). Под лок-резолюцией понимается последовательное получение лок-резольвент из данного множества дизъюнктов и вновь получаемых дизъюнктов.

Лок-резолюция, пример 2 Рассмотрим множество S дизъюнктов, которое рассматривалось выше: (1) P∨Q; (2) ; (3) ; (4) ; Проведём следующую индексацию: (1) , (2)   (3) , (4) . Из дизъюнктов (1) – (4) можно получить только одну лок-резольвенту (5) из (3) и (4). Из дизъюнктов (1) – (5) получаются только две лок-резольвенты: (6) 2Q из (1) и (5), (7) из (2) и (5). Применяя правила резолюции к дизъюнктам (6) и (7), мы получаем (8) . Таким образом, мы получаем вывод пустого дизъюнкта . Отметим, что были порождены всего три лок-реольвенты. При использовании обычной (неограниченной) резолюции для получения были порождены 38 резольвент. Результативность лок-резолюции не зависит от того, как проиндексировать литеры в S.

Теорема о полноте лок-резолюции Теорема: Пусть S множество дизъюнктов, в котором каждая литера индексирована целым числом. Если S противоречиво (неудовлетворимо), то имеется лок-вывод пустого дизъюнкта из S.

Хорновские дизъюнкты В общем случае метод резолюций требует больших вычислений. Если дизъюнкты имеют специальный вид, являются, так называемыми хорновскими дизъюнктами, то можно упростить вычисления. Литера называется позитивной, если она не содержит отрицания и негативной, если содержит отрицание. Дизъюнкт D называется хорновским, если он содержит не более одной позитивной литеры. Примеры хорновских дизъюнктов: А, В, , , , , . В общем случае хорновский дизъюнкт можно представить в виде (A1&A2&…&An)⇒B или , n≥1, или А. При этом дизъюнкт называют точным, дизъюнкт называют негативным, а дизъюнкт А - унитарным позитивным дизъюнктом.

Метод резолюций для хорновских дизъюнктов Рассмотрим множество S хорновских дизъюнктов без тавтологий. Невыполнимость можно проверить с помощью следующего алгоритма. 1. Полагаем, что . 2. Пусть , построено. Для построения выбираем из дизъюнкты D1 и D2 такие, что: D1 - унитарный позитивный дизъюнкт, пусть, например, D1= Р; D2 - дизъюнкт, содержащий литеру . Вычисляем резольвенту R для дизъюнктов D1 и D2 и полагаем, что . Эта процедура повторяется до тех пор, пока не будет получен пустой дизъюнкт либо пока не окажется, что в не существует дизъюнктов D1 и D2 указанных видов. Можно показать, что для приведенного алгоритма появление пустого дизъюнкта означает, что множество S хорновских дизъюнктов невыполнимо. Если же окажется, что не содержит дизъюнктов D1 и D2 указанных видов, то исходное множество S хорновских дизъюнктов выполнимо.

Пример метода резолюций S={, Q, R, , , } Дизъюнкты, из которых строятся резольвенты, выделены жирным курсивом. На четвертом шаге получаем пустой дизъюнкт, следовательно, множество S хорновских дизъюнктов невыполнимо.

Преобразование формул логики предикатов слайд 1 Любую формулу логики предикатов можно представить в предваренной нормальной форме, т. е. в виде: , где некоторая совокупность кванторов, а формула В не содержит кванторов. Для формулы совокупность кванторов называется префиксом формулы А, а формула B – матрицей формулы А. Будем дополнительно считать, что матрица приведена к конъюнктивной нормальной форме Очевидно, что формула A является противоречием тогда и только тогда, когда – является логически общезначимой. Из свойств формул следует, что формула B является логически общезначимой тогда и только тогда, когда логически общезначимо замыкание формулы B. Как известно, замыкание формулы B получается приписыванием к B кванторов всеобщности по всем её свободным переменным.

Преобразование формул логики предикатов слайд 2 1) исключим знаки импликации, выразив их через ; ∨; 2) добьемся того, чтобы относилась только к элементарным формулам это можно сделать, используя правила перенесения отрицания через кванторы и законы де Моргана; 3) проведём стандартизацию (переименование) переменных для вынесения кванторов за скобки; 4) вынесем кванторы за скобки, т.е. получим предваренную нормальную форму: , здесь B – матрица формулы, а – префикс (совокупность кванторов). Будем считать, что матрица приведена к конъюнктивной нормальной форме; 5) проведём исключение кванторов существования, введением сколемовских функций (Skolem T).

Исключение кванторов существования Исключение кванторов существования проводится следующим образом. Пусть , где – кванторы всеобщности или существования. Положим, что – квантор существования в префиксе . Если никакой квантор всеобщности не стоит в префиксе левее , то выбираем новую предметную постоянную c, отличную от всех предметных постоянных в B, и заменяем все встречающиеся в B на c и вычеркиваем из префикса. Пусть имеем формулу ∃x∀y(P(x,y)⇒Q1(x,a)). Тогда для исключения квантора введем постоянную c. В результате получим формулу:. Рассмотрим другой пример. Пусть имеем формулу . Тогда, исключая кванторы существования, получим: .

Сколемовские функции Если – список всех кванторов всеобщности, встречающихся левее квантора существования , , то выберем новую m–местную функциональную букву , отличную от других функциональных букв из B, и заменим все в B на и вычеркнем из префикса. Пример. Пусть имеем формулу ∀x∃y(P(x,y)⇒Q(f1(a),y)). Введя функцию f2, с аргументом х и исключая импликацию получим: . Пример. Пусть имеем другую формулу: . Тоже, вводя необходимую функцию и исключая импликацию, получим: . Описанная процедура выполняется до тех пор, пока не будут исключены все кванторы существования. Полученная в результате формула есть сколемовская стандартная форма, для краткости стандартная форма формулы A. Константы и функции, используемые для замены переменных квантора существования, называются сколемовскими функциями.

Стандартная форма функции Пример. Пусть имеем формулу . Приведём матрицу формулы к к.н.ф.:. Затем введём функции f(x), g(x): . Полученная формула является стандартной формой исходной формулы. Элементарную формулу или её отрицание называют литералом (литерой) в логике предикатов. Дизъюнктом в логике предикатов называют дизъюнкцию литералов. Иногда литералы или дизъюнкты называют клаузами (clause – предложение, являющееся частью сложного предложения).

Многозначность стандартной формы Пусть формула А приведена в предваренную нормальную форму, а ее матрица представлена в к.н.ф., т. е. где префикс формулы А, а – дизъюнкты. Положим, что стандартная форма для A равна , где в префиксе опущены кванторы существования, а получены из введением сколемовских функций вместо переменных кванторов существования. Отметим, что стандартная форма формулы А определяется не единственным образом, ибо сколемовские функции можно вводить неоднозначно.

Теорема о противоречии Теорема: Формула A является противоречием тогда и только тогда, когда её стандартная форма является противоречием. Следствие 1: Если А противоречие, и то . Следствие 2: Пусть – стандартная форма формулы A и пусть A противоречие. Тогда . Отметим, что если A не является противоречием, то может быть, что A не равносильна . Например, пусть . Тогда . Построим интерпретацию. Пусть область интерпретации M={1,2} . Положим, что a=1, а P(x) обозначает предикат «x - четное число». Тогда обозначает: «1 - четное число». Следовательно, формула As ложна в этой интерпретации. Формула A в этой интерпретации представляет истинное высказывание: .

Унификация Процесс унификации является основным в формальных преобразованиях, выполняемых при нахождении резольвент (для метода резолюций). Пусть задано множество дизъюнктов. Каждый дизъюнкт составлен из литералов. Пример. Пусть имеем следующее множество дизъюнктов: Термы литерала могут быть переменными, постоянными или выражениями, состоящим из функциональных букв и термов. Например, для литерала P(x, f(y), b) имеем, что х – переменная, f(y) – сложный терм, b - постоянная.

Частные случаи литерала и подстановки Подстановочный частный случай литерала получается при подстановке в литералы термов вместо переменных. Пусть имеем литерал P(x, f(y), b). Его частными случаями будут: , , – константный частный случай литерала или атом, т.к. нет переменных. Подстановки, примененные в рассматриваемом примере, можно обозначить следующим образом: , здесь z подставляется вместо x, а w вместо y; θ2 = {a/y}; ; .

Применение подстановки к литералу Применение подстановки θ к литералу Р обозначаем Рθ. Тогда имеем Если – подстановка и она применяется к каждому из литералов , то полученные частные случаи обозначаются через . Последовательное применение двух подстановок и дает новую подстановку , которую обозначаем . Множество литералов называется унифицируемым, если существует такая подстановка , что В этом случае подстановку называют унификатором для .

Унификатор Пусть имеем множество литералов , где . Подстановка является унификатором для этого множества литералов. Унификатор для множества выражений называется наиболее общим унификатором тогда и только тогда, когда для каждого унификатора для этого множества существует такая подстановка , что . Существует алгоритм, называемый алгоритмом унификации, который приводит к наиболее общему унификатору для унифицируемого множества литералов и сообщает о неудаче, если это множество не унифицируемо.

Алгоритм унификации Алгоритм начинает работу с пустой подстановки и шаг за шагом строит наиболее общий унификатор, если таковой существует. Предположим, что на k-ом шаге получена подстановка . Если все литералы из в результате становятся идентичными, то и есть наиболее общий унификатор. В противном случае каждый из литералов в рассматривается как цепочка символов и выделяется позиция первого символа, в которой не все из литералов имеют одинаковый символ. Рассмотрим пример двух литералов. Стрелками пометим позиции, где появились различные символы (при просмотре слева направо). Затем конструируется множество рассогласования, содержащее правильно построенные выражения из каждого литерала, который начинается с этой позиции (правильно построенное выражение представляет собой либо терм, либо литерал). Так для рассмотренного примера множеством рассогласования будет {g(z), u}. Далее модифицируем (если можно) подстановку , чтобы сделать равным два элемента из множества рассогласования. Это можно сделать только тогда, когда множество рассогласования содержит переменную, которую можно положить равной одному из его термов. Если множество рассогласования не содержит переменных, то множество унифицировать нельзя.

Теорема Робинсона Теорема Робинсона. Описанный выше алгоритм находит наиболее общий унификатор для множества унифицируемых литералов и сообщает о неудаче, если литералы неунифицируемы.

Пример унификации 1 слайд 1 Пусть . Найдем общий унификатор. 1. Пустая подстановка ε. – не единичный дизъюнкт, следовательно, не получили наиболее общий унификатор. 2. Множество рассогласования равно: , следовательно, , тогда , S1 – не единичный дизъюнкт.

Пример унификации 1 слайд 2 3. Множество рассогласований для S1 равно: , тогда , и . S2 – не единичный дизъюнкт. 4. Множество рассогласований для S2 равно: , тогда вновь строим: и . S3– единичный дизъюнкт, следовательно, θ3 наиболее общий унификатор.

Пример унификации 2 Пусть . Пустая подстановка ε. – не единичный дизъюнкт и , , , S1 – не единичный дизъюнкт. . В множестве нет переменной как элемента этого множества. Следовательно, алгоритм унификации завершается, и определяется что S не унифицируемо.

Метод резолюций в логике предикатов слайд 1 Пусть имеем множество литер . Если для этого множества существует общий унификатор , например, , то из этих трех литер достаточно оставить только одну. Если для некоторых оставшихся существует общий унификатор , например, , то тоже оставляем только одну из них и т.д. Пример. Пусть , тогда: , , где ,, – факторы. Если две или более литер (с одинаковым знаком) дизъюнкта имеют наиболее общий унификатор : , то оставление одного из этих литералов вместо всех них называют склейкой.

Метод резолюций в логике предикатов слайд 2 Пусть имеем два дизъюнкта и и переменные входящие в D1 не входят в и обратно. Если это не так, то переименованием переменных этого можно добиться. Пусть в есть литера, например, , а в - литера . Если и имеют наиболее общий унификатор, т. е. , то новый дизъюнкт R: называется бинарной резольвентой и (в логике предикатов). Литеры и называются отрезаемыми литерами.

Пример метода резолюций Пусть , . Переименуем х в : . Положим, что . Тогда имеем , , Отбрасываем литеры , и получим бинарную резольвенту: . Пусть имеем , . Тогда и .

Резольвента дизъюнктов Резольвентой дизъюнктов – посылок и является одна из следующих резольвент: 1) бинарная резольвента и , 2) бинарная резольвента и склейки , 3) бинарная резольвента и склейки , 4) бинарная резольвента склейки и склейки . Применение описанных резольвент к множеству дизъюнктов и называется методом резолюций. Можно доказать следующую важную теорему: Теорема (полнота метода резолюций): Множество S дизъюнктов невыполнимо тогда и только тогда, когда существует вывод пустого дизъюнкта из S.

Проблема дедукции логики предикатов Проблема дедукции логики предикатов состоит, как и в логике высказываний, в выяснении будет ли формула В логическим следствием формул . Можно получить следующую последовательность действий для выяснения будет ли формула В логическим следствием формул Строим конъюнкцию . Отметим, что требуемое следствие (заключение) взято с отрицанием. Находим стандартную форму Сs для формулы С. Положим, что форма , где префикс формулы без кванторов существования, а – дизъюнкты, в которых по необходимости введены сколемовские функции. Для множества дизъюнктов применяем метод резолюций. Формула В будет логическим следствием формул тогда и только тогда когда существует вывод пустого дизъюнкта из S.