From Logic to Prolog: Horn Clauses and SLD-Resolution

How do we bridge the gap between abstract mathematical resolution and a programming language like Prolog? The answer lies in a specific subset of logic called Horn Clauses. What is a Horn Clause? A Horn clause is a disjunction of literals with at mos...