Альтернативные системы аксиом
Методическое пособие - Философия
Другие методички по предмету Философия
стина).В КНФ нет одинаковых дизъюнктов, т. к. C&C = C.
Пример:
(AVB)(AVC)( AVB) - КНФ.
КНФ тоже можно записывать как множество дизъюнктов. Т. е. есть
КНФ С1 С2 … Сn => (C1, C2, …,Cn) - КНФ.
Приведем формулу
F1& … Fn&G к КНФ => вопрос: КНФ - противоречива ?
Для приведения формулы к КНФ используются тождества булевой алгебры:
A B = A V B B = (A B)(B A)&И = AV И = И& (B V C) = (A & B) V (A & C)V (B & C) = (A V B) & (A V C)
(AVB) = A&B
(A&B) = AVB
з-ны иденпатентности, ассоциативности, дистрибутивности.
Пример: (AB) V (A&C) приведем к КНФ.
(A B) V (A & C) = A V B V (A & C) = ( A V B V A) & ( A V B V C) = A V B V C.
Теперь проверяем на противоречивость КНФ.
Резольвентой 2-х дизъюнкта R(C1, C2), где
C1 = L1 V L2 V … V Lk,2 = L1 V L2 V … V Lm,
наз. R(C1, C2) = L2 V … V Lk V L2 V … V Lm
Пример: C1 = A V B V C, C2 = A V B V D
Тогда R(C1, C2) = BVCVD
Замечание: не имеет смысла искать R(C1, C2), если C1 = AVB, а C2 = AVB, т. к. в любом случае получим ТИ (и по А, и по В), а мы ищем противоречивость формулы.
Понятие резольвенты. Логическое следование резольвенты из дизъюнктов
Пусть C1, … Cm - мн-во дизъюнктов, тогда резолютативным выводом из этого множества дизъюнкта D наз. цепочка дизъюнктов A1, A2, …, Ak (=D), где A1 - либо исходный дизъюнкт, либо получен из исходных дизъюнктов с помощью метода резолюций.
Лемма: резольвента является логическим следствием своих дизъюнктов, т. е. R, C1, C2. C1&C2R - тавтология (*).
Док-во:
Если R - резольвента
С1, С2, то С1 = LVL1V … V Lk, C2 = L V L1 V … V Lm.
Если (С1&C2) = Л, то ф-ла (*) - И
если истина - 1 из литералов L1, …, Lk (C1), то этот литерал войдет и в R =>R - истина => импликация - истина;
если С1 = И за счет литерала L, по С2 - тоже истина, а L = Л, а С2 = И за счет какого-то литерала кроме L => этот литерал войдет и в R =>R = И => импликация - И.
Следствие: Пусть дана КНФ С1& … &Cn и резольвента R = R(Ci, Cj). Тогда эта формула КНФ C1& … &CnC1& … &Cn&R.
Доказательство:
Если л.ч. = Л =>п.ч. = Л
Если л.ч. = И =>п.ч. = И (по лемме)
Замечание: для проверки на противоречивость КНФ (мн-ва дизъюнктов) можно порождать резольвенты до тех пор, пока не получим ТЛ.
Резольвенты находятся не только для исходных дизъюнктов, но и для тех резольвент, кот. порождаются.
Теорема о полноте метода резолюций
Теорема о полноте метода резолюций:
КНФ (множество дизъюнктов) - противоречие из множества дизъюнктов выводится резолютотивно пустой дизъюнкт.
Док-во:
Если выводим пустой дизъюнкт, то формула - противоречие. Это возможно только в том случае, если
C1 = L, C2 = L
Но тогда имеем КНФ: LL Л.
{C1& … &Cn = C1& … &Cn&R1 = … = C1& … &Cn&R1& … &L&L Л}
II
Пусть исходная формула - противоречие. Покажем, что выводится пустой дизъюнкт (по индукции).
Есть C1, …, Cn
Выводится пар-р K(S) = (кол-во вхождений всех литералов) - n (кол-во дизъюнктов) аксиома резолюция противоречие
Например, КНФ: (BVA)C(BVD)K(S) = 5 - 3 = 2
БИ: докажем справедливость при K(S) = 0 (для всех таких формул)
K(S) = 0 пустой дизъюнкт выводится.
Индуктивный переход: пусть мы доказали для km. Докажем для формулы, у которой k = m + 1 > 0.
Если K> 0 => 1 из дизъюнктов содержит хотя бы 2 литерала (пусть С1).
С1 = LVC1.
Исх. формула: S = C1& … &Cn = C1& S = (L V C1) S.
Эта формула -противоречие , когда формула S = LS VC1S - противоречие.
Но у формул LS и C1S характеристика К меньше, чем у формулы S на 1.
Берем КНФ C1S (для нее выполнимо предположение индукции) => для нее пустой дизъюнкт выводим (с помощью метода резолюций). Берем этот вывод, кот. применяли к C1S и применяем его к S. S и C1S отличаются тем, что во 2-й формуле отбросили литерал L. Тогда из S получим либо пустой дизъюнкт, либо литерал L => из S можно вывести L. По предположению индукции из LS можно получить пустой дизъюнкт => получился вывод из S пустого дизъюнкта.
Алгоритм метода резолюций для ЛВ
Алгоритм метода резолюций для исчисления высказываний.
Представляем формулу, противоречивость которой нужно показать в виде КНФ. Для этого можем пользоваться алгеброй тождеств булевой алгебры.
i=1
Находим все всевозможные резольвенты
Дополняем исходное множество всеми найденными резольвентами.
(Батарея села)
Таким образом, в соответствии с методом резолюций, для любой ферулы ИВ за конечное число шагов можно определить является ли она противоречием.
Понятие предиката, функции, терма
Рассмотренные нами ИВ являются грубой моделью представления знаний, основным недостатком которой является то, что высказывание рассматривается как единое целое без анализа его внутренней структуры. Это ограничивает возможности ИВ при моделировании сложных силологических построений.
Рассмотрим классический пример: пусть имеются предпосылки: все люди смертны, Сократ-человек, следовательно Сократ - смертен. С точки зрения логики вывод здесь безупречен, но он уже выходит за рамки ИВ. С помощью пропозициональных связок и букв:
.
Если высказывание оперирует с фактом как с единой формулой, то предикатная форма наоборот отображае?/p>