First-Order Logic (FOL) Practice Flashcards

Comprehensive vocabulary flashcards covering basic symbols, syntax, semantics, inference strategies, and knowledge representation concepts for First-Order Logic (FOL).

First-Order Logic (FOL)

A formal language, also called Predicate Logic, that represents the world using objects, relations, and functions, offering more expressiveness than propositional logic.

Constant Symbols

Symbols in FOL vocabulary that refer to specific objects, such as John, Richard, or Nono.

Variable Symbols

Lowercase symbols like $x$, $y$, and $z$ that range over objects in a domain.

Predicate Symbols

Symbols representing relations or properties, such as $King(x)$ or $Brother(x,y)$.

Function Symbols

Symbols used to map objects to unique objects, such as $LeftLeg(x)$ or $Father(x)$.

Quantifiers

Logical symbols including the Universal Quantifier ($\forall$) and the Existential Quantifier ($\exists$) used to generalize over objects.

Term

A logical expression referring to an object, which can be a constant, a variable, or a function applied to other terms like $LeftLeg(John)$.

Atomic Sentence

A sentence formed by applying a predicate to terms, such as $Brother(Richard, John)$, which is true if the relation holds between the objects.

Model (FOL)

A mathematical structure consisting of a non-empty domain and an interpretation mapping symbols to specific objects, relations, and functions.

Ontological Commitment

What a logic assumes about the nature of the world; in FOL, it assumes the world consists of facts, objects, and relations.

Epistemological Commitment

The state of knowledge a logic assumes an agent can have; in FOL, a person can believe a sentence is True, False, or Unknown.

Forward Chaining

A data-driven inference strategy that starts with known facts and repeatedly applies rules using Generalized Modus Ponens until a goal is reached.

Backward Chaining

A goal-driven inference strategy that starts from a target query and decomposes it into sub-goals until known facts are reached.

Unification

The process of finding a substitution $\theta$ that makes two or more logical expressions syntactically identical.

Most General Unifier (MGU)

The least restrictive substitution $\theta$ that unifies two logic expressions, imposing the fewest constraints.

Occur Check

A step in the UNIFY algorithm that verifies a variable $x$ does not appear inside a term $t$ before binding them, preventing circular loops like $x = f(x)$.

Standardizing Apart

The process of renaming variables in expressions to avoid naming conflicts before performing unification.

Resolution

A complete, refutation-based inference method for FOL that proves a sentence by showing that the negated goal combined with the knowledge base is unsatisfiable.

Conjunctive Normal Form (CNF)

A standard format for logical sentences where they are expressed as a conjunction of disjunctions (clauses), required for the resolution method.

Skolemization

The process of eliminating existential quantifiers in CNF conversion by introducing Skolem constants or Skolem functions like $f(x)$.

Generalized Modus Ponens (GMP)

A lifted inference rule that allows concluding $SUBST(\theta, q)$ if for all $i$, $SUBST(\theta, p_i) = SUBST(\theta, p'_i)$ given premises and a rule.

Universal Instantiation (UI)

The process of substituting ground terms for variables in a universally quantified sentence to create propositional versions.

Unique Names Assumption

The database semantics assumption that every constant symbol refers to a distinct object, such that John is not Richard by default.

Closed World Assumption (CWA)

The assumption that any atomic sentence not known to be true in the knowledge base is false.

Domain Closure

The assumption that there are no objects in the domain beyond those explicitly named by constant symbols.