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

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