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.