新论文:《HOL的验证生成反思》

||论文

假日MIRI研金宝博娱乐究员Benya Fallenstein和副研究员Ramana Kumar合著了一篇关于机器反射的新论文。用于建模多态的HOL的验证生成反射。”

假日表示高阶逻辑,这里指流行鉴证助理的家属基于教会的类型理论。库马尔和合作者之前已正式在HOL (具体来说,HOL4)对某个东西来说,能够在霍尔身上被证明是什么意思,对某个东西成为霍尔的榜样又是什么意思。1在“高阶逻辑的自形式化Kumar、Arthan、Myreen和Owens证明,如果某些东西在HOL身上可以被证明,那么它在所有的HOL模型中都是真实的。

“对酒精的证明-生产反思”建立在这一结果之上,通过展示酒精内部的酒精模型(“内部酒精”)和酒精本身(“外部酒精”)之间的正式对应关系。非正式地说,Fallenstein和Kumar表明,人们总是可以构建对内酒精中的术语的解释,使它们与外酒精中的术语具有相同的含义。然后,作者表明,如果语句的某种类型是可证明的在霍尔自己的模型中,它们确实是真正的在(外部)假日。这种通信使作者能够使用HOL实现模型多态性的第6.3节所述的机器自我验证方法。Vingean反思:自我改进代理的可靠推理。”2

这个项目的动机是,在正式的验证系统中建模正式的验证系统,特别是在它们本身的建模上,几乎没有实际的工作。金宝博官方Fallenstein注意到,只关注Vingean反射的数学理论可能会使我们对软件实现的工程困难所在进行错误的校准。在实现模型多态的过程中,Fallenstein和Kumar确实遇到了从过去的理论工作中不明显的困难,其中最重要的是来自HOL的多态性

法伦斯坦和库马尔的论文被提交到2015年国际旅游业伙伴关系可以找到在线或在相关的会议论文集。多亏了由未来生命研究所提供Kumar和Fallenstein将继续在这个项目上合作。继“对HOL的验证生成反思”之后,Kumar和Fallenstein的下一个目标将是开发利用模型多态性进行推理的HOL proof助手内代理的玩具模型。


  1. 库马尔表明,如果霍尔有一个集合理论的模型,那么他也有一个关于霍尔的模型。此外,Fallenstein和Kumar还表明,如果一个更简单的公理成立的话,在HOL中存在一个集合理论的模型。
  2. 更多关于逻辑推理在机器反射中的作用,请参见Fallenstein的2013关于自我修改系统的对话金宝博官方