LGGs (on antiunfiers) can be a useful widening technique.
One way to take advantage: when we make a new rule LHS => RHS if C, we could try to transform it as much as possible (using unification) to C [ LHS' => RHS' ]. Then if C has the structure like C(T1,...TI, LHS' => RHS', TI+1,...TN), then all of T1...TI, and TI+1...TN could be replaced with variables. This may make the abstraction process more automatable in the presence of things like threads.
LGGs (on antiunfiers) can be a useful widening technique.
One way to take advantage: when we make a new rule
LHS => RHS if C, we could try to transform it as much as possible (using unification) toC [ LHS' => RHS' ]. Then ifChas the structure likeC(T1,...TI, LHS' => RHS', TI+1,...TN), then all ofT1...TI, andTI+1...TNcould be replaced with variables. This may make the abstraction process more automatable in the presence of things like threads.