我期待在自動化軟件驗證的要求，即一個程序，它的代碼（用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中使用）基本上是一階的，但也有能力做一些更高階的推理。