将投影几何自动证明器集成为 Coq 证明助手中的新策略
计算机科学中的逻辑
2021-07-13 v1 软件工程
摘要
近来，我们开发了一个用于投影关联几何的自动定理证明器。该证明器基于使用拟阵的组合方法，通过拟阵规则的饱和过程进行。它被设计为一个独立工具，用 C 语言实现，以几何构型作为输入，并生成一些 Coq 证明脚本作为输出：预期定理的陈述、证明该定理的证明脚本以及可能的若干辅助引理。在本文中，我们展示如何将此类外部工具作为插件嵌入 Coq 中，使其可用作一个简单的策略。
引用
@article{arxiv.2107.05493,
title = {Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant},
author = {Nicolas Magaud},
journal= {arXiv preprint arXiv:2107.05493},
year = {2021}
}
备注
In Proceedings PxTP 2021, arXiv:2107.01544