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

т.е. необходимо доказать, что из формул Vx(S(x)^P(x)) и Vx(P(x)^>Q(x)) логически следует формула Vx(S(x)^>Q(x)). Известно, что, если формула С = (Vx(S(x)^P(x)))&(Vx(P(x)^(x)))& -п Vx(S(x)^(x)) (3.9) является противоречием, из посылок силлогизма будет логически следо­ вать его заключение. Так как формула С содержит только одноместные преди­ катные буквы (S,P,Q), то выяснение является противоречием С или нет можно было бы свести к проблеме разрешимости логики высказываний. При этом по­ лучили бы нетривиальную задачу в силу следующего. В формуле С три преди- л катные буквы, следовательно, нужно было бы взять множество, содержащее 2 =8 элементов, положимМ={1,2,...,8}. Тогда каждый предикат порождает наМ по 8 высказываний: S(\),... ,S(S); Р(\),... ,P(S) ; Q(\),... ,Q(S). Следовательно, в пропозициональной форме, построенной для С, будет 24 переменных и таблица 24 истинности будет содержать 2 строк. Ясно, что составление такой таблицы сложно даже с помощью ЭВМ. В случае метода резолюций вычисления оказы­ ваются совсем незначительными. Следуя указанной в параграфе 8 процедуре, нужно получить сколемовскую стандартную форму С для формулы С. Сначала переименуем вхождения х во второй посылке на а в заключении силлогизма на z (в первой посылке пере­ менную X не переименовываем). Легко видеть, что первые два дизъюнкта в Cg будут следующими: 1)^S(xJ vP(x), 2)^(y)vQ(y), которые, очевидно, получены из посылок силлогизма. Заключение силло­ гизма в (3.9) взято с отрицанием: -i Vz(S(z)^>Q(z)). Преобразуя последнюю фор­ мулу, получим: 3z(S(z)&^Q(z)). При нахождении сколемовской стандартной формы квантор существования можно вынести первым и затем, удаляя его, ввести постоянную а вместо переменной удаляемого квантора (переменной z). В результате в стандартной форме С будут еще два дизъюнкта: \)S(a), 2) -^Q(a), полученные из заключения силлогизма. Теперь к множеству дизъюнктов 1)-4) применяем метод резолюций. Тогда имеем последовательно: 5)Р(а) из 3) и 1), 6) —Р(а) из 4) и 2), 7) • из 5) и 6). Таким образом, получили пустой дизъюнкт, следовательно, силлогизм верен. Рассмотрим силлогизм Darii {АН по 3-ей фигуре). В символической записи имеем: 80