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/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...

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