UNIF-PROBLEM : UNIFOPUNIF-PROBLEM is an unification command.
Set up a new unification problem. `Name', the first argument to this
command must already represent a disagreement set. Use the command ADD-DPAIR
to create this set. This is in some ways the inverse of the NAME-DPAIR
The command format for UNIF-PROBLEM is:
<Unif>UNIF-PROBLEM NAME FREE-VARS
TPS documentation homepage