特徴
Paradoxの開発者は、このソフトウェアを、McCuneの同名のツールにちなんで、モデルと反例（Mace）スタイルの手法であると説明した。 [ 5 ] [ 6 ] Paradoxは、モデル探索問題の計算複雑性を軽減するのに役立つ新しい技術を導入した。[ 5 ]
- 用語の定義– 新しい変数削減方法
- 段階的充足可能性チェッカー– 最初は小さなドメインで動作し、その後、以前の失敗した検索から得られた情報を再利用しながら、ドメインサイズを徐々に大きくします。
- 静的対称性の低減– 追加の制約を加える
- ソート推論– ソートされていない問題に対応
Paradoxはバージョン4まで開発され、最終バージョンはWeb Ontology Language OWL2のモデル検索に効果的であった。[ 7 ]
参考文献
- ↑ 「パラドックス」。チャルマース工科大学。2007年1月8日のオリジナルからアーカイブ済み。 2007年5月26日取得。
- 1 2 Pudlák, Petr (2007 年 7 月 17 日). "自動定理証明のための前提のセマンティック選択" (PDF) . In Urban, J.; Sutcliffe, G.; Schulz, S. (eds.). Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories . The 21st International Conference on Automated Deduction. CEUR Workshop Proceedings. Vol. 257. Bremen. pp. 27– 44. ISSN 1613-0073 . S2CID 16318678 . 2018 年 11 月 7 日のオリジナル(PDF)からアーカイブ済み. 2011 年11 月 7 日取得.
- ↑ 「応募者のシステム説明」。マイアミ大学。Paradox 3.0。2018年11月7日にオリジナルからアーカイブ済み。 2018年11月7日に取得。
- ↑ 「パラドックス」。チャルマース工科大学。2007年1月15日のオリジナルからアーカイブ済み。 2020年4月30日取得。
- 1 2 Claessen, Koen; Sörensson, Niklas. "MACE スタイルの有限モデル探索を改善する新しい技術" (PDF) . S2CID 15694927 . 2018 年 11 月 11 日にオリジナル(PDF)からアーカイブ済み . 2018 年11 月 11 日に取得.
- ↑ 「自動定理証明」(PDF)。オーストラリア国立大学工学部・コンピュータサイエンス学部。73 ～ 74ページ。2018年11月11日にオリジナルからアーカイブ(PDF) 。 2018年11月11日に取得。
- ↑ Schneider, Michael; Sutcliffe, Geoff (2011). "OWL 2 Full Ontology Languageにおける一階自動定理証明を用いた推論". arXiv : 1108.0155 [ cs.AI ].
- ↑ 「CADE ATPシステムコンペティション - 自動定理証明の世界選手権」。過去のCASC部門優勝者。2018年9月1日にオリジナルからアーカイブ済み。 2018年11月7日に取得。
