离散数学证明中表示的自动化变换
人工智能
2015-05-12 v1
摘要
表示决定了我们如何推理一个特定问题。有时一种表示比其它表示更帮助我们轻易找到证明。当前大多数自动化推理工具聚焦于在单一表示内推理。因此，需要开发更好的工具来机械化和自动化形式化且逻辑合理的表示变更。在本文中，我们考察离散数学中表示变换的例子，并展示我们如何使用 Isabelle 的 Transfer 工具来自动化这些变换在证明中的使用。我们简要概述了我们认为适于思考该问题的一般变换理论，并解释它如何与 Transfer 包相关联。我们展示了在开发通用策略方面的进展，该策略在证明过程中融入表示的自动搜索。
引用
@article{arxiv.1505.02449,
title = {Automating change of representation for proofs in discrete mathematics},
author = {Daniel Raggi and Alan Bundy and Gudmund Grov and Alison Pease},
journal= {arXiv preprint arXiv:1505.02449},
year = {2015}
}