Inference rules as graph arcs (reasoning-as-search), in Prolog

Answer

mortal(X) :- man(X). man(socrates). ?- mortal(socrates).

Each clause is an arc in a reasoning state space: the fact man(socrates) is a start state; the rule mortal(X):-man(X) is an inference arc; the query ?- mortal(socrates) asks whether a path of rule applications reaches the goal fact. Prolog's proof IS a goal-driven (backward) search.