Abstract:
The problem of deducibility checking for a special form formula is under consideration. Many Artificial Intelligence problems may be reduced to such a form formulas. To solve this problem it is suggested to use a combination of the inverse Maslov method with Ant algorithms permitting concurrent processing during the derivation construction. Algorithm solving such a problem is constructed. This algorithm run bounds of step number are proved. An example of a model problem solving with the help of the described algorithm is described. Refs 7. Figs 2.