Complete integer decision procedures as derived rules in HOL
Authors
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, isbn = {978-3-540-40664-8}, publisher = {Springer}, booktitle = {International Conference on Theorem Proving in Higher Order Logics}, month = sep, slides = {http://ts.data61.csiro.au/publications/nicta_slides/2138.pdf}, paperurl = {https://ts.data61.csiro.au/publications/nicta_full_text/2138.pdf}, year = {2003}, editor = {{D. Basin and B. Wolff}}, title = {Complete Integer Decision Procedures as Derived Rules in {HOL}}, pages = {71--86}, author = {Norrish, Michael}, address = {Rome} }