Theorem proving with definitions
Fausto Giunchiglia, Toby Walsh · 1989
This paper analyses a technique (called Gazing) for unfolding definitions on the basis of a global plan built in an abstract space. Gazing's logical properties are studied inside a formal framework which relies on a more general theory of abstraction. Some experimental results conrming the theoretical ones are also presented.