The problem of naming and function replacement

This article is the twenty-eighth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria that an automated reasoning program can profitably use to remove functions present in the representation and replace them with appropriate predicates or constants thatname the entities that werenamed by the functions. The notation used to present a problem to a reasoning program can have a profound effect on the likelihood of the program's success.This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.