Напомним, что если х - логическая переменная, а σœ{0,1} то выражение
x σ = xx еслиеслиσσ == 10 или x σ = 10 еслиесли x x =≠σσ , называется литерой. Литеры x и Ÿx называются контрарными.Конъюнктом называется конъюнкция литер. Дизъюнктом называется дизъюнкция литер.
Пусть D1 = B1 ∨ A , D2 = B2 ∨ A — дизъюнкты. Дизъюнкт B1¤B2 называется резольвентой дизъюнктов D1 и D2 по литере А и обозначается через resA(D1,D2). Резольвентой дизъюнктов D1 и D2 называется резольвента по некоторой литере и обозначается через res(D1,D2). Очевидно, что res(A,ŸA)=0. Действительно, т.к. A=A¤0 и ŸA=ŸA¤0, то res(A,ŸA)=0¤0=0. Если дизъюнкты D1 и D2 не содержат контрарных литер, то резольвент у них не существует.Пример 5.5.1. Если
D1=A¤B¤C, D2 = A ∨ B ∨ Q , то resA(D1,D2)=B¤C¤ B ¤Q, resB(D1,D2)=A¤C¤A¤Q, resC(D1,D2) не существует.Утверждение 5.5.1. Если res(D1,D2) существует, то D1,D2+ res(D1,D2).
Пусть S=(D1,D2,…,Dn) - множество дизъюнктов.
Последовательность формул F1,F2,…,Fn называется резолютивным выводом из S, если для каждой формулы Fk выполняется одно из условий:
1. FkœS;
2. существуют j, k <i такие, что Fi=res(Fj,Fk).
Теорема 5.5.1.(о полноте метода резолюций). Множество дизъюнктов S противоречиво в том и только в том случае, когда существует, резолютивный вывод из S, заканчивающийся 0.
Отметим, что метод резолюций можно использовать для проверки выводимости формулы F из данного множества формул F1,F2,…,Fn. Действительно, условие F1,F2,…,Fn+F равносильно условию F1,F2,…,Fn,ŸF+ (множество формул противоречиво), что в свою очередь равносильно условию Q+, где Q=F1⁄F2⁄…⁄Fn⁄(ŸF). Приведем формулу Q к КНФ: Q=D1⁄D2⁄...⁄Dm, тогда Q+ ‹D1⁄D2⁄...⁄Dm+ ‹ D1,D2,...,Dm+. Таким образом, задача проверки выводимости F1,F2,…,Fn+F сводится к проверке противоречивости множества дизъюнктов S={D1,D2,...,Dm}, что равносильно существованию резолютивного вывода 0 из S.
Пример 5.5.2. Проверить методом резолюций соотношение АØ(ВØС), CDØЕ, ŸFØD&(Ÿ)E + АØ(ВØF).
Согласно утверждению 5.3.1. надо проверить на
противоречивость множество формул
S = {АØ(ВØС), CDØЕ, ŸFØD&(Ÿ)E, Ÿ(АØ(ВØF))}.
Приведем все формулы из. S к КНФ:
S = {A ∨ B ∨ C,C ⋅ D ∨ E, F ∨ D ⋅ E, A ∨ B ∨ F} == {A ∨ B ∨ C, C ∨ D ∨ E, (F ∨ D) ⋅ (F ∨ E), A ⋅ B ⋅ F} . Таким образом, получаем множество дизъюнктов S = {A ∨ B ∨ C, C ∨ D ∨ E,F ∨ D,F ∨ E,A,B, F}Построим резолютивный вывод из S, заканчивающийся 0:
1.
res A {A ∨ B ∨ C,A} = B ∨ C ;2. res B{B ∨ C,B} = C ;
3.
res D {C ∨ D ∨ E,F ∨ D} = C ∨ E ∨ F ;4. res E {C ∨ E ∨ F,F ∨ E} = C ∨ F ;
5.
res C {C, C ∨ F} = F ; 6. res{F, F} = 0 .Итак, заключаем, что формула АØ(ВØF) выводима из множества формул АØ(ВØС), CDØЕ, ŸFØD&(Ÿ)E .
Отметим, что метод резолюций достаточен для обнаружения возможной выполнимости данного множества дизъюнктов S. Для этого включим в множество S все дизъюнкты, получающиеся при резолютивных выводах из S. Из теоремы о полноте метода резолюций вытекает
Следствие 5.5.1. Если множество дизъюнктов S содержит резольвенты всех своих элементов, то S выполнимо тогда и только тогда, когда 0–S.
Характерной чертой современности является широкое использование компьютеров при решении проблем (задач) в различных областях человеческой деятельности. Однако, предварительно задача должна быть решена алгоритмически, т.е. должно быть задано формальное предписание, следуя которому можно получить итоговый результат для решения всех задач определенного типа (это интуитивное, не строгое понятие алгоритма). Например, алгоритм нахождения наибольшего общего делителя двух натуральных чисел а, b, выглядит следующим образом :
1) разложить число a на простые множители;
2) повторить п. 1 для b и перейти к п. 3;
3) составить произведение общих простых множителей из разложений а и b с показателями, равными наименьшим из показателей вхождения в разложения.
Проанализировав этот пример, отметим важнейшие черты (свойства) алгоритма:
1. Массовость — применимость алгоритма не к одной задаче, а к классу задач.
2. Дискретность — четкая разбивка на отдельные этапы (шаги) алгоритма.
3. Детерминированность — такая организация этапов выполнения, при которой всегда ясно как осуществить переход от одного этапа к другому.
4. Конечность — для получения результата при применении алгоритма к решению конкретной задачи выполняется конечная последовательность шагов алгоритма:
Отметим, что если наличие алгоритма само по себе служит доказательством существования алгоритма, то для доказательства его отсутствия необходимо иметь строгое математическое определение алгоритма.
Попытки формализовать понятие алгоритма привели к созданию машины Тьюринга, как некоего воображаемого устройства, реализующего алгоритм. Ещё одним шагом в определении понятия алгоритма стало появление рекурсивных функций, как функций, формализующих понятие алгоритма и реализующих интуитивное понятие вычислимости. Вскоре было установлено, что множество рекурсивных функций совпадает с множеством функций, вычислимых на машинах Тьюринга. Появлявшиеся затем новые понятия, претендующие на объяснение понятия алгоритма, оказывались эквивалентными функциям, вычислимым на машинах Тьюринга, а значит, и рекурсивным функциям. Итогом развернувшейся дискуссии о том, что такое алгоритм, стало утверждение, называемое сейчас тезисом Чёрча.
Тезис Чёрча. Понятие алгоритма, или вычислимости некоторым механическим устройством, совпадает с понятием вычислимости на машинах Тьюринга (а значит, с понятием рекурсивной функции). Другими словами, алгоритм - это процесс, который может быть представлен функциональной схемой и реализован некоторой машиной Тьюринга.
Это утверждение нельзя считать математической теоремой. Это есть некоторый естественнонаучный тезис, принятый большинством исследователей.
Машина Тьюринга представляет собой (абстрактное) устройство, состоящее из ленты, управляющего устройства и считывающей головки.
Лента разбита на ячейки. Во всякой ячейке в точности один символ из внешнего алфавитаA={a0,a1,…,an}. Некоторый символ (будем обозначать его Ÿ) алфавита A называется пустым, а любая ячейка, содержащая в данный момент пустой символ, называется пустой ячейкой (в этот момент). Лента предполагается потенциально неограниченной в обе стороны.
Управляющее устройство в каждый момент времени находится в некотором состоянии qj, принадлежащем множеству Q={q0, q1,..., qm} (m=l). Множество Q называется внутренним алфавитом. Одно из таких состояний (обычно q0) называется заключительным, а некоторое другое (обычно q1) -начальным.
Считывающая головка перемещается вдоль ленты так, что в каждый момент времени она обозревает ровно одну ячейку ленты. Головка может считывать содержимое обозреваемой ячейки и записывать в нее вместо обозреваемого символа некоторый новый символиз внешнего алфавита A (возможно тот же самый).
В процессе работы управляющее устройство в зависимости от состояния, в котором оно находится и символа, обозреваемого головкой, изменяет свое внутреннее состояние q. Затем выдает головке приказ напечатать в обозреваемой ячейке определенный символ из внешнего алфавита A, а потом приказывает головке либо остаться на месте, либо сдвинуться на одну ячейку вправо, либо сдвинуться на одну ячейку влево. Попав в заключительное состояние, машина прекращает работу.
Конфигурацией на ленте (или машинным словом) называется совокупность, образованная: