Proof-object generator for unification and antiunification in ML:
- proof-object generation for unification uses the Martelli-Montanari syntactic unification algorithm;
- proof-object generation for antiunification uses the Plotkin algorithm for antiunification;
- proof-objects are based on the (Applicative) ML proof system and some derived rules.