## Definition **First-Order Logic (FOL)** — also called *predicate logic* — extends [[Propositional Logic]] with **objects**, **relations** between objects, and **quantifiers**. It is the standard formal language for [[Knowledge Representation]] in classical AI. ## Syntax - **Constants:** $a, b, \text{Alice}, \text{Earth}$ — specific objects. - **Variables:** $x, y, z$ — placeholders for objects. - **Predicates:** $P(x), \text{Loves}(x, y)$ — properties and relations. - **Functions:** $f(x), \text{FatherOf}(x)$ — map objects to objects. - **Connectives:** $\neg, \land, \lor, \to, \leftrightarrow$. - **Quantifiers:** $\forall$ (universal), $\exists$ (existential). Example: $\forall x \, (\text{Human}(x) \to \text{Mortal}(x))$ "All humans are mortal." ## Semantics An interpretation specifies: - A non-empty *domain* of objects. - A mapping from constants to domain objects. - A mapping from predicates to relations over the domain. - A mapping from functions to functions on the domain. A formula is **valid** if true under every interpretation, **satisfiable** if true under some. ## Quantifier Patterns - **Universal-existential** ($\forall x \exists y$): "for every $x$ there exists a $y$ such that…" - **Existential-universal** ($\exists x \forall y$): "there exists an $x$ such that for every $y$…" - Order matters: $\forall x \exists y \, \text{Loves}(x, y)$ (everyone loves someone) is *not* the same as $\exists y \forall x \, \text{Loves}(x, y)$ (someone is loved by everyone). ## Inference in FOL Sound and complete inference is **semi-decidable**: there's an algorithm that confirms entailment when it holds, but no algorithm guaranteed to halt when it doesn't (Church-Turing). Main inference techniques: - **[[Resolution Inference]]** with unification — the workhorse for FOL theorem proving. - **[[Forward and Backward Chaining]]** for definite clauses. - **Tableaux methods.** ## Restrictions Used in Practice Full FOL is rarely used directly. Practical systems use restricted fragments: - **Horn clauses** — at most one positive literal per disjunct. Underlies Prolog. - **Description logics** — decidable fragments used in OWL ontologies. - **Datalog** — recursive rules over a database. ## Related - [[Propositional Logic]] - [[Inference Rules]] - [[Resolution Inference]] - [[Knowledge Representation]] - [[Forward and Backward Chaining]]