The Constructions Of A Parallel Interactive Theorem Prover

It has become more and more important that the application of theorem proving on mathematic theorem proving, protocol verification, hardware verification and software verification. In order to improve the efficiency and the automation of the procedure during proving, various kinds of theorem provers have been developed, falling into interactive or automatic categories.Isabelle is a logic framework used to construct theorem provers. Isabelle/HOL, which came from Isabelle, is a theorem prover with mature functions. The main method used in Isabelle to prove theorems is tactic, which is a program accomplishing one step or many steps of basic deduction. 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. So the main problem in theorem proving in Isabelle is to find a sequence of tactics which can be used to prove a theorem.This paper describes an implementation of a construction of a parallel theorem proving system based on Isabelle. It distributes the proving tasks to some servers running Isabelle in order to prove theorems in parallel. And then discusses several automatic tactics based on it. The main ideas of the tactics is that, for a given set of tactics, the system try to prove a theorem through checking all sequences composed by the tactics in the set in order to prove theorems automatically.