Mechanising the theory of intervals using OBJ3

摘要

This work uses the OBJ3 term rewriting system to formalize the type interval through some of its algebraic and topological properties. The intended contribution is not the discovery of new theorems related to numerical or interval arithmetic. Rather, our aim is to formally specify the type interval with the view of performing mechanical (automated) reasoning about its properties.