Algorithm for Extracting the Common Properties of Objects Described in the Predicate Calculus Language with a Single Predicate Symbol

In artificial-intelligence problems, connected with the study of complex structured objects which are described in the terms of properties of their elements and relationships between these elements, it is convenient to use predicate-calculus formulas, more precisely elementary conjunctions of atomic predicate formulas. In such a case, the problem of extracting the common properties of objects arises. The common properties of complex structured objects are set by formulas with variables as arguments, which, up to the names of the arguments, coincide with the subformulas of the objects under study, that is, are isomorphic to these subformulas. In the case of a single predicate symbol in the descriptions of objects, the problem under consideration is polynomial equivalent to the NP-hard problem of extracting the largest common subgraph of two graphs. An algorithm for finding the largest (in terms of the number of literals) subformula with variables as arguments, isomorphic to the subformulas of two elementary conjunctions of predicate formulas containing a single predicate symbol is proposed in this work. Estimates of the computational complexity of the proposed algorithm are proved. The algorithm is implemented in Python.