В предлагаемой работе модифицируется метод резолюций Робинсона на случай использования интерпретированных на эрбрановском универсумепредикатов. К известному правилу резолюции Робинсона добавляется правило унарной резолюции Ru, которое может быть применено только к дизъюнкту, использующему интерпретированный предикат. Правило Ru оказывается неэффективным правилом, так как вопрос о том, можно ли Ru именно таким образом применить к дизъюнкту или нет, сталкивается с алгоритмически неразрешимой проблемой. Поэтому нас будут интересовать его эффективные ограничения, а если точнее, то эффективные разумные ограничения, которые по своим возможностям эквивалентны Ru. Нами доказана полнота модифицированного правила резолюции в случае любых разумных ограничений Ru. Полнота понимается следующим образом: из конечного множества дизъюнктов 5 выводим пустой дизъюнкт тогда и только тогда, когда 5 противоречиво на множестве эрбрановских интерпретаций.
展开▼
