* output a PGF grammar in prolog readable syntax * variables in abstract syntax (hypotheses and lambda-abstractions) are translated to unique logical variables * PGF terms in concrete syntax are translated to more prolog-like terms