Reverse parallel deductive reasoning method based on paradox separation formula in first-order logic

Abstract

The invention discloses a reverse parallel deductive reasoning method based on a paradox separation formula in first-order logic. The method comprises the following steps that: constructing a paradoxfor a clause set S in the first-order logic, forming a paradox separation formula R, and judging whether deductive reasoning is terminated or not according to R; if a judgment result shows that the Scan not be satisfied, stopping; otherwise, constructing t pieces of new clause sets by R and S, then, carrying out deductive reasoning on the t pieces of new clause sets to obtain results Rj, and if all results Rj are empty clauses, judging that the S can not be satisfied; and otherwise, circulating the above steps for the new clause set corresponding to the Rj which is not empty, and stopping until the judgment conclusion of S properties or a set condition is met so as to realize a deductive reasoning process. By use of the method, the paradox separation formula can be dynamically decomposed,a dynamic reverse deduction target is formed, the parallel processing of logic formula set property judgment is realized, the deductive reasoning is effectively guided, and the efficiency of the dynamic automatic deductive reasoning based on the paradox separation is improved. The method can be used for fields, including program verification, automated theorem proving and the like.

Description

technical field [0001] The invention belongs to the technical field of automatic deductive reasoning based on logic, and relates to a reverse parallel deductive reasoning method based on the separation of contradictions in first-order logic. Background technique [0002] A large number of scientific problems in the fields of logic, mathematics, system optimization, artificial intelligence, computer science, etc. can be formalized into logical representations. One of the essences of solving these problems is to analyze the attributes of the corresponding logical formulas (satisfiability or unsatisfiability (constant False)), but because of its abstraction, complexity, and scale, it is impossible to effectively implement logical reasoning and solution artificially, so it needs to be automatically judged by a computer. Automatic reasoning is the process of formalizing the reasoning process through a series of symbols, and making the computer automatically perform a series of ca...

AI Technical Summary

Problems solved by technology

Binary resolution selects two clauses with complementary pairs from the clause set S to be determined each time, deletes the complementary pair from the two clauses, and adds the new clauses formed by the disjunction of the remaining words into the atomic sentence set, and repeats as above process, until an empty clause is obtained, it can be determined that the clause set S is unsatisfiable

[0005] Although the automatic reasoning system based on the resolution principle has made many achievements, it is still far from meeting the objective needs in terms of ability and efficiency. Only in the internationally renowned problem bank TPTP in the field of automatic reasoning, there are a large number of the most difficult (Rating 1) problems so far. solve

In the resolution method, because each deduction has and can only have two clauses involved, it cannot reflect the cooperative logical relationship between multiple clauses

The reasoning mechanism of binary resolution seriously restricts the further improvement of the ability and efficiency of automatic reasoning

At the same time, due to the limitation of the binary reasoning mechanism, the binary resolution method lacks the effective guidance and control of the next step of deductive reasoning by dynamically using the deductive results of each step, and it is difficult to parallelize the deductive task decomposition.

Images