Formal Analysis Oriented To Robot Planning

Robot planning is an important branch of robot domain, it is also an important means of problem solving. In this paper, we use the proving theorem method to formal analyze the robot planning based on the HOL4 (higher-order logic) system. The content below shows the main work of this paper:Firstly, we analyze the robots, the robot planning, the formal method, the theorem proving, and the HOL4 system, and then summarize them.Secondly, we explore the formal modeling and analysis of the STRIPS planning system using a formal method, theorem proving. We summarize the main knowledge of the world model, the F rules and the operation method of the STRIPS planning system. Then, we extract and do the formal modeling of some domain knowledge including the world model and the F rules in STRIPS planning domain, and construct some basic operation functions, and then package all of this knowledge using HOL4. After packaging, the domain knowledge will be shown as an entirety and can be called by any object that wants to use it. Simultaneously, we summarize the general method and flow of the establishment of the STRIPS rules library in HOL4, showing all of the contents and the structure of the STRIPS rules library.Finally, we complete the application of the STRIPS rules library in the verification of related problems of robot planning:a block world planning is illustrated, the reachability of action sequences in block world planning is verified. We have completed the definition and the formal modeling of the IMP and the SPEC, showing the basic idea of modeling, the specific design of formalization and the formal model. We summarize the main idea of verification, and explain how to apply the STRIPS rules library to the verification of related problems of robot planning by showing the verification goal, the process of verification and the results of verification. Our experiments demonstrate that the the STRIPS rules library can effectively solve the problem of repeating the formalization of domain knowledge, and reduce the scale of the verification, and save the time of the verification, and improve the efficiency of the verification.