Z3とcoqの違いを教えてもらえますか?私には、coqは、ユーザーに証明ステップを記入する必要があるという点で証明補助者であると思われますが、Z3にはその要件がありません。しかし、coqもZ3と同様の自動戦術を持っているようですね?あるいは、coqの証明検索能力がZ3ほど強力でないかもしれませんか?Z3とcoqの相違
答えて
Coqは、対話式定理証明(aka proof proof assistant)です。それは、数学的な定義、アルゴリズム、定理を書くための言語を提供します。また、マシンチェックプルーフを作成する環境も提供します。 Coqは、数学の定理を形式化し、プログラミング言語の意味を提供するために使用されてきました。今日では、Coqを使ったPOPLで多くの論文を見つけることができます。将来Coqなどのシステムが数学者によって広く使用されると主張する人もいます。 articleには、数学の正式な証明のための説得力のある議論があります。最近、Georges Gonthier は、4色定理の測量可能な証明を作成するためにCoqを使用しました。 Coqは信頼できるコアが小さく、高い保証を提供します。
Z3はSMT(充足可能性モジュロ理論)ソルバです。その言語は、多くのソートされた1次論理+算術、ビットベクトル、データ型、配列などの理論です。この言語は、Coqで使用されているものほど表現力がありません。 Z3はまたCoqのような証明管理のためのサポートを持っていません。 Z3は主にソフトウェアのテストと検証に使用されます。また、制約、計画問題、パズルなどを解決するために使用することもできます。 満足できる公式のためのモデル(すなわち、解)を見つけることには非常に重点があります。 articleには、Microsoftや他の多くのZ3アプリケーションが記述されています。 Z3は本質的に自動定理証明である。 Z3では、戦術を使用してdomain specific strategiesを指定します。つまり、特定のアプリケーションドメインの問題に対するカスタマイズされたソルバーです。 Z3は、独立してチェックできる証明書/証明書を作成することができます。しかし、証明生成はZ3プロジェクトの主な焦点ではありません。さらに、多くのモジュールはプルーフプロダクションをサポートしていないため、プルーフ生成がユーザによって要求されたときは無効にする必要があります。 Z3はまた、Isabelleのような証拠アシスタントに統合されており、Z3はCoqにZ3を統合するために取り組んでいます。そのアイデアは、非常に表現力豊かな言語と非常に優れた自動化の両方の世界を誇ることです。 Z3は、より大きなアプリケーションに組み込むことができるロジック推論エンジンとして見ることもできます。実際、これまでのすべてのZ3アプリケーションでそうです。エンドユーザーはZ3を直接使用しません。それはIsabelle、Pex、VCCなどのツールの中に隠されています.Z3のnew Python front-endはこれを変更しようとします。
- 1. importとconstとの相違点とcommonjsでの相違点
- 2. =と:=の相違点
- 3. Java JFrameとJPanelの相違点Repaint()との相違
- 4. z3 :: tacticとz3 :: goalの目的
- 5. PHPUnitとPHPSpecの相違点と相違点
- 6. z3から間違った結果
- 7. MSBuildとTFSBuildの相違点
- 8. string.hとstrings.hの相違点
- 9. NSArrayとNSMutableArrayの相違点
- 10. System.Web.CacheとHTTPContext.Curent.Cacheの相違点
- 11. saveとsave_model()の相違点
- 12. sparse.model.matrixとas.matrixの相違
- 13. Color.redとColor.REDの相違
- 14. ディスパッチキューとNSOperationQueueの相違点
- 15. HTML5とjQueryの相違点
- 16. QtGui.QApplicationとQtCore.QCoreApplicationの相違点
- 17. CDO.MessageとSystem.Net.Mailの相違点
- 18. TransactionとTransactionScopeの相違点
- 19. addonGlobalLayoutListenerとaddOnPreDrawListenerの相違点
- 20. getGenericParameterTypesとgetParameterTypesの相違点
- 21. vmlinuxとvmlinux.oの相違点
- 22. KeyEventArgs.systemKeyとKeyEventArgs.Keyの相違点
- 23. Thread.sleep()とTimeUnit.SECONDS.sleep()の相違点
- 24. レポートとサブレポートの相違点
- 25. MPI_ScatterとMPI_Bcastの相違点
- 26. V8とECMAScriptの相違点
- 27. カーネルモードとドライバの相違点
- 28. アルゴリズムとメソッドの相違点
- 29. mysql_num_rowsとmysql_affected_rowsの相違点
- 30. modelAttributeとcommandNameの相違点