| Abstract: | Conclusion This paper offers an effective resolution method for checking the satisfiability of a collection of disjuncts in the languageL. The method permits one to substantially reduce the number of generated resolvents in comparison with the method ofR-resolution. One more factor ensuring the efficiency of the method is a significant reduction in the number of disjunct pairs checked for the possibility of resolving them. As for the number of generated disjuncts, its greatest reduction is obtained in the case of the use of the disjunct-set partition corresponding to the limiting system of predicate-symbol subsets given by symbol ordering. It is possible to interpret the result obtained for this case as proof of the completeness of the strategy combining an ordering of predicate symbols andR-resolution. It is necessary to note that to different orderings of predicate symbols correspond different partitions of the disjunct set giving, in turn, different numbers of generated disjuncts in the process ofSp-completion. Nevertheless, the methods described in Sec. 2, which use partition of the disjunct set into two classes, are of independent importance. As has already been said, completion of a disjunct set is used for solution of a number of problems during the design of a procedural automaton specification. For example, in the case of checking the consistency of two interacting automata [5] based on completion of a disjunct set, there exists a natural partition of the predicate symbols into input and output symbols, to which corresponds the partition of the disjunct set into subsets specifying the interacting automata. Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 13–20, November–December, 1998. |
