Lolli can be viewed as a refinement of the Hereditary Harropformulas of Lambda-Prolog. All the operators (though not

the higher order unification) of Lambda-Prolog are

supported, but with the addition of linear variations. Thus a

Lolli program distinguishes between clauses which can be used

as many, or as few, times as desired, and those that must be

used exactly once. Lolli is implemented in SML/NJ.