LINQ to Z3，世界上最快的定理证明程序

作者 Jonathan Allen 译者 朱永光 发布于 2010年12月1日

领域

语言 & 开发

主题

.NET ,

编程 ,

定理证明程序 ,

Z3 ,

LINQ

分享到

微软研究院宣称，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

译者 朱永光 是IT自由人和环境保护者，微软最有价值专家（MVP）和MCSD。

1. 返回顶部

   LINQ to Z3，世界上最快的定理证明程序

   发表人 施 程煕

   很不错的文章，简短，深刻！转载到我的博客【www.ackarlix.com】

   回复