Дедуктивный вывод с использованием необходимых и достаточных условий выводимости в исчислении предикатов первого порядка

Даются необходимые и достаточные условия выводимости в рамках исчисления предикатов первого порядка. С использованием этих условий формируются конечные алгоритмы проверки существования строгого логического вывода заключения из группы посылок, пригодные для создания прикладных машин вывода.На примере доказательства известных силлогизмов демонстрируется работоспособность предложенных алгоритмов.