Thanks! Note that the first two inferences I show above are valid resolution steps since they have literals that are complements under unification, like swan(al

Thanks! Note that the first two inferences I show above are valid resolution steps since they have literals that are complements under unification, like swan(alice) and swam(X)← (the latter being a negative literal, since it's in the body). But the third and fourth inferences can't be made with resolution. There is a whole bunch of work on abductive reasoning in a first-order framework, but I'm far from an expert on it. Antonis Kakas is a prominent name in the subject. For example, see: Abductive Logic Programming, A.C. Kakas, R. A. Kowalski, F. Toni https://academic.oup.com/logcom/article-abstract/2/6/719/942121?login=false https://academic.oup.com/logcom/article-abstract/2/6/719/942... Although behind a paywall. And yes, that's that Kowalski. Here's an unpaywalled overview: Abduction in Logic Programming, Marc Denecker and Antonis Kakas https://web.stanford.edu/class/cs227/Readings/Abudction%20in%20LP.pdf https://web.stanford.edu/class/cs227/Readings/Abudction%20in... And here's one on the application to learning: Abductive concept learning, Antonis C. Kakas & Fabrizio Riguzzi https://link.springer.com/article/10.1007/BF03037531 https://link.springer.com/article/10.1007/BF03037531