Complete Integer Decision Procedures as Derived Rules in HOL

Select |




Print


Norrish, Michael

Norrish, Michael


2003-09-01


Conference Material


Theorem Proving in Higher Order Logics


Rome


71-86


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


Springer


http://www.informatik.uni-trier.de/~ley/db/conf/tphol/tphol2003.html


978-3-540-40664-8


nicta:2138


Norrish, Michael. Complete Integer Decision Procedures as Derived Rules in HOL. In: D. Basin and B. Wolff Editor, editor/s. Theorem Proving in Higher Order Logics; Rome. Springer; 2003-09-01. 71-86.



Loading citation data...

Citation counts
(Requires subscription to view)