His 1979 book, Logic: Form and Function, is out of print and now only available second-hand. It's sunk into obscurity, as you can see from Amazon's terrible image above.
After some efforts, I have managed to order a copy and will do my best to write a review (Google reports no accessible reviews on the Internet). Here is some background on Robinson (Wikipedia).
"Robinson was born in Halifax, Yorkshire, England in 1930 and left for the United States in 1952 with a classics degree from Cambridge University. He studied philosophy at the University of Oregon before moving to Princeton University where he received his PhD in philosophy in 1956. He then worked at Du Pont as an operations research analyst, where he learned programming and taught himself mathematics.---
He moved to Rice University in 1961, spending his summers as a visiting researcher at the Argonne National Laboratory's Applied Mathematics Division. He moved to Syracuse University as Distinguished Professor of Logic and Computer Science in 1967 and became professor emeritus in 1993.
It was at Argonne that Robinson became interested in automated theorem proving and developed unification and the resolution principle. Resolution and unification have since been incorporated in many automated theorem-proving systems and are the basis for the inference mechanisms used in logic programming and the programming language Prolog.
Automated theorem proving (ATP) is the engine of classical AI in the way that neural nets are the engine of contemporary AI.
Deep Learning, which makes everything into a classification problem, has superseded brittle, classical AI not least because high-level features emerge from the weight-training process under some optimisation criteria, rather than being hand-crafted by the programmer.
Check this brilliant article from the NYT (via Steve Hsu).
But if your ambitions are somewhat modest, ATP takes you a long way .. and you can do it at home, kids.
Here is the table of contents from "Logic: Form and Function".
And finally, here is the text from Chapter 13 where Robinson documents his (very old-fashioned) Lisp code for the hyper-resolution theorem prover (PDF).
My apologies for the poor quality, but it is readable. To make sense out of how it works, I suspect you need to buy the book and to read the preceding chapters.