An Algebraic Method to Identify Classes of Formulas in Calculus of Predicates

Abstract

The P-complete problem of logic deduction in classical propositional and first order predicate calculus is considered. The suggested method is alternative to the traditional methods of direct and inverse logic deduction in particular to the Robinson’s resolution principle. The deterministic algorithm of polynomial complexity based on Boolean algebra of cubic functions for differentiation between two classes of formulas: valid and satisfiable, or unsatisfiable and satisfiable, is suggested.

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