Loading article…
CADE ATPシステムコンペティション（CASC ）は、古典論理の完全自動定理証明システムの年次コンペティションである[1] [2] [3] [4]
競争
CASCは、自動推論協会が主催する自動演繹会議および自動推論に関する国際合同会議と提携しています。関連分野での同様のコンペティション、特に理論を法とした充足可能性コンペティション[5] 、命題推論システムのためのSATコンペティション[6]、様相論理推論コンペティション[7]の成功に影響を与えました。
最初のCASCであるCASC-13は、1996年にニュージャージー州ニューブランズウィックのラトガース大学で開催された第13回自動演繹会議の一環として開催されました。 [3]競合システムの中にはOtter [8]とSETHEOがありました。[9]
参照
参考文献
- ^ Sutcliffe, Geoff (2011). 「第5回IJCAR自動定理証明システムコンペティション - CASC-J5」. AI Communications . 24 (1): 75–89. doi :10.3233/AIC-2010-0483.
- ^ Geoff Sutcliffe . 「CADE ATP システム競技会」。2009 年 3 月 2 日時点のオリジナルよりアーカイブ。2008 年 10 月 23 日閲覧。
- ^ ab Geoff Sutcliffe および Christian Suttner (2006)。「CASC の現状」。AI Communications。19 ( 1): 35–48。
- ^ Jeff Pelletier、Geoff Sutcliffe、Christian Suttner (2002)。「CASCの開発」(PDF)。AI Communications。15 ( 2–3 ): 79–90。
- ^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). 「SMT-COMP: 理論を法とする充足可能性コンペティション」(PDF) .コンピュータ支援検証. コンピュータサイエンスの講義ノート . 3576 . Springer: 20–23. doi :10.1007/11513988_4. ISBN 978-3-540-27231-1。
- ^ マッティ、ヤルビサロ;ル・ベール、ダニエル;ルーセル、オリヴィエ。サイモン、ローラン (2012)。 「国際SATソルバーコンテスト」。AI マガジン。33 (1): 89–92。土井: 10.1609/aimag.v33i1.2395。
- ^ Massacci, Fabio; Donini, Francesco M. (2000). 「TANCS-2000 非古典的 (モーダル) システムの比較の設計と結果」。分析的タブローと関連手法による自動推論に関する国際会議。コンピュータサイエンスの講義ノート。1847 年。Springer: 52–56。CiteSeerX 10.1.1.385.6267。doi : 10.1007 /10722086_4。ISBN 978-3-540-67697-3。
- ^ McCune, William ; Wos, Larry (1997). 「Otter-the CADE-13 competition incarnations」. Journal of Automated Reasoning . 18 (2): 211–220. doi :10.1023/A:1005843632307. S2CID 2481653.
- ^ Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus (1997). 「Otter-the CADE-13 competition incarnations」. Journal of Automated Reasoning . 18 (2): 237–246. doi :10.1023/A:1005808119103. S2CID 821198.
外部リンク
- オリジナルの CASC ウェブサイトのアーカイブ
- CASCウェブサイト