BT

如何利用碎片时间提升技术认知与能力? 点击获取答案

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

| 作者 Jonathan Allen 关注 594 他的粉丝 ,译者 朱永光 关注 0 他的粉丝 发布于 2010年12月2日. 估计阅读时间: 2 分钟 | QCon上海2018 关注大数据平台技术选型、搭建、系统迁移和优化的经验。

微软研究院宣称,Z3是世界上最快的定理证明程序。Z3被设计作为其他应用程序的底层工具,它不适合单独使用。而嵌入到定理证明程序中的时候,在大量的项目中都有应用,包括Spec#/BoogiePexYogiVigilanteSLAMF7SAGEVS3FORMULAHAVOC

通过使用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

评价本文

专业度
风格

您好,朋友!

您需要 注册一个InfoQ账号 或者 才能进行评论。在您完成注册后还需要进行一些设置。

获得来自InfoQ的更多体验。

告诉我们您的想法

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

LINQ to Z3,世界上最快的定理证明程序 by 施 建雄

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

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

1 讨论

登陆InfoQ,与你最关心的话题互动。


找回密码....

Follow

关注你最喜爱的话题和作者

快速浏览网站内你所感兴趣话题的精选内容。

Like

内容自由定制

选择想要阅读的主题和喜爱的作者定制自己的新闻源。

Notifications

获取更新

设置通知机制以获取内容更新对您而言是否重要

BT