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

2. Находим (сколемовскую) стандартную форму Q для формулы С. Положим, что форма Q = (Q \X\Q2X2 ...Qr^nyCi&C2&....&.Cm, где HQi X iQ2 X 2- • 'QriXn) - префикс формулы без кванторов существования, а Ci,C2,...,Cm - дизъюнкты, в которых по необходимости введены ско- лемовские функции. 3. Для множества дизъюнктов 5^{СьС2,...,С„,} применяем метод резолюций. Формула В будет логическим следствием формулЛ ь Aj, А„ тогда и только тогда, когда существует вывод пустого дизъюнкта из S. В мозгах как иа мануфактуре, есть ниточки и узелки, • Посылка не по той фигуре грозит запутать узелки. И. Гете § 11. Приложение метода резолюций д л я анализа силлогизмов Аристотеля По Аристотелю «силлогизм океестьречь,в которойприпред­ положении чего-нибудь из негос необходимостью вытекает нечто отличное от утвержденного и [именно] в силу того, чтоэтоесть». Известно, что силлогизм Аристотеля можно представить как не­ которую комбинацию предложений следующих ввдов; А : Всякий М есть Р \/д:(М(д:)=> Р ( х ) ) ; Е: Всякий М не есть Р V x ( M ( x ) = > l Р(х)); I: Некоторый М есть Р Зх{М{х)&Р{х)У, О: Некоторый Мне есть Р Зх{М{х)& 1 Р(х)). Силлогизм обозначают буквами по видам посылок и виду заключения. Например, силлогизм A A A означает, что использованы три предложения вида А. В зависимости от положения среднего тер­ 113