 The clause flight(toronto, london) is a fact while flight(X,Y) :– flight(X,Z) , flight(Z,Y) is a rule, written by convention as a reversed conditional (the symbol “:–” means “if”; the comma means “and”; terms starting in uppercase are variables). The former states that there is flight connection between Toronto and London; the latter states that there is a flight between cities X and Y if, for some city Z, there is a flight between X and Z and one between Z and Y. Clauses in Prolog programs are a special type of Horn clauses having precisely one positive literal: Facts are program clauses with no negative literals while rules have at least one negative literal. (Note that in standard clause notation the program rule in the previous example would be written as flight(X,Y) ∨ ~flight(X,Z) ∨ ~flight(Z,Y).) The specific form of the program rules is to effectively express statements of the form: “If these conditions over here are jointly met then this other fact will follow”. Finally, a goal is a Horn clause with no positive literals. The idea is that, once a Prolog program Π has been written, we can then try to determine if a new clause γ, the goal, is entailed by Π, Π ⊨ γ; the Prolog prover does this by attempting to derive a contradiction from Π ∪ {~γ}. We should remark that program facts and rules alone cannot produce a contradiction; a goal must enter into the process. Like input resolution, SLD-resolution is not refutation complete for first-order logic but it is complete for the Horn logic of Prolog programs. The fundamental theorem: If Π is a Prolog program and γ is the goal clause then Π ⊨ γ iff Π ∪ {~γ} ⊢ [ ] by SLD-resolution (Lloyd 1984).