## Definition **Inference rules** are syntactic patterns that derive new formulas from existing ones while preserving truth. They are the engine of automated reasoning. ## Soundness and Completeness - **Sound:** the rule derives only formulas that are *semantically entailed* by the premises. - **Complete:** the set of rules can derive every formula entailed by the premises. A *proof system* is the combination of axioms + inference rules. A useful system is both sound and complete. ## Core Propositional Rules ### Modus Ponens $\frac{\alpha, \quad \alpha \to \beta}{\beta}$ Given $\alpha$ and $\alpha \to \beta$, conclude $\beta$. ### Modus Tollens $\frac{\neg \beta, \quad \alpha \to \beta}{\neg \alpha}$ Contrapositive of modus ponens. ### And-Elimination $\frac{\alpha \land \beta}{\alpha}$ (And similarly for $\beta$.) ### And-Introduction $\frac{\alpha, \quad \beta}{\alpha \land \beta}$ ### Or-Introduction $\frac{\alpha}{\alpha \lor \beta}$ ### Resolution $\frac{\alpha \lor \beta, \quad \neg \beta \lor \gamma}{\alpha \lor \gamma}$ Refutation-complete on CNF for propositional logic. The basis of modern automated theorem proving — see [[Resolution Inference]]. ## First-Order Additions ### Universal Instantiation (UI) $\frac{\forall x \, \alpha(x)}{\alpha(t)}$ For any ground term $t$. ### Existential Instantiation (EI) $\frac{\exists x \, \alpha(x)}{\alpha(c)}$ Where $c$ is a new constant (Skolem constant). Must not appear elsewhere in the proof. ### Unification The mechanism that finds substitutions making two literals identical. Underlies resolution in FOL. Robinson's unification algorithm (1965) is sound and complete. ## Substitution and Skolemization - **Substitution** $\theta = \{x/a, y/f(z)\}$: applies term-for-variable replacements. - **Skolemization** removes existential quantifiers by introducing Skolem functions. $\exists y \, \text{Loves}(x, y)$ becomes $\text{Loves}(x, f(x))$ where $f$ is a fresh function. ## Related - [[Propositional Logic]] - [[First-Order Logic]] - [[Resolution Inference]] - [[Forward and Backward Chaining]]