LINQ to Z3，世界上最快的定理证明程序
by
at 2010-12-01 18:15:21
original http://news.cnblogs.com/n/83052/
微软研究院宣称，Z3是世界上最快的定理证明程序。Z3被设计作为其他应用程序的底层工具，它不适合单独使用。而嵌入到定理证明程序中的时候，在大量的项目中都有应用，包括Spec#/Boogie、Pex、Yogi、 Vigilante、SLAM、F7、SAGE、VS3、FORMULA和HAVOC。
通过使用Z3的.NET的API，你可以使用面向对象的风格来编码定理。不过，在Z3练习指导中演示的一个非常小的问题，都用到了非常多的代码。Bart De Smet编写了名为LINQ to Z3的包装器，把OO风格的API包装为查询风格的API，极大地简化了Z3的使用。下面是Bart De Smet在做Channel 9访谈的时候演示的一个例子：
var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
where t.X1 - t.X2 >= 1
where t.X1 - t.X2 <= 3
where t.X1 == (2 * t.X3)+ t.X5
where t.X3 == t.X5
where t.X2 == 6 * t.X4
select t;
var solution = theorem.Solve();
Console.WriteLine("X1 = {0}， X2 = {1}， X3 = {2}， X4 = {3}， X5 = {4}",
Z3起初只提供了Windows平台的支持，不过现在也有Linux的版本。Z3基于“微软研究院许可协议”发布，不能用于商业目的。你可以通过Z3 on RiSE4Fun来尝试一下在线版本。
查看英文原文：LINQ to Z3, The World’s Fasted Theorem Prover
相关新闻：
· 讨论：“Mono是个跨平台的.NET”是否是个正确的说法(2010-11-30)
· .NET消息服务器Laharsub简介(2010-10-31)
· 从高司令到Ray Ozzie,技术大牛们的冬天来了？(2010-10-22)
· 采访开源Web框架SimpleFramework开发团队(2010-12-01)
· Mono向Mac OS应用程序开发示好(2010-10-27)
本文链接：http://news.cnblogs.com/n/83052/