A theory of abstraction

摘要

Informally, abstraction can be described as the process of mapping a representation of a problem onto a new representation. The aim of this paper is to propose the beginnings of a theory of reasoning with abstraction which captures and generalizes most previous work in the area. The theory allows us to study the properties of abstraction mappings and provides the foundations for the mechanization of abstraction inside an abstract proof checker.