This document provides a complete specification of the input language for the environmental theorem prover. This language is essentially the same input language used by any of the programs designated by AURA, an automated reasoning program developed at Argonne National Laboratory. The intended audience is the user who is already familiar with the concepts and terms associated with resolution-based theorem provers.