Formalization Of Graph Theory In Theorem Prover HOL4

With the large scale and complexity of computer system design,the security of the system is also severely tested.Formal method in system design verification using mathematics method,compared with the traditional program to test with higher reliability and completeness,the theorem proving method can not only make up for a lack of traditional test in the process of system verification,validation of system more perfect,and can deal with infinite state space of system verification work.Graph theory is an important branch of mathematics,which has been widely used in aerospace,electric power,communication and other systems with high security requirements.However,at present,there is no formal theory library of graph theory in the theory library of theorem prover HOL4,which limits the application of theorem prover HOL4 in graph theory related fields.Therefore,formalizing graph theory in theorem prover HOL4 has important research significance and practical value.This paper for the first time in the theorem prover HOL4 to formal work of graph theory,including in the system to establish the basic data types of figure,and the complete graph modeling on the basis of the basic data type in the directed graph theory basic figure types,operation of figure,figure,edge and vertex degrees path,the subgraph and so on five parts related to the definition of the modeling work,Then the related properties contained in the definition modeling are formally verified,and the directed graph theorem library of graph theory is established for the first time in the theorem prover HOL4.At the same time to illustrate the use of directed graph theorem libraries have established methods,therefore will have to establish library directed graph theorem is applied to the depth first search algorithm and breadth-first search algorithm modeling and termination of the theorem prover HOL4 as proof,and established the validity and the practicability of the directed graph theorem library,to further promote the development of the HOL system,So that the formal method can solve more practical problems.