综合几何中命题与证明的自动补全：一种基于约束求解的方法
人工智能
2024-01-25 v1 计算机科学中的逻辑
摘要
猜想和定理证明是数学实践的核心活动，且难以分离。本文提出一个用于补全不完整猜想和不完整证明的框架。该框架可以将带有缺失假设和目标未充分指定的猜想转化为一个恰当的定理。同时，所提出的框架有助于将证明草图补全为人类可读且机器可验证的证明。我们的方法聚焦于综合几何，使用相干逻辑和约束求解。所提出的方法对三类任务统一适用、灵活，并且据我们所知是独一无二的。
引用
@article{arxiv.2401.11898,
title = {Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving},
author = {Salwa Tabet Gonzalez and Predrag Janičić and Julien Narboux},
journal= {arXiv preprint arXiv:2401.11898},
year = {2024}
}
备注
In Proceedings ADG 2023, arXiv:2401.10725