Z3とcoqの相違

Question

Z3とcoqの違いを教えてもらえますか？私には、coqは、ユーザーに証明ステップを記入する必要があるという点で証明補助者であると思われますが、Z3にはその要件がありません。しかし、coqもZ3と同様の自動戦術を持っているようですね？あるいは、coqの証明検索能力がZ3ほど強力でないかもしれませんか？

Answer 1

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はこれを変更しようとします。