There are two ideas behind Inference in First order logic in Artificial intelligence
- convert the KB to propositional logic and use propositional inference
- a shortcut that manipulates on first-order sentences directly (resolution, will not be introduced here)
Universal Instantiation
- infer any sentence by substituting a ground term (a term without variables) for the variable
Examples

A First-Order Inference Rule
- If there is some substitution θ that makes the premise of the implication identical to sentences already in the knowledge base, then we assert the conclusion of the implication, after applying θ
- Sometimes, we need to do is find a substitution θ both for the variables in the implication and in the sentence to be matched