深度分析 可驗證的多項式到達遊戲求解:排序證書、模板合成與半完備性分析 本論文針對無限狀態的到達遊戲,提出一種稱為「排序證書」的新型數學證明規則,可證明 REACH 玩家具有必勝策略。作者把問題限定為以多項式約束描述的遊戲,提出模板化的自動化合成演算法,並以 PolyQEnt 轉譯、Z3 與 MathSAT5 作為後端 SMT 求解器實作。