Prolog and pattern-matching

I am sitting now in a Prolog lab session. This is a nice coincidence, since I've been thinking a lot about Prolog (not very successfully).

I want to express the facts that:
(1) the Moon is in Uniform Circular Motion around the Earth, with someone unknown Period of translation.
(2) If a body Body1 is in UCM centered around position Pos2, then acc(Body1) = vel(Body1)^2 / distance(pos(Body1),Pos2).

From this, I would like the program to find the to instantiate the formula, finding that:
acc(moon) = vel(moon)^2 / distance(pos(moon),pos(earth)).

ucm(moon, pos(earth), Periodme).    %
avvr(Body1, Pos2) :- ucm(Body1, Pos2, Period1). %

(UI '(UCM moon (pos earth) Period-moon-earth)
     (IMPLIES (UCM Body1 Pos2 Period1)  (= (acc Body1) (/ (^ (vel Body1) 2) (distance (pos Body1) Pos2)))))

=> (= (acc moon) (/ (^ (vel moon) 2) (distance (pos moon) (pos earth))))

Body1 => moon
Pos2 => (pos earth)


I want to implement this pattern matching in my Lisp code. Maybe I will use fare-matcher afterall, if only fare will tell me how.

Hang on... this is not very hard at all, is it?


Now, look at the new precondition of the IMPLIES. This problem is somewhat harder, but still no problem.

(UI '(UCM moon (pos earth) Period-moon-earth)
     (IMPLIES (UCM Body1 (pos Body2) Period1)  (= (acc Body1) (/ (^ (vel Body1) 2) (distance (pos Body1) Pos2)))))

=> (= (acc moon) (/ (^ (vel moon) 2) (distance (pos moon) (pos earth))))

We just need to make sure that (pos earth) matches (pos Body2).

Unfortunately, Lisp doesn't have a natural way of encoding which variables are universally quantified (in Prolog, you use capitals).


General pattern-maching, however, seems like a non-trivial problem.

;;pre: args and pattern are trees with atoms that are either CAPITAL or lowercase.
;;post: if there is a match, return the set of substitutions; otherwise return nil.
;; this will basically be a search for a substitution that works
  ;;first, it will try obvious substitutions
  ;;but I suspect this problem is NP-hard
(defun match-args (arg pattern)

)