## 抄録

In many automated methods for proving inductive theorems, finding a suitable generalization of a conjecture is a key for the success of proof attempts. On the other hand, an obtained generalized conjecture may not be a theorem, and in this case hopeless proof attempts for the incorrect conjecture are made, which is against the success and efficiency of theorem proving. Urso and Kounalis (2004) proposed a generalization method for proving inductive validity of equations, called sound generalization, that avoids such an over-generalization. Their method guarantees that if the original conjecture is an inductive theorem then so is the obtained generalization. In this paper, we revise and extend their method. We restore a condition on one of the characteristic argument positions imposed in their previous paper and show that otherwise there exists a counterexample to their main theorem. We also relax a condition imposed in their framework and add some flexibilities to some of other characteristic argument positions so as to enlarge the scope of the technique.

本文言語 | English |
---|---|

ホスト出版物のタイトル | FSTTCS 2008 - IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science |

ページ | 13-24 |

ページ数 | 12 |

巻 | 2 |

出版ステータス | Published - 2008 12月 1 |

イベント | 28th International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008 - Bangalore, India 継続期間: 2008 12月 9 → 2008 12月 11 |

### Other

Other | 28th International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008 |
---|---|

国/地域 | India |

City | Bangalore |

Period | 08/12/9 → 08/12/11 |

## ASJC Scopus subject areas

- ソフトウェア