CSE-MTECH-04-030




Lemma Generation in Inductive Theorem Proving
Abhijit Toley, M.Tech, 04, 77 pp.
Department of Computer Science and Engineering
Indian Institute of Technology Bombay, Powai, Mumbai 400 076.
Supervisor(s): G.Sivakumar

The dissertation presents a new heuristic to generate intermediate lemmas in inductive theorem proving. When a proof attempt based on cover set induction gets stuck, this heuristic applies ``backward reasoning'' (i.e. lifting of subterms using the rules given in the definitions from right to left) to generate possible lemmas that are sufficient to complete the proof. Simple feasibility checks are given to prune the suggested lemmas. We give some examples of theorems not provable directly earlier, for which our method automatically generates interesting provable lemmas which complete the proof. An implementation of the heuristic is given as pseudo code. The heuristic and the required framework for it to be applicable has been implemented in Common Lisp and has been incorporated in the theorem prover RRL. Capabilities of RRL and its limitations were highlighted by a few examples and some progress has been made in overcoming the limitations. Future possibilities are highlighted towards the end of the dissertation.