ベンチマークと競技会
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/05/28 07:09 UTC 版)
「自動定理証明」の記事における「ベンチマークと競技会」の解説
実装システムの品質は標準ベンチマーク例の大きなライブラリ Thousands of Problems for Theorem Provers (TPTP) の存在によって高められている。また、Conference on Automated Deduction(CADE) 主催の ATP System Competition (CASC) は一階述語論理システムの競技会であり、これもシステムの品質向上に寄与している。 以下に主なシステムを列挙する（いずれも少なくとも1回は CASC で優勝している）。 E は Purely Equational Calculus に基づいた高性能証明機。ミュンヘン工科大学の自動推論グループが開発した。 Otter はアルゴンヌ国立研究所で開発された世界で初めて広く使われた高性能証明機である。導出と導出における統合推論に基づいている。Otterの後継としてen:Prover9Prover9とMasce4がある。 SETHEO はゴール指向の model elimination 法に基づいた高性能システム。ミュンヘン工科大学の自動推論グループが開発した。E と SETHEO は統合され、E-SETHEO となった。 Vampire はマンチェスター大学の Andrei Voronkov と Krystof Hoder が開発・実装した。かつては Alexandre Riazanov も参加していた。定理証明機のワールドカップ（the CADE ATP System Competition）の最高の CNF (MIX) 部門で7年間優勝している（1999年、2001～2006年）。 Waldmeister は unit-equational な一階述語論理に特化したシステムである。10年間にわたって CASC UEQ 部門で優勝している（1997年～2006年）。 SPASSは等号を含む一階述語論理の定理証明機である。マックス・プランク研究所が開発した。
※この「ベンチマークと競技会」の解説は、「自動定理証明」の解説の一部です。
「ベンチマークと競技会」を含む「自動定理証明」の記事については、「自動定理証明」の概要を参照ください。
- ベンチマークと競技会のページへのリンク
