formula tree, how to represent and manipulate

Dear all,

I have the problem to represent and manipulate formulas of some first-order
language.  The manipulations include the anotation of nodes with further
information and the removal of nodes (simplifications).  

Which data structure would you suggest for this task?  How would you perform
the updates?

For me, this pretty much looks like a task for some imperative language but
I'm sure there is a good way to do it in (ECLiPSe) Prolog.  Nevertheless, my
current best idea is to use structure notation for nodes and setarg/3 to
perform the updates.  

Thank you, Uli

-- 
Ulrich Scholz

Personal Memory Group                   
European Media Laboratory GmbH