#verification

Li et al.: 記号ソルバーを審判にして幾何問題を「検証可能」に解く — Fukai が読む

Can Li らによる幾何問題解決(GPS)の arXiv プレプリント。図と文の問題を記号ソルバーが実行できる形式へ翻訳し、行き詰まりでは補助的な補題を提案してソルバー自身に検証させる SD-GPS を提案。要旨によれば Geometry3K・PGPS9K で既存手法を一貫して上回ったという。解けることを保証するパズル生成への応用を Fukai が読む。