Автоматизация логического вывода в исчислении предикатов

Abstract

Рассмотрена интерпретация формул исчисления предикатов первого порядка на конечной предметной области с помощью алгебры кубических функций. Предложена машинно-ориентированная стратегия логического вывода на основе выполнения операций над кубическими покрытиями.

Розглянута інтерпретація формул числення предикатів першого порядку на кінцевій предметній області за допомогою алгебри кубічних функцій. Запропонована машинно-орієнтована стратегія логічного виведення на основі виконання операцій над кубічними покриттями.

The interpretation of the formula of first-order logic on the finite data domain by means of the algebra of cubic functions is considered. The machine oriented inference method based on execution of operations with the cubic coverings is proposed.