First-order predicate calculus also has inference rules:
Rules for deriving truths from previously stated or proven truths.
A typical inference rule is the following:
Inference rules allow us to construct the set of all statements that can be derived from a given set of statements.
For example, the fist five statements in the previous example allow us to derive the following statements:
legs( horse, 4 ).
arms( horse, 0 ).
legs( human, 2 ).
arms( human, 2 ).
If we take the five statements to be axioms, then the preceding four statements become theorems.
A theorem is a statement which has been proved to be true.
The essence of logic programming is
A collection of statements are assumed to be axioms, and from them a desired fact is derived by the application of inference rules in some automated way.