Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

ДЛЯ любого i, l<i<m. Теорема 3.4. Если формула Ai &A2&...&Arfi & —[B (3.3) является противоречием, то В является логическим следствием из A2yA2^'''yAffi, т.е.. A2fA2f'yAffi ^В. Доказательство. Пусть формула (3.3) является противоречием, тогда ее отрицание является тавтологией: 1= (3.4) Очевидно, имеем —i(Aj&A2&...&Afn&S) —\(A j &A2& ...&Ащ) vB ~ (А1&А2&...&Ащ) В. Следовательно, утверждение (3.4) можно записать в виде: 1= (Ai&A2&...&Ar^^B. (3.5) Из (3.5) по теореме 3.2 получаем, что (А1&А2&...&Ащ) \'В. (3.6) Теперь, используя утверждения (3.2) и (3.6), по теореме 3.1 получим требуемое соотношение (3.1). Теорема доказана. Используя теорему 3.3, можно получать следствия из заданного множества формул следующим образом. Для заданного множества формул Л;, А2у...^т, т>1, строим их конъюнкцию: C=Ai&A2&...&Am. Для С находим с.к.н.ф.: С= Di&D2&...&Dk, здесь Z)/, l<i <к, - элементарные суммы (дизъюнкты). Теперь по указанной теореме 3.3 получаем, что каждый дизъюнкт Z)/, 1<i<к, а также их конъюнкции являются следствиями mAj,A2,..../im, пг>1, т. е. имеем: Ai,A2,...^m\=Di для любого г, l<i<k; Ai, А2,...^т\= & для любого г, 1< г< к и любых sj, S2,...,Sr, l<Sj, S2,...,Sr<k. Заметим, что для формул логики предикатов понятие логического следствия из данной формулы (данных формул) введено в 6 - ом параграфе второй главы. Нетрудно убедиться, что теоремы 3.1 - 3.4 остаются в силе и для формул логики предикатов, в частности, теорема 3.2 для формул логики предикатов уже доказана, см. теорему 2.1. § 2. Резольвента дизъюнктов логнкн высказываний. Метод резолюций в логике высказываний Элементарная сумма (дизъюнкция пропозициональных букв или их отрицаний), считается дизъюнктом в логике высказываний. 61