A couple of thousand years ago, Aristotle, or one of those guys (I don't know as much as I should about the history of logic), came up with the idea of the syllogism. I assume people already took it for granted that you could justify a statement by saying it followed from one or two other statements. So for example, from "All men are mortal" and "Socrates is a man", we may conclude that Socrates is mortal. Or, as you will learn from Monty Python's Logician sketch, from "All mackerel are fish" and "All fish live in the sea", you can legitimately conclude that all mackerel live in the sea. Though the Logician complains that his wife will conclude that fish live in trees, that if she buys kippers it will not rain, or even that he does not love her any more, since she is not Logical.
Aristotle, who married twice, may similarly have been worried by his illogical wives; so he wrote down a list of the possible ways in which you were allowed to make this kind of inference, and these were the syllogistic forms. It was a major breakthrough, but when you look at the list - you can for example find it in the Wikipedia article - you still feel it's kind of long and redundant. Do we really need both "Darii":
All rabbits have fur. Some pets are rabbits. Some pets have fur.
and also "Baroco":
All rabbits have fur. Some pets do not have fur. Some pets are not rabbits?
But, in 1965, John Robinson discovered how to fold all of the syllogisms into one single rule of deduction, "the resolution rule", which could be implemented on a computer. It's a stunningly elegant synthesis of two thousand years of work. In this book, Robinson gives you all the background in formal logic you need to understand what he did; the treatment is quite self-contained.
Robinson's discovery has had an incalculable influence on the development of Artificial Intelligence. If someone brought Aristotle to the twenty-first century in a time-machine, this is the first thing I'd show him.