Computer Arithmetic: Logic, Calculation, and Rewriting
Marco Benini, Dirk Nowotka, Carl Pulley · 1998
. Computer arithmetic is the logical theory which formalizes the way computers manipulate integer numbers. In this paper, we describe a combined system whose components are a logical theory for the Isabelle theorem prover, a calculational engine based on rewriting techniques, and a decision procedure for an extension of quantifier-free Presburger arithmetic. The goal of this work is to provide a general and efficient tool to help proving theorems in computer arithmetic. This contribution shows how it is possible to combine different formal techniques (deductive systems, rewriting techniques, decision procedures) in order to solve a notoriously hard problem. Keywords: Computer Arithmetic, theorem proving, decision procedures, rewriting, Presburger arithmetic 1. Introduction Computer arithmetic is the mathematical theory which underlies the way calculational machines operate on integer numbers. Computers manipulate integer numbers of a finite, fixed precision, internally represented as...