Research Publications

Placeholder
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.

Details

published
Conference Paper
Theorem Proving in Higher Order Logics
71-86
Rome
www.informatik.uni-trier.de/~ley/db/conf/tphol/tphol2003.html
D. Basin and B. Wolff
Springer
978-3-540-40664-8