(Continued article "Machine Proof Introduction (1)")
The machine proves that a starting point is "reasonable", but this road is not flat. Mathematical logic is exploring the symbolicization of thinking, computer scientists are also exploring the capacity limit of the computer itself. A generation of people, in thinking, human wisdom of the wisdom; how to do this, how to do better, and even as human beings?
The last time, the proof of this formula: ┣ (α → β) → (α α) Its proof sequence is simple, as follows: (1) α → (β → α) (A1) (2) (α → (α → β → α)) → ((α → β) → (α)) (A2) (3) (α → β) → (α → α) (m) (1) (2)
When I introduced the process of proved the formation of the idea, I used the word "eye-catching", but it is not good in science, this description is not good. On this issue, Mr. Zhang Jingzhong has discussed the extension of human prove to the process of geometric theorem and the process of machine certification. I am expanded that as follows: (1) Test: Observe and calculate all known conditions to determine propositions (2) Search: Find more information based on existing (commonly used) ores, if these results cannot achieve their goals; (3) Regions: Departure, use known information to eliminate certain amounts and conditions dependent, so that true and false conclusions tend to be obvious or easy to test; (4) Transformation: Change the form of propositions;
The machine simulation of the means (1) has been implemented. The study of the means (3) has achieved the greatest success, and Mr. Wu Wenjun's geometric theorem has a method, it belongs to this class. (2) It is a comparative and conventional means of conventional conventional regulations. The means (4), fully reflect the flexibility and richness of human thinking, and is still difficult to mechanize.
The idea of the above example can reflect these conclusions. However, there is no doubt that even the perfect mechanization of the means (4), we also need our further effort; let alone, I want the machine to prove that the place to be developed is far more than one.
So, let us start along the historical footsteps, let's take a detailed test method, computer-aided proof, judgment method, and proof algorithm, etc., I hope we can feel wonderful interests. And have fun. Le Zhi is my purpose, but if you are ready to check the information, I want to go deep, I will dance.
1. Test method uses the test method to proof the agencies, which can be sent from premise, or from conclusions. From the premise, several propositions are launched by the premise (including the axiom, definition, proven theorem, and the assumptions of the theorem to prove) to introduce several propositions as an intermediate conclusion; then add the intermediate conclusions to the premise, and launched a number Intermediate conclusion. In this way, if the conclusions have been launched, theorem has been proved that otherwise, additional intermediate conclusions are launched from the other prodigroups, and the proof is introduced to the proof theorem. From the conclusions, it is to consider what kind of proposition can launch the conclusions to deal with these propositions; similar to the above process, if the proactive premise includes the proposition required, theorem is certified, otherwise An additional way is still required. Try is a means that it is only possible to obtain a problem, but it does not guarantee that it can be obtained. Moreover, before the theorem gets prove, we can't affirm it is not proven. In history, NEWELL-Shaw-Simon has proved the reputation of the proposition logic. The form of the system they use is not a natural reasoning system, but a reply system, that is, the proposition inference system P in the last introduced. Below is their tempering method: A is a formal aimation to be proven, regarding A as a problem to solve. The first step, the test is set into rules. For example: can be launched by α → (β → α): α → (α → β) → α), (α → → → → → → →)), if it can be stored in a regular rule A formatizer in the formal cell form (including formal axict) launches A, demonstrates the end; otherwise, the rule is invalid, and go to the next step. In the second step, the test separation rules. Find the formula in the form of (b → a) in the formatter form. If there is, the problem is that the proof A is approximately approximately proof B, B is called a sub-problem. Then use B test to enter the rule to prove that if B can be proven, then the proof of A ends, otherwise send B to the "child problem table". So continuing the test separation rules, if the formula in the form of (B → a) is not found, transfer to the next step. In the third step, the test contains the word transfer rules. Implication Word Passage is not part of the definition, it can be defined prove, but it is very useful, specifically, α → β, β → r┣α → r (TR) specific method is, first check A is implication, if No, the third step is not performed, so I take the next formula in the sub-problem table, turn the second step; if A is the implication, for example, there is a formula in the form of B → D, then find B → C in the formatter table Or the formula of C → D, if the formula in the form of B → C is found, the problem is demonstrated to a (ie B → D) to demonstrate C → D, and if the formula in the form of C → D is found, the problem is contracted To prove B → C. B → C or C → D is a sub-problem, so that it is performed to the rule certificate. If this proves succeeded, then the end, otherwise the sub-problem is stored in the sub-problem table, continue to look for B → C or C → D form formula in the formati table, and repeated the process of repeating, if not found, then The next formula is removed in the child problem table and transferred to the second step.
During the process of proof A, the shutdown condition is one of the following four cases: A is proved; the machine time is used; the machine memory is used; the formula in the child problem is used. Therefore, when the proof process ends, A is not necessarily certified. Wang Hao, a famous mathematical logic, gave an algorithm, more than this temple method to be simple, proved hundreds of the prodigal logic in the "Mathematics Principles" of Russell, only 9 minutes. This is a far-reaching work. Interested in-depth readers can check the references provided by Note 2.
Today, our journey, this time we will follow today's footprints. I am enthusiastic about your concern about theoretical science.
Note 2: [Wang Hao]. Toward Mechanical Mathematics, IBM Journal, IBM Journal, IBM, 4,224-268,1960
This article reference materials:
1, [Lu Zhong Wan]. Mathematical Logic and Machine Proof. Scientific Press, 1983
2, [Zhang Jingzhong]. Profit research on the geometric theorem machine. The second phase of the Chinese Academy of Sciences, 1997
