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

Итак, в выводе, который только что был продемонстрирован, все время приходилось выводить истинность отдельных литералов, а затем, комбинируя их 82 4.1. Исчисление предикатов в истинную конъюнкцию а и используя какую-либо истинную импликацию а з р, применять правило модус поненс а, а z> p Ьр для получения новой истинной формулы р, по которой затем снова приходилось выводить истинные литералы, и так до тех пор, пока не получится требуемая нам истинная формула. Поскольку в этом процессе все время приходилось спускаться на уровень отдельных литералов, то естественным образом напрашивается идея ввести ограничения на вид используемых в исчислении и правиле модус поненс формул так, чтобы не приходилось постоянно и раздельно применять правила исключения квантора общности, исключения конъюнкта и введения конъюнкции.