تقرير
Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
| العنوان: | Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL |
|---|---|
| المؤلفون: | Raška, Martin, Starosta, Štěpán |
| سنة النشر: | 2021 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science, 03B35, 68R15, 68V20, 68V15, D.2.4 |
| الوصف: | Many facts possess symmetrical counterparts that often require a separate formal proof, depending on the nature of the involved symmetry. We introduce a method in Isabelle/HOL which produces such a symmetrical fact for the list datatype and the symmetry induced by the list reversal mapping. The method is implemented as an attribute and its result is based on user-declared symmetry rules. Besides general rules, we provide rules that are aimed to be applied in the domain of Combinatorics on Words. Comment: accepted at FMM 2021 |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2104.11622 |
| رقم الأكسشن: | edsarx.2104.11622 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |