Artificial Intelligence Knowledge, Reasoning, and Logic Syllabus

What is the phase transition / satisfiability threshold in random 3-SAT?

The hardness of random 3-SAT problems peaks near a critical clause/symbol ratio $\frac{m}{n} \approx 4.3$. Below it problems are almost always satisfiable, above it almost always unsatisfiable, and the hardest instances cluster at the threshold.

What is model checking as an approach to logical inference?

Model checking enumerates possible worlds (models) to test entailment: to check $KB \models \alpha$, verify that $\alpha$ is true in every model where $KB$ is true. Truth-table enumeration and improved backtracking (DPLL) and local search (WalkSAT) are model-checking methods.

What does First-Order Logic add over propositional logic ontologically?

FOL assumes the world contains objects (with individual identities), relations among objects (properties are unary relations), and functions (relations with exactly one value for a given input). Propositional logic only has facts that are true or false.

List the two quantifiers of FOL and their meanings.

Universal $\forall x\, P(x)$: $P$ holds for all objects. Existential $\exists x\, P(x)$: $P$ holds for at least one object. Their duality: $\forall x\, P \equiv \lnot \exists x\, \lnot P$.

What connective typically pairs with $\forall$, and which with $\exists$? Give the common mistake.

$\forall$ typically uses implication: $\forall x\; \text{King}(x) \Rightarrow \text{Person}(x)$. $\exists$ typically uses conjunction: $\exists x\; \text{King}(x) \land \text{Person}(x)$. Using $\land$ with $\forall$ wrongly asserts everything is a king; using $\Rightarrow$ with $\exists$ is trivially satisfied by any non-king.

State the semantics of a ground atomic sentence and of the equality symbol in FOL.

A term refers to an object via an interpretation; a predicate refers to a relation. An atomic sentence $P(t_1,\dots,t_n)$ is true iff the tuple of referred objects is in the relation. Equality $t_1 = t_2$ is true iff $t_1$ and $t_2$ refer to the same object.

What are the three commitments of the standard database (unique-names, closed-world, domain-closure) semantics sometimes used with FOL?

Unique-names assumption: distinct constants name distinct objects. Closed-world assumption: atomic sentences not known true are false. Domain closure: there are no objects beyond those named by constants. Standard FOL makes none of these assumptions.

Outline the steps of knowledge engineering in FOL.

1) Identify the task/questions. 2) Assemble the relevant knowledge (knowledge acquisition). 3) Decide on a vocabulary of predicates, functions, constants (the ontology). 4) Encode general domain knowledge as axioms. 5) Encode the specific problem instance. 6) Pose queries and get answers. 7) Debug and refine the knowledge base.

Define Universal Instantiation (UI) and Existential Instantiation (EI).

UI: from $\forall x\, \alpha$, infer $\alpha$ with $x$ substituted by any ground term. EI: from $\exists x\, \alpha$, infer $\alpha$ with $x$ replaced by a brand-new constant symbol (a Skolem constant) not appearing elsewhere in the KB.

What is unification, and what is a unifier?

Unification finds a substitution $\theta$ that makes two logical expressions identical: $\text{Unify}(p,q)=\theta$ where $p\theta = q\theta$. For example, $\text{Unify}(\text{Knows}(John,x), \text{Knows}(y,Jane)) = \{x/Jane,\; y/John\}$.

What is the Most General Unifier (MGU) and why standardize apart?

The MGU is the unifier that makes the fewest commitments (every other unifier is a specialization of it); it is unique up to variable renaming. Variables in the two expressions must be standardized apart (renamed to be distinct) to avoid spurious name clashes during unification.

State the Generalized Modus Ponens (lifted) inference rule.

For atomic $p_i, p_i', q$ and substitution $\theta$ with $p_i'\theta = p_i\theta$ for all $i$: from $p_1',\dots,p_n'$ and $(p_1 \land \cdots \land p_n \Rightarrow q)$, infer $q\theta$. Lifting applies the substitution once rather than instantiating all sentences.

What is the occur check in unification and why does it matter?

The occur check verifies that a variable is not unified with a term containing that same variable (e.g. $x$ with $S(x)$), which would create an infinite/cyclic term. Omitting it makes unification faster but unsound; many systems skip it for speed.

State Herbrand's theorem and its significance for FOL inference.

If a set of clauses is unsatisfiable, then there is a finite subset of ground instances (over the Herbrand universe) that is already unsatisfiable. This lets propositional methods lift to FOL, and it underlies the completeness of resolution (though FOL entailment is only semidecidable).

How is forward chaining used with first-order definite clauses (e.g. Datalog)?

Repeatedly apply Generalized Modus Ponens: find rules whose premises unify with known facts, and add the (instantiated) conclusions, until the query is proved or no new facts appear. For Datalog (function-free definite clauses) this terminates and is sound and complete.

What optimizations make first-order forward chaining efficient?

Pattern matching / conjunct ordering to reduce joins, incremental forward chaining (only rules whose premises match a newly added fact are reconsidered), and the Rete algorithm which precompiles rule conditions into a shared network to avoid redundant matching.

How does backward chaining work in FOL, and what search strategy does it use?

To prove a goal, find rules whose head unifies with the goal and recursively prove the (substituted) subgoals in the body, composing substitutions. It is a depth-first, goal-directed search—the basis of logic programming—but can loop infinitely and repeat work.

State the full first-order resolution inference rule.

For clauses $(\ell_1 \lor \cdots \lor \ell_k)$ and $(m_1 \lor \cdots \lor m_n)$, if $\ell_i$ and $m_j$ have unifier $\theta$ (i.e. $\text{Unify}(\ell_i, \lnot m_j)=\theta$), infer the clause containing all remaining literals, with $\theta$ applied. This is refutation-complete for FOL.

List the steps to convert a first-order sentence into Conjunctive Normal Form.

1) Eliminate $\Leftrightarrow$ and $\Rightarrow$. 2) Move $\lnot$ inward (De Morgan, quantifier duality). 3) Standardize variables apart. 4) Skolemize existentials (replace with Skolem constants/functions of enclosing universals). 5) Drop universal quantifiers. 6) Distribute $\lor$ over $\land$.

What is Skolemization and when is a Skolem function (vs. constant) needed?

Skolemization removes existential quantifiers by replacing the variable with a new constant or function. Use a Skolem constant if the $\exists$ is not inside any $\forall$; use a Skolem function of the enclosing universally quantified variables if it is, e.g. $\forall x\,\exists y\,P(x,y)$ becomes $\forall x\,P(x, f(x))$.

What is a resolution refutation proof and why must the KB be in CNF?

To prove $KB \models \alpha$, add $\lnot\alpha$ to the KB, convert everything to CNF, and repeatedly resolve clauses; deriving the empty clause $\{\}$ shows unsatisfiability, hence entailment. CNF is required because resolution operates on clauses (disjunctions of literals).

Define a definite clause in Prolog and describe Prolog's execution model.

A Prolog clause is Head :- Body, meaning body $\Rightarrow$ head. Prolog uses backward chaining with depth-first, left-to-right search, tries clauses in database order, uses unification without occur check, and applies negation-as-failure (a goal is 'false' if it cannot be proved).

What is negation as failure and how does it differ from logical negation?

Negation as failure treats $\text{not}(P)$ as true exactly when the system fails to prove $P$ (closed-world assumption). It differs from classical negation, which requires $\lnot P$ to be provably true; NAF makes conclusions defeasible and non-monotonic.

What is ontological engineering and what is an upper ontology?

Ontological engineering is the design of general-purpose frameworks of categories, objects, and relations for representing broad knowledge (events, time, physical objects, beliefs). An upper ontology is the general top-level structure (very abstract categories) under which domain-specific concepts are organized in a hierarchy.

How are categories represented in FOL, and what is the difference between membership and the subset relation?

Categories can be reified as objects. Membership: an object belongs to a category, $BB_9 \in Basketballs$ or $Member(BB_9, Basketballs)$. Subset (subcategory): $Basketballs \subseteq Balls$. Categories inherit properties and can be organized into a taxonomy.

Define physical composition ($PartOf$) and the difference between a category and an individual.

$PartOf(x,y)$ says $x$ is a physical part of $y$; it is transitive and reflexive, so parts form a hierarchy (e.g. $PartOf(Bucharest, Romania)$). A category is a class of objects; an individual is a single object that may be a member of categories.

What is a semantic network and what is its core reasoning mechanism?

A semantic network is a graph whose nodes are objects/categories and whose labeled edges are binary relations (e.g. $SubsetOf$, $MemberOf$, $HasColor$). Its core mechanism is inheritance: properties asserted of a category are inherited by members and subcategories along the links.

What are Description Logics designed to do, and name their two central inference tasks.

