Искусственный интеллект

Как следствие, неутешительным остается ответ и на вопрос распознавания противоречивости исчисления: для того чтобы установить непротиворечивость исчисления в общем случае, придется осуществить вывод всех теорем и только при отсутствии среди них любых двух, одна из которых является отрицанием другой, сделать заключение о непротиворечивости исчисления. 95 4. Вывод в логике предикатов 4.4. Вывод на основе правила резолюция Правило резолюции (или резолюция) уже рассматривалось во второй главе. Это правило гласит, что из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая — его отрицание, следует (выводима) формула, являющаяся дизъюнкцией исходных формул без упомянутого дизъюнкта и его отрицания. Резолюция записывалась в следующем виде: