1(* ========================================================================= *) 2(* MATCHING AND UNIFICATION *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibMatch = 7sig 8 9type term = mlibTerm.term 10type formula = mlibTerm.formula 11type subst = mlibSubst.subst 12 13(* mlibMatching *) 14val matchl : subst -> (term * term) list -> subst 15val match : term -> term -> subst 16val matchl_literals : subst -> (formula * formula) list -> subst 17val match_literals : formula -> formula -> subst 18 19(* Unification *) 20val unifyl : subst -> (term * term) list -> subst 21val unify : subst -> term -> term -> subst 22val unify_and_apply : term -> term -> term 23val unifyl_literals : subst -> (formula * formula) list -> subst 24val unify_literals : subst -> formula -> formula -> subst 25 26end 27