Talk about the evolution of calculating ideas to make machine proves and reasoning ideas [2]
Preliminary division of the operation of evolution and reasoning and the type of evolution
Nature is natural to be good. Now that we are close to the core questions, how to apply the ideas of evolutionary calculations to machine certificates and reasoning.
We look at several examples of proof, there will be a good revelation.
Example 1 α, β is a formula in Kφ, proves: ├ (α → β) → (α → α).
prove
(1) α → (β → α) (k1)
(2) (α → (β → α)) → ((α → β) → (α)) (K2)
(3) (α → β) → (α → α) (m) (1) (2)
This proof process is very simple, the axiom (K1) and (K2) should be that our evolution proof is provided after the initialization of the reasoning system, which can prove the conclusions we need. In general, we take the formula tree of two different families to evolve, it is expected to get the target formula tree, such a evolutionary process, we call it a family to evolve.
Example 2 α is a formula in kφ, proves: ├α → α.
prove
(1) α → ((β → α) → α) (k1)
(2) (α → (β → α) → α) → ((α → (β → α)) → (α → α))
(K2)
(3) (α → (β → α)) → (α → α) (m) (1) (2)
(4) α → (β → α) (k1)
(5) α → α (m) (3) (4)
This proof is slightly complicated, and the entire procedure is expanded from the formula (1). How to find (1) in the formula is the key to prove. Traditional methods, it is difficult to realize (1), but in our evolution proof and reasonce, see (1) is very natural, because the formula and (4) in (1) are the same family, we Simply change the β node of the formula tree corresponding to the β → α node, notice that the flag set of the formula tree has not changed, and this evolutionary process, we call it a family to evolve. Therefore, if it is proved by evolutionary proof and reasoning, the successful trajectory will be like this:
(1) Family evolution for family (K1);
(2) According to (1), the family (K2) is evolved in the family;
(3) Family evolution by (1) and (2);
(4) The formula tree introduced into the family (K1);
(5) Family evolution and success by (3) and (4).
It can be seen that the design of the evolution process and the strategy will be complicated and critical, which is one of our future work.
Example 3 α, beta is a formula in Kφ, proves: Ø (α → β) Ø Øβ.
analysis
The proven of this proposition is quite complicated, and we simply give the analysis process.
Considering the known formula tree contains α → beta tree, we have the following family evolution results:
(1) β → (α → β) (k1)
We have a tendency to Ø. In the future, design more than one of our empowerment is also one of our work. If we know the following internal theorem:
(2) (α → β) → Ø Ø (α → β)
(3) Ø Ø ø → → β
Then we evolve between family, you can get:
(4) Ø Ø ø β → Ø Ø (α → β) (Tr) (1) (2) (3)
Introduction:
(5) (Ø Ø ø β → ø Ø (α → β)) → (Ø (α → β) → Ø β) (K3)
The evolution of the family can be obtained:
(6) Ø (α → β) → Ø ø β (m) (4) (5)
A known:
(7) Ø (α → β)
Then we successfully prove the proposition:
(8) Ø Ø ø β (m) (6) (7) This process gives us a envelope.
First, the inner sequence
├ Ø øα → α and ├α → Ø Øα,
It can be further proven, we introduce them, indicating that our evolution proof and reasoning system should record the commonly used internal theorem in time, and use in the new proof in the process of reasoning.
Secondly, for linkages, the reasoning process should have a rich tendency, although evolution is random, but we give a certain evolutionary tendency, convergence speed will greatly improve.
Finally, (6) and (7) evolution is a new way of evolution, because their formula trees are not any family, so that the evolution of the formula tree we call the group is a group evolution. The family's evolution and family evolution can be collectively referred to as a family evolution. Group evolution and family evolution is interacting with each other, but in general, the former is more flexible than the latter. Designing this interaction and interaction will be the core of our future work.
The introduction of the above internal sequence is in the form system Kφ, but in the physicalist logic, formula
Ø Øα → α
It is not an internal orientation. Our evolution proof and reasoning system must be developed in accordance with the content of the form system during software design. Below we consider an example of other logical morphology, select a simple example of modal logic. The form system is system K.
Example 4 α is the formula of K, prove: □ α↔ Ø ◇ øα.
prove
(1) α ↔ Øøα THP15
(2) □ α ↔ Øø □ □ (1) × Sb
(3) □ α ↔ ØØ □ Ø Øα (2) (1) × RES
(4) □ ↔ ↔ Ø ◇ Øα (3) (d ◇) × RES
This proof process shows that the concepts and principles of our discussion above are effective here. The method of evolution proof and reasoning is a basic method.
In summary, evolution proof and reasoning is a good entry point in formalization process. Basically, the type of evolution process can be divided into:
This has a large number of design work, which has been mentioned in the above analysis, but in the process of actual evolution computing and machine certification and reasoning, there are certain problems we don't realize. Therefore, in theory, with the software system, we have to work harmonize. The atrial innovation is carried out and the test is accepted.
Outlook and reasoning of the evolution and reasoning
I have been thinking about when the machine can know the personnel. The large scale scientific operation is handled by non-numerical data, and the computer can do it. However, knowing the subtleness of people, it seems to be the penalty area of the machine. Artificial intelligence is slowly developed; human computing power, computer has exceeded, but human association, innovation ability, computer did not learn.
If the evolution of the computer is feasible, it is hoped to break through this. The thinking of evolution is uncharged, with broad vision and self-organizing, self-optimization, which can supplement the lack of conventional machine certification and reasoning methods. So, let's see the picture below:
In the figure, 1 is based on the evolutionary proof and reasoning model of the form system. 2 is a generic evolutionary proof and reasoning model. 3 is the semantic model of evolution and reasoning, 5 is the identification and understanding of human activities, 4 is unknown transition model. This system is described below, as mentioned above, is composed of five models, trying to help computer identify personnel.
Based on the evolutionary proof and reasoning model of the form system, it is a model that this article focuses on the discussion, and it is also the point of work.
The formal system can have a rich semantic explanation, but the formal system does not cover all of human knowledge, thoughts, so we are eager to find a new model, but also based on the evolutionary thinking, to simulate the broader thinking activities of humans. . We are temporarily called generic evolution proof and reasoning model.
1 Follow the "Strict Formal Principles", but for 2, we said, follow another principle, we call it "Fuzzy not in violation of the environmental principle". For example, during the different evolution of the formal system and the different evolution of the reasoning model, in particular the process of group evolution, a large number of formula trees will produce a large number of formula trees, we will discard it, but we will discard it; but in generic evolution proof In the reasoning model, as long as we take certain environmental factors, we reserve the proposition. The direction is different, but the opposite is the most tightly combined in five models, which is the kernel portion of our system.
The evolution proof and reasoning semantic model is the semantic implementation of the kernel.
The identification and understanding of human activities is the model of various branch disciplines of artificial intelligence, such as natural language understanding and processing models, computer visual understanding and processing models. This model is not directly and evolution proof of linking with the semantic model of reasoning. Because this cause is so tough, the establishment of each model is to fight. For example, natural language understanding and processing, I have seen the best model, is the HNC theory of Huang Zengyang, Chinese Academy of Sciences. Since it is the battle, the model of HNC theory is relatively independent, we can't take into account mutual needs, such as complexity is too large. So, in the future, we need an unknown transition model to complete their connection to connect to the internal connection.
This is what our 4 (transition model) exists.
When one day we went to unity, that is, when the system of Figure 5 is relatively perfect, our computer will have human characteristics. Artificial intelligence, even if it is really a big step.
This work is meaningful, but it is also difficult. We will start with 1 (based on the evolutionary certificate and reasoning model of form systems), and do the instinct theoretical innovation and practice inspection. This process will also be repeated, and our software has the following stages, we need to do reviews in the following stages:
(1) The basic establishment of the system and the proof of partial formula;
(2) Optimization and system expansion of the evolution process;
(3) The evolution proof based on the form system is basically completed.
There is no doubt that we will continue to do it. It can be seen that we are currently thinking that this program is effective; but we hope to prove by practice, evolutionary proof and reasoning is effective or invalid.
<2003-9-25 Reported from Wuhan>
Reference:
(1) Zhou Beihai, "Modal Logic", China Social Science Press, 1996.
Finished>
------------------------------------------
Disclaimer: This article keeps all rights, if you have any suggestions, please send it to percylee@126.com
