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