Loop-Detection in Hyper-Tableaux by Powerful Model Generation
Дата
Авторы
Stolzenburg,Frieder
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
Automated reasoning systems often suffer from redundancy: similar parts of derivations are repeated again and again. This leads us to the problem of loop-detection, which clearly is undecidable in general. Nevertheless, we tackle this problem by extending the hyper-tableau calculus as proposed in [Baumgartner, 1998] by generalized terms with exponents, that can be computed by means of computer algebra systems. Although the proposed loop-detection rule is incomplete, the overall calculus remains complete, because loop-detection is only used as an additional, optional mechanism. In summary, this work combines approaches from tableau-based theorem proving, model generation, and integrates computer algebra systems in the theorem proving process.
Ключевые слова
hyper-tableau , loop-detection , terms with exponents , computer algebra systems , model generation.