Chan, Tat-hung2007-04-232007-04-231977-10http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR77-326https://hdl.handle.net/1813/7447This paper describes the operation and implementation of the arithmetic proof rule for the quantifier free integer arithmetic used in the PL/CV 2 program verification system. The general arithmetic satisfiability problem underlying the rule is shown to be NP complete.1697202 bytes582291 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report