[Back]

B. Gramlich:
"Strategic Issues, Problems and Challenges in Inductive Theorem Proving";
Electronic Notes in Theoretical Computer Science (ENTCS) (invited), 125 (2005), 2; 5 - 43.

(Automated) \emph{Inductive Theorem Proving} (ITP) is a challenging
field in automated reasoning and theorem proving. Typically,
\emph{(Automated) Theorem Proving} (TP) refers to methods, techniques
and tools for automatically proving \emph{general} (most often
first-order) theorems. Nowadays, the field of TP has reached a
certain degree of maturity and powerful TP systems are widely
available and used. The situation with ITP is strikingly different, in
the sense that proving inductive theorems in an essentially automatic
way still is a very challenging task, even for the most advanced
existing ITP systems. Both in general TP and in ITP, strategies for
guiding the proof search process are of fundamental importance, in
automated as well as in interactive or mixed settings. In the paper we
will analyze and discuss the most important strategic and proof search
issues in ITP, compare ITP with TP, and argue why ITP is in a sense
much more challenging. More generally, we will systematically isolate,
investigate and classify the main problems and challenges in ITP
w.r.t. automation, on different levels and from different points of
views. Finally, based on this analysis we will present some theses
about the state of the art in the field, possible criteria for what
could be considered as \emph{substantial progress}, and promising
lines of research for the future, towards (more) automated ITP.

(see: English abstract)

http://aleph.ub.tuwien.ac.at/F?base=tuw01&func=find-c&ccl_term=AC05936156