An important advance in 20th-century mathematical logic was achieved in 1965 when J.A. Robinson introduced the resolution calculus as a method for mechanical theorem-proving. This calculus underlies most of the work that has gone on in automated theorem-proving since. In very brief terms, we may say that a mathematical formula is a logical consequence of a set of formulae S if an only if S {¬ } is inconsistent. The achievement of the resolution method is that it mechanizes proofs of inconsistency, i.e., makes it possible to prove when a certain set of formulae is inconsistent.

Further on, in the early 1970s R. Kowalski and A. Colmerauer discovered that it was possible to give an operational interpretation to sentences of predicate logic. For this they used the resolution method of Robinson as the underlying computational model, and logic programming was born.

Logic programming is a science...