Complete Integer Decision Procedures as Derived Rules in HOL

Michael Norrish

I describe the implementation of two complete decision procedures for integer Presburger arithmetic in the HOL theorem-proving system. The first procedure is Cooper’s algorithm, the second, the Omega Test. Between them, the algorithms illustrate three different implementation techniques in a fully expansive system.


Status: published
Type: Conference Paper
Conference/location: Theorem Proving in Higher Order Logics
Conference URL:
Full text
Presentation Slides: Download