Description Logics formally define and reason about categories (concepts) and their relationships, emphasizing tractable, decidable inference. Central tasks: subsumption (is concept $C$ necessarily a subcategory of $D$?) and classification (does an object belong to a category?); also consistency checking of a concept.

What is default (non-monotonic) reasoning, and why is classical logic monotonic?

Default reasoning draws tentative conclusions that may be retracted given new information (e.g. 'birds fly' but not penguins). Classical logic is monotonic: if $KB \models \alpha$ then $KB \land \beta \models \alpha$—adding facts never invalidates conclusions—so it cannot model defaults.

Compare circumscription and default logic as formalisms for default reasoning.

Circumscription minimizes the extension of certain 'abnormality' predicates, assuming things are as normal as possible unless stated otherwise. Default logic adds default rules of the form 'prerequisite : justification / conclusion' to derive extensions—conclusions that hold when the justification is consistent with what is known.

Define the PDDL representation of a classical planning problem (its main components).

A planning problem in PDDL specifies: an initial state (conjunction of ground fluents), a goal (a conjunction/partial state), and a set of action schemas, each with a name, parameters, a PRECONDITION, and an EFFECT (added and deleted literals). States use the closed-world assumption.

State the closed-world and STRIPS assumptions used in classical planning, and how an action's effect is applied.

Closed-world: unmentioned fluents are false. An action is applicable in a state if its precondition holds. Its result is $\text{Result}(s,a) = (s - \text{Del}(a)) \cup \text{Add}(a)$: remove the delete-list literals and add the add-list literals; all other fluents persist (avoiding the frame problem).

Contrast forward (progression) and backward (regression) state-space search for planning.

Forward/progression search starts at the initial state and applies applicable actions toward the goal (large branching factor, needs good heuristics). Backward/regression search starts from the goal and works backward through actions whose effects are relevant and consistent, keeping only relevant actions (smaller branching).

How are admissible heuristics for planning derived via relaxation (e.g. ignore-delete-lists)?

Relax the problem to make it easier and use the relaxed optimal cost as a heuristic. The ignore-preconditions relaxation drops preconditions; the ignore-delete-lists relaxation removes all negative effects so progress is monotonic, yielding an admissible, informative heuristic (basis of the $h_{max}$/$h_{add}$ family).

What is a planning graph and what are its two alternating levels?

A planning graph is a layered, polynomial-size data structure built from the initial state. It alternates state levels $S_i$ (literals possibly true after $i$ steps) and action levels $A_i$ (actions possibly applicable), connected by precondition, add, and delete edges, including 'persistence' (no-op) actions for each literal.

Define the two types of mutex (mutual exclusion) links between actions in a planning graph.

Two actions at a level are mutex if: (1) inconsistent effects—one deletes a literal the other adds; (2) interference—one's effect deletes a precondition of the other; or (3) competing needs—their preconditions are mutex. Two literals are mutex if one negates the other or all ways of achieving them are pairwise mutex.

How is a planning graph used as an admissible heuristic (max-level, level-cost)?

The level at which a goal literal first appears is a lower bound on the steps needed to achieve it. The max-level heuristic (largest first-appearance level over goal literals) and the set-level heuristic (first level where all goal literals appear together and non-mutex) are admissible; the sum/level-sum heuristic is efficient but not admissible.

Describe the GRAPHPLAN algorithm.

GRAPHPLAN alternates two phases: (1) expand the planning graph one level; (2) attempt to extract a valid plan by searching backward from the goal literals at the last level, respecting mutex constraints. If extraction fails, expand another level and retry. It terminates with failure once the graph has 'leveled off' and no plan is found.

What does it mean for a planning graph to 'level off,' and why does GRAPHPLAN terminate?

A graph levels off when two consecutive levels are identical (same literals and same mutexes). Because the graph is monotonically growing but bounded (finitely many literals/actions and mutexes only decrease), it must level off; if the goal is still unreachable or mutex after leveling off, no plan exists and GRAPHPLAN returns failure.

How can a classical planning problem be solved as a SAT (Boolean satisfiability) problem?

Encode the planning problem for a fixed horizon $T$ as propositional logic: propositionalize the actions and fluents with time indices, assert the initial state at $t=0$, the goal at $t=T$, successor-state axioms, precondition axioms, and action-exclusion axioms; then use a SAT solver. Increase $T$ until a satisfying assignment (a plan) is found.