A formal definition and sound implementation of analogical reasoning in logic programming