Skip to main content

TS

Complete integer decision procedures as derived rules in HOL

Authors

Michael Norrish

NICTA

Abstract

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.

BibTeX Entry

  @inproceedings{Norrish_03,
    publisher        = {Springer},
    isbn             = {978-3-540-40664-8},
    author           = {Norrish, Michael},
    month            = sep,
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/2138.pdf},
    editor           = {{D. Basin and B. Wolff}},
    year             = {2003},
    title            = {Complete Integer Decision Procedures as Derived Rules in {HOL}},
    booktitle        = {International Conference on Theorem Proving in Higher Order Logics},
    pages            = {71-86},
    address          = {Rome}
  }

Download

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.