Mechanical identification of inductive properties during verification of finite state machines

This paper describes a method to verify a finite state machine by theorem proving. For some instances, inductive reasoning comes in handy to support the proof of verification. In this work the theorem prover itself tries to find out the properties on which induction needs to be applied. A short account of the proof procedure which is based on goal directed backward reasoning is given. A nontrivial example is presented to illustrate the approach. A proof construction algorithm has been provided