Design And Implementation Of Automation Proving Tactics In Isabelle

The theorem machine prove is an important research area of the artificial intelligence, being applied in mathematics theorem proving, protocol verification, software and hardware of formal verify and so on consequently it is in the interest of the artificial intelligence group to improve the efficiency of theorem machine proving. So, various kinds of theorem proves have been developed, mainly falling into interactive or automatic categories.Isabelle which abbreviates Isabelle/Isar/HOL is based on higher order logic interactive parallel theorem prove. It is a generic theorem proving environment developed at Cambridge (Larry Paulson) and TU Munich (Tobias Nipkow).The main method of theorem proving is a tactic in Isabelle, The process of constructing a proof is to choice a tactic by the user and then to execute the tactic on a computer repeatedly until the proof is complete.On the basis of analyzing most basic proof tactics in Isabelle, we designed a system of parallel automated proof tactics by embedding the control block in Isabelle. The block explains and implements parallel tactics. Running environment of this system is the parallel computers or the microcomputer cluster which supports MPI programming standard. The system is made up of a lot of parallel Isabelle processes. The main process lies in user's computer, and the server process lies in the selected cluster. The main process is responsible to control whole parallel programs. It assigns missions to other processes. Then the other processes send the results to the main process.