Finite Model Generation
Mathematical induction is required for reasoning about objects or
events containing repetition, e.g. computer programs with recursion or
iteration, electronic circuits with feedback loops or parameterized
components. Thus automating mathematical induction is a key enabling
technology for the use of formal methods in information technology.
Failure to automate inductive reasoning is one of the major obstacles
to the widespread use of formal methods in industrial hardware and
software development. In the last ten years, we implemented two
methods based on the approach of proof by
consistency in the prover RRL. We also
developed a method based on the concept of cover
set for mechanizing proofs by explicit induction for equational
specifications. We have used the coverset method for
software verification and hardware verification.
Papers on Automated Induction
System Development

Kapur, D., Zhang, H.: (1995)
An overview of Rewrite Rule Laboratory
.
Journal of Mathematics of Computation.

Kapur, D., Zhang, H.: (1994)
Automated induction: explicit vs.
implicit (abstract)
In Proc. of Third International Symposium on Artificial
Intelligence and Mathematics. Fort Lauderdale, Florida.
The full paper is available upon request.

Zhang, H., Hua, G.X.: (1993)
Proving Ramsey theorem by the cover set
induction: a case and comparison study
.
The Annals of Mathematics and Artificial Intelligence, Volume 8, (1993)
383405.

Hua, G.X., Zhang, H.: (1992)
FRI: Failure Resistant Induction in RRL
.
In Kapur, D.: (ed.): Proc. of 1992 International Conference of
Automated Deduction. Saratoga, NY. Lecture Notes in Artificial
Intelligence, 607, SpringerVerlag. pp. 691695.

Kapur, D., Narendran, P., Zhang, H.: (1991)
Automating inductionless
induction by test sets
.
J. of Symbolic Computation}, 11, 83111.

Zhang, H. (ed.): Automated Mathematical Induction, April 1996, 224 pp.
Kluwer Academic Publishers.

Lee, K., Zhang, H.: (1995)
Formal development of a register allocation algorithm
.
Technical Report, Dept. of Computer Science, UI.

Zhang, H., Hua, G.X.: (1992)
Proving the Chinese remainder theorem by
the cover ste induction
.
In Kapur, D.: (ed.): Proc. of 1992
International Conference of Automated Deduction. Saratoga, NY.
Lecture Notes in Artificial Intelligence, 607, SpringerVerlag.
pp. 431445.

Hua, G.X., Zhang, H.: (1993)
Formal verification of circuit designs in
VHDL
.
In Proc. of 9th International Conference on Advanced Science
and Technology, Motorola, Inc., Schaumburg, Illinois.

Hua, G.X., Zhang, H.: (1992)
Axiomatic semantics of a hardware
specification language
.
In Proc. of the Second IEEE Great Lakes
Symposium on VLSI Design. Kalamazoo, MI. pp. 183190.
Hantao Zhang