Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving

要約

推測と定理の証明は数学的実践の中心となる活動であり、分離するのは困難です。
この論文では、不完全な推測と不完全な証明を完了するためのフレームワークを提案します。
このフレームワークは、前提が欠落していたり​​、目標が不十分に指定されている推測を、適切な定理に変えることができます。
また、提案されたフレームワークは、プルーフ スケッチを人間が判読可能で機械チェック可能なプルーフに完成させるのに役立ちます。
私たちのアプローチは合成幾何学に焦点を当てており、一貫したロジックと制約解決を使用します。
提案されたアプローチは、3 種類のタスクすべてに対して均一であり、柔軟であり、私たちの知る限り、そのようなアプローチはユニークです。

要約(オリジナル)

Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google