Automated Planning Techniques for Elementary Proofs in Abstract Algebra

要約

この論文では、数学的証明を構築するためのアルゴリズムとコンピューター プログラムの開発に関係する自動推論の一部門である自動定理証明への自動計画の適用を検討します。
特に、私たちは、群、環、体、加群などの代数構造を研究するための厳密で公理的な枠組みを提供する抽象代数における初等証明を構築するための計画の使用を調査します。
決定論的領域と非決定論的領域の両方で基本的な含意、等式、ルールを実装して、可換環をモデル化し、それらに関する基本的な結果を推定します。
この初期実装の成功は、自動計画で見られる確立された手法が自動定理証明の比較的新しい分野に適用できることを示唆しています。
同様に、自動化された定理証明は、自動化された計画に新たな挑戦的な領域を提供します。

要約(オリジナル)

This paper explores the application of automated planning to automated theorem proving, which is a branch of automated reasoning concerned with the development of algorithms and computer programs to construct mathematical proofs. In particular, we investigate the use of planning to construct elementary proofs in abstract algebra, which provides a rigorous and axiomatic framework for studying algebraic structures such as groups, rings, fields, and modules. We implement basic implications, equalities, and rules in both deterministic and non-deterministic domains to model commutative rings and deduce elementary results about them. The success of this initial implementation suggests that the well-established techniques seen in automated planning are applicable to the relatively newer field of automated theorem proving. Likewise, automated theorem proving provides a new, challenging domain for automated planning.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google