تقرير
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
| العنوان: | Template-Based Conjecturing for Automated Induction in Isabelle/HOL |
|---|---|
| المؤلفون: | Nagashima, Yutaka, Xu, Zijin, Wang, Ningli, Goc, Daniel Sebastian, Bang, James |
| سنة النشر: | 2022 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science |
| الوصف: | Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluation shows that our working prototype, TBC, achieved 40 percentage point improvement of success rates for problems at intermediate difficulty level. Comment: To appear at Fundamentals of Software engineering 2023 (http://fsen.ir/2023/) |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2212.11151 |
| رقم الأكسشن: | edsarx.2212.11151 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |