Труды КНЦ (Технические науки вып. 7/2023(14))

Исчисление предикатов первого порядка. Язык L, в свою очередь, используется для построения теории первого порядка, которая формируется на основе языка первого порядка за счет добавления аксиом и правил вывода, причем аксиомы делятся на два класса: логические и собственные (или нелогические). Язык первого порядка с логическими аксиомами и правилами вывода называется исчислением предикатов первого порядка. В публикациях по математической логике имеется несколько вариантов логических аксиом для исчисления предикатов. Что касается собственных (или нелогических) аксиом, то они добавляются к логическим для построения на основе исчисления предикатов различных математических теорий (например, теории групп или аксиоматической теории множеств). Рассмотрим правила вывода. Они весьма лаконичны. В работе [2] они выражены так (здесь B и C — ППФ языка L): modus ponens (MP): из B и B з C следует C; правило обобщения (Gen): из B следует (Vxi)B. Правило MP пришло из античности, впервые оно упомянуто в трудах преемника Аристотеля Теофраста. Что касается правила Gen, то в книге Мендельсона оно выражено не совсем корректно, т. к. при определенных условиях, которые почему-то не сформулированы в работе [2], формула (Vxi)B не может быть следствием B. В исследовании [4] доказано, что в случае, когда формула B содержит свободную переменную x, то формула (Vx,)B может быть следствием формулы B лишь в исключительных случаях. Поэтому без учета этих условий правило Gen нельзя считать корректным. Аксиомы и правила вывода исчисления предикатов не предназначены и трудно применимы для естественных рассуждений. В искусственном интеллекте, в частности, в таких его разделах, как «Моделирование рассуждений» [10] и «Автоматическое доказательства теорем» [11], они не используются в силу малой эффективности, но применяются принципиально иные методы, в частности, метод резолюций и алгоритм унификации. Кроме того, с помощью средств математической логики трудно, а иногда просто невозможно, применять многие необходимые в естественных рассуждениях методы логического анализа такие, как формулирование и проверка гипотез, анализ неопределенностей, распознавание и анализ ошибок и некорректностей в рассуждениях, вывод следствий с заданными свойствами, поиск абдуктивных заключений и т. д. [4]. Не в том ли причина, что в математической логике потеряна связь с семантикой, т. е. с интерпретацией, в основе которой лежит алгебра множеств? Новый подход к интерпретации языка первого порядка В работе [2] предлагается следующая интерпретация языка первого порядка: в качестве области интерпретации ( domain ) для всех переменных используется одно и то же множество D элементов (констант), а для n-местных предикатов и формул с n-свободными переменными областью интерпретации является n-местное отношение, т. е. подмножество n-местных кортежей элементов из декартова произведения множеств D n. В данной интерпретации языка первого порядка предикаты и формулы соответствуют математическим отношениям. Но эта интерпретация представляет лишь частный случай отношения и поэтому трудно применима на практике. С целью усиления аналитических возможностей в общепринятую интерпретацию языка первого порядка было предложено внести следующие изменения [4]. Изменение 1. Для разных переменных языка первого порядка предлагается использовать не одну какую-то область интерпретации D , а разные области интерпретации, которые в большей степени соответствуют предметной области рассуждения. Поэтому по аналогии с базами данных имена разных областей интерпретации предложено называть атрибутами , а сами области интерпретации (т. е. множества всех значений атрибутов) — их доменами. Изменение 2. Исследования показали, что для обоснования закономерностей и решения многих задач логического анализа более удобно рассматривать n-местное отношение не только как множество Труды Кольского научного центра РАН. Серия: Технические науки. 2023. Т. 14, № 7. С. 26-34. Transactions of the Kola Science Centre of RAS. Series: Engineering Sciences. 2023. Vol. 14, No. 7. P. 26-34. © Кулик Б. А., 2023 29