Математическая логика и теория алгоритмов

с помощью ЭВМ. В случае применения метода резолюций вычисле­ ния оказываются совсем незначительными. Следуя указанной в § 10 процедуре, нужно получить сколемов- скую стандартную форму Cj для формулы С, которая имеет вид (3.9). Сначала переименуем вхождения х во второй посылке на у, а в заклю­ чение силлогизма на z (в первой посылке переменную х не переимено­ вываем). Легко видеть, что первые два дизъюнкта в Q будут следую­ щими: Г) 1 ^(x) у Р (Л:), 2) ЛР(уШ{у\ и, очевидно, они получены из посылок силлогизма. Заключение сил­ логизма в (3.9) взято с отрицанием: lV2(5(z)=>2(z)). Преобразуя по­ следнюю формулу, получим: 3z(S(z)Sc]Q(z)). При нахождении сколе- мовской стандартной формы квантор существования можно вынести первым и затем, удаляя его, ввести постоянную а вместо переменной удаляемого квантора (переменной г). В результате в стандартной форме Cj будут еще два дизъюнкта: 3) S{a), 4) полученные из заключения силлогизма. Теперь к множеству дизъюнк­ тов 1 ) ^ ) применяем метод резолюций. Тогда имеем последовательно: 5) Р{а) из 3) и 1), 6) ~\Р{а) из 4) и 2), 7) • из 5) и 6). Таким образом, получили пустой дизъюнкт, следовательно, сил­ логизм A A A верен. Рассмотрим силлогизм Darii ( A l l по 3-й фигуре), В символиче­ ской записи имеем: Vx(P(x):=^S(x)) зх {р(х) & е(х)) 3x(5(A-)&e(x)). Преобразуя, как и ранее, получим: 115