Hi, there!

I'm having some problems with a program I have to implement using Lisp, and I was wondering if anyone could give me a few pointers or maybe a bit of code.

The task is this - I have to write a function that receives a list of rules (each rule being stated as '(a b then c), meaning "if a and b are true, then c is true"), a fact, and a list of facts that are considered true. The function should create a "demonstration path" of rules from the first list, proving that the given fact is itself true, starting from the facts from the second list. An example would be:

(prove '( (a b then c) (b c then d) (a b c d then x) ) 'x '(a b)), which should return ((A B THEN C) (B C THEN D) (A B C D THEN X)).

Thanks in advance for any help.