我期待在自动化软件验证的要求，即一个程序，它的代码（用C和Java语言程序的普通代码），生成一串定理说的，每个回路必须最终停止，没有断言将被违反，永远不会有一个空指针的解除引用等，然后将其传递给定理证明器，以证明它们实际上是真实的（否则找到一个指示代码中的错误的反例）。逻辑的软件验证
问题是使用什么样的逻辑。两个主要的位置似乎是：
一阶逻辑就好了。
一阶逻辑是不足够的表现力，需要高阶逻辑。
问题是，似乎有很多支持这两个职位。那么哪一个是对的？如果它是第二个，那么您是否有任何可用的事例要做，基于一阶逻辑的验证器是否有问题？
你可以做你的FOL需要的一切，但它是一个很多额外的工作 - 很多！大多数现有系统是由学者/人员开发的，时间不多，所以他们很想采取捷径来节省时间/精力，因此被HOL，功能语言等所吸引。但是，如果您想要构建一个系统将被成千上万的人使用，而不仅仅是数百人，我们相信FOL是一条可行之路，因为它对更广泛的受众来说更容易获得。做这项工作是无可替代的。我们已经在这25年了！请看看我们的项目（http://www.manmademinions.com）
问候，亚伦。
在我的实践经验，这似乎是“1一阶逻辑就好了”。有关基于一阶逻辑完全以规范语言编写的各种功能的完整规范示例，请参见ACSL by Example或this case study。
一阶逻辑具有自动已提炼多年来处理好这来自程序验证性检验仪（没有证据助理）。这些用途的显着自动化证明器是例如Simplify,Z3和Alt-ergo。如果这些证明者失败并且没有明显的引理/断言可以添加来帮助他们，那么您仍然有办法为困难的证明义务启动证明助手。另一方面，如果您使用HOL，则根本无法使用Simplify，Z3或Alt-ergo，虽然我听说过高阶逻辑的自动化证明，但我从来没有听说过它们在性能方面受到赞扬的效率来自程序。
我们发现FOL对于大多数验证条件都是很好的，但高阶逻辑对于小数目是无价的，例如用于证明集合中元素求和的属性。所以我们的定理证明器（在Perfect Developer和Escher C Verifier中使用）基本上是一阶的，但也有能力做一些更高阶的推理。