Slide 14.4: Inference rules

Slide 14.3: An example of first-order predicate calculus
Slide 14.5: Horn clauses
Home

Inference Rules

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:

From the statements a→b and b→c, one can derive the statement a→c, or written more formally,

       ( a → b ) and ( b → c )       
 a → c

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.