I know this is not the done thing, but a meta-interpreter is the best, easiest, simplest way I've found to explain resolution (for maximum impact, you can trace a program through the meta-interpeter so the other person gets to see what's going on).
And if I can be allowed a shamless plug of my research team's work, it's also possible to turn a meta-interpreter to an inductive learning procedure, so that you can generate a new program from examples of its inputs and outputs, even as you prove it. It's called Meta-Interpetive Learning:
And if I can be allowed a shamless plug of my research team's work, it's also possible to turn a meta-interpreter to an inductive learning procedure, so that you can generate a new program from examples of its inputs and outputs, even as you prove it. It's called Meta-Interpetive Learning:
https://github.com/metagol/metagol