[Zurück]

B. Gramlich:
"On Strategies for Inductive Theorem Proving ";
Vortrag: 5th International Workshop on Strategies in Automated Deduction (STRATEGIES 2004), Cork, Ireland (eingeladen); 04.07.2004; in: "Proc. 5th International Workshop on Strategies in Automated Deduction (STRATEGIES 2004), held in conjunction with IJCAR 2004 (2nd International Joint Conference on Automated Reasoning), Cork, Ireland, July 4, 2004", Eigenverlag, (2004), S. 62 - 63.

Inductive Theorem Proving (ITP) is a challenging field in automated reasoning and theorem proving. Typically, Automated Theorem Proving (ATP) refers to methods, techniques and tools for automatically proving general (most often first-order) theorems. Nowadays, the field of ATP has reached a certain degree of maturity and powerful ATP 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 ATP 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 talk we will try to give a thorough assessment of strategies in ITP and, more generally, of the main structural, conceptual and technical problems and challenges that need to be addressed in order to achieve major progress towards Automated Inductive Theorem Proving (AITP).

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