«В исчислении предикатов в гильбетровском варианте правилами вывода являются
- модус поненс
- правило обобщения» (q) https://ru.wikipedia.org/wiki/Правило_вывода
   (нет ли здесь опечатки в слове "гильбеРТовском"?)

«правило вывода — это эффективная процедура для проверки того, что одна заданная формула в рассматриваемой теории непосредственно за один шаг выводится из других заданных формул»
   Что общего у резолюции (resolution) и у унификации (unification)?

Отредактировано Лис (2019-11-24 18:51:50)