在 Isabelle/HOL 中由表反转映射诱导的表对称事实的自动生成
计算机科学中的逻辑
2022-05-10 v2
摘要
许多事实具有对称的对应事实，往往需要根据所涉及对称性的性质进行单独的正式证明。我们在 Isabelle/HOL 中引入了一种方法，可为表数据类型以及由表反转映射所诱导的对称性生成此类对称事实。该方法作为一个属性实现，其结果基于用户声明的对称规则。除通用规则外，我们还提供了旨在组合词（Combinatorics on Words）领域中应用的规则。
引用
@article{arxiv.2104.11622,
title = {Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL},
author = {Martin Raška and Štěpán Starosta},
journal= {arXiv preprint arXiv:2104.11622},
year = {2022}
}
备注
accepted at FMM 2021