Z3_Theorem_Prover
Z3 Theorem Proverは、Microsoftによるクロスプラットフォームの満足度モジュロ理論（SMT）ソルバーです。
Z3定理証明者
原作者 Microsoft Research 開発者
マイクロソフト
初回リリース
2012 ; 9年前 （2012）
安定したリリース
z3-4.8.12 / 2021年7月13日 ; 35日前 （2021-07-13）
リポジトリ
github .com / Z3Prover / z3
で書かれている
C ++
オペレーティング・システム
Windows、FreeBSD、Linux（Debian、Ubuntu）、macOS
プラットホーム
IA-32、x86-64
タイプ
定理証明者
ライセンス
MITライセンス
Webサイト
github .com / Z3Prover
コンテンツ
1 概要
2 例
2.1 命題論理と述語論理 2.2 方程式を解く
3 も参照してください
4 参考文献
5 参考文献
6 外部リンク
概要
Z3は、MicrosoftResearchのResearchin Software Engineering（RiSE）グループで開発され、ソフトウェア検証およびソフトウェア分析で発生する問題の解決を目的としています。Z3は、算術、固定サイズのビットベクトル、拡張配列、データ型、未解釈の関数、および数量詞をサポートします。その主なアプリケーションは、拡張静的チェック、テストケース生成、および述語抽象化です。
2015では、受信したプログラミング言語ソフトウェア賞をからACM SIGPLAN。 2018年、Z3は、ソフトウェアの理論と実践に関する欧州合同会議（ETAPS）からTest of TimeAwardを受賞しました。マイクロソフトの研究者であるNikolajBjørnerとLeonardode Mouraは、Z3で定理証明を進めた功績が認められ、自動推論への顕著な貢献に対して2019年のエルブラン賞を受賞しました。
Z3は2015年の初めにオープンソース化されました。ソースコードはMITライセンスの下でライセンスされ、GitHubでホストされています。ソルバーは、Visual Studio、Makefile、またはCMakeを使用して構築でき、Windows、FreeBSD、Linux、およびmacOSで実行されます。
C、C ++、Java、Julia、Haskell、OCaml、Python、WebAssembly、.NET / Monoなどのさまざまなプログラミング言語のバインディングがデフォルトの入力フォーマットはSMTLIB2です。
例
命題論理と述語論理
この例では、命題論理アサーションは、命題aとbを表す関数を使用してチェックされます。次のZ3スクリプトは、次のことを確認します。 ∧ ¯ ≡ ¯ ∨ ¯
{{ overline {a land b}} equiv { overline {a}} lor { overline {b}}}
：（declare-fun a（）Bool）（declare-fun b（）Bool）（assert（not（=（not（and ab））（or（not a）（not b）））））（チェック土）
結果： unsat スクリプトは、関心のある命題の否定を主張することに注意してUNSAT否定命題は所望の結果を証明し、満足できる結果ではない手段（ド・モルガンの法則）。
方程式を解く
次のスクリプトは、与えられた2つの方程式を解き、変数aとbに適した値を見つけます。（declare-const a Int）（declare-const b Int）（アサート（=（+ ab）20））（アサート（=（+ a（* 2 b））10））（チェック土）（get-model）
結果：
座った（モデル （define-fun b（）Int -10） （define-fun a（）Int 30））。
も参照してください
無料のオープンソースソフトウェアポータル
フォーマル検証
Alt-Ergo
参考文献
^ https://github.com/Z3Prover/z3/releases/tag/z3-4.8.12 ^ http://lim.univ-reunion.fr/staff/fred/Enseignement/AlgoAvancee/Exos/Z3-exercises.pdf ^ 「プログラミング言語ソフトウェア賞」。www.sigplan.org。
^ MicrosoftZ3定理証明者が賞を受賞 ^ ETAPS2018テストオブタイムアワード ^ Z3定理証明者の背後にある内なる魔法-MicrosoftResearch ^ エルブラン賞 ^ 「MicrosoftのVisualStudioタイムラインとZ3Theorem Prover、Google Cloud Launcher、FacebookのFresco—SD Timesニュースダイジェスト：2015年3月27日」。2015年3月27日。
^ 「GitHub-Z3Prover / z3：Z3定理証明者」。2019年12月1日–GitHub経由。
参考文献
レオナルド・デ・モウラ、ニコライ・ビョルナー（2008）。「Z3：効率的なSMTソルバー」。システムの構築と分析のためのツールとアルゴリズム。4963：337–340。
DennisYurichev-例によるSAT / SMT -Z3Pyを使用した多くの例。
外部リンク
公式ウェブサイト
Z3定理証明者の背後にある内なる魔法
マイクロソフトのZ3 @ rise4fun”