Abstract. The parallel resolution procedures based on graph structures method are presented. OR-, AND- and DCDP- parallel inference on connection graph representation is explored and modifications to these algorithms using heuristic estimation are proposed. The principles for designing these heuristic functions are thoroughly discussed. The colored clause graphs resolution principle is presented. The comparison of efficiency (on the Steamroller problem) is carried out and the results are presented. The parallel unification algorithm used in the parallel inference procedure is briefly outlined in the final part of the paper.

Keywords: Automated Reasoning, Logical inference

ACM Classification Keywords: I.2.3 Artificial Intelligence: Deduction and Theorem Proving

Link:

THE DEVELOPMENT OF PARALLEL RESOLUTION ALGORITHMS USING THE GRAPH REPRESENTATION

Andrey Averin, Vadim Vagin

http://www.foibg.com/ijita/vol13/ijita13-3-p10.pdf