Logic

• Representation (Syntax): defines a set of valid formulas.
• Semantics: for each formula, specify a set of models (assignments / configurations of the world).
• Inference rule: a rule that allows us to derive new formulas from existing ones.

2.1 Representation

Formal languages: syntax and model

2.1.1 Propositional logic

Syntax:

• Propositional symbols (atomic formulas): \(A, B, C\)
• Logical connectives: \(\neg, \land, \lor, \to, \leftrightarrow\)
• Build up formulas recursively—if \(f\) and \(g\) are formulas, so are the following:
  • Negation: \(\neg f\)
  • Conjunction: \(f \land g\)
  • Disjunction: \(f \lor g\)
  • Implication: \(f \to g\)
  • Biconditional: \(f \leftrightarrow g\)

Model:

A model \(w\) in propositional logic is an assignment of truth values to propositional symbols.

Interpretation function:

Let \(f\) be a formula and \(w\) be a model. An interpretation function \(\mathcal{I}(f,w)\) returns:

• true (1) (say that \(w\) satisfies \(f\))
• false (0) (say that \(w\) does not satisfy \(f\))

Base case: For a propositional symbol \(p\) (e.g., \(A, B, C\)):

\[ \mathcal{I}(p,w) = w(p) \]

Recursive case

Let \(\mathcal{M}(f)\) be the set of models \(w\) for which \(\mathcal{I}(f,w) = 1\).

Knowledge base:

A knowledge base \(\mathrm{KB}\) is a set of formulas representing their conjunction / intersection:

\[ \mathcal{M}(\mathrm{KB}) = \bigcap_{f \in \mathrm{KB}} \mathcal{M}(f). \]

2.1.2 First-order logic

Syntax:

• Terms denote objects: constant symbols \(c\), variables \(x\), and function applications \(f(t_1,\ldots,t_n)\), where each \(t_i\) is a term.
• Formulas are built from:
  • Atomic formulas: \(P(t_1,\ldots,t_n)\); also \(t_1=t_2\) in logic with equality.
  • Connectives applied to formulas: \(\neg,\land,\lor,\to,\leftrightarrow\).
  • Quantifiers applied to formulas: \(\forall x\,\varphi\), \(\exists x\,\varphi\).

Models:

• A model \(w\) specifies a nonempty domain \(D\) and interprets:
  • Constant symbols as objects: \(w(c)\in D\).
  • Function symbols as functions: \(w(f):D^n\to D\).
  • Predicate symbols as sets of tuples: \(w(P)\subseteq D^n\), equivalently functions \(D^n\to\{0,1\}\).
• A separate variable assignment \(s:\mathrm{Var}\to D\) gives variables their values: \(s(x)\in D\).

For example, if \(w(\mathrm{alice})=o_1\), \(w(\mathrm{arithmetic})=o_3\), and \((o_1,o_3)\in w(\mathrm{Knows})\), then \(\mathrm{Knows}(\mathrm{alice},\mathrm{arithmetic})\) is true.

2.2 Inference

2.2.1 Entailment and satisfiability

Entailment: \(\mathrm{KB}\) entails \(f\) (written \(\mathrm{KB} \models f\)) iff \(\mathcal{M}(\mathrm{KB}) \subseteq \mathcal{M}(f)\).

Contradiction: \(\mathrm{KB}\) contradicts \(f\) iff \(\mathcal{M}(\mathrm{KB}) \cap \mathcal{M}(f) = \emptyset\).

Contingency:

\[ \emptyset \subsetneq \mathcal{M}(\mathrm{KB}) \cap \mathcal{M}(f) \subsetneq \mathcal{M}(\mathrm{KB}) \]

Satisfiability: A knowledge base \(\mathrm{KB}\) is satisfiable if \(\mathcal{M}(\mathrm{KB}) \neq \emptyset\).

2.2.2 SAT and model-checking

Model checking:

• Input: knowledge base \(\mathrm{KB}\)
• Output: exists satisfying model (\(\mathcal{M}(\mathrm{KB}) \neq \emptyset\))?

Popular algorithms:

• DPLL (backtracking + propagation + pruning)
• WalkSat (randomized local search over complete assignments)

2.2.3 Inference rules

Modus ponens inference rule:

For any propositional symbols \(p\) and \(q\):

\[ \frac{p,\quad p \to q}{q} \]

General inference rule:

If \(f_1, \ldots, f_k, g\) are formulas, then the following is an inference rule:

\[ \frac{f_1,\quad \ldots,\quad f_k}{g} \]

Algorithm: forward inference:

Input: set of inference rules \(\mathrm{Rules}\).

Repeat until no changes to \(\mathrm{KB}\):

1. Choose set of formulas \(f_1, \ldots, f_k \in \mathrm{KB}\).
2. If matching rule \(\frac{f_1,\quad \cdots,\quad f_k}{g}\) exists, add \(g\) to \(\mathrm{KB}\).

Derivation:

\(\mathrm{KB}\) derives/proves \(f\) (\(\mathrm{KB} \vdash f\)) iff \(f\) eventually gets added to \(\mathrm{KB}\).

2.2.4 Horn clauses and modus ponens

Propositional logic:

Definite clause: A definite clause has the following form:

\[ (p_1 \land \cdots \land p_k) \to q \]

where \(p_1, \ldots, p_k, q\) are propositional symbols.

Horn clause: A Horn clause is either:

• a definite clause \((p_1 \land \cdots \land p_k \to q)\)
• a goal clause \((p_1 \land \cdots \land p_k \to \mathrm{false})\)

Modus ponens:

\[ \frac{p_1,\quad \cdots,\quad p_k,\quad (p_1 \land \cdots \land p_k) \to q}{q} \]

First-order logic:

Definite clause: A definite clause has the following form:

\[ \forall x_1 \cdots \forall x_n \bigl((a_1 \land \cdots \land a_k) \to b\bigr) \]

for variables \(x_1, \ldots, x_n\) and atomic formulas \(a_1, \ldots, a_k, b\) (which contain those variables).

Modus ponens:

\[ \frac{a_1,\ldots,a_k \qquad \forall x_1\cdots\forall x_n\bigl((a_1\land\cdots\land a_k)\to b\bigr)}{b} \]

Substitution:

A substitution \(\theta\) is a mapping from variables to terms.

\(\operatorname{Subst}[\theta, f]\) returns the result of performing substitution \(\theta\) on \(f\).

Unification:

Unification takes two formulas \(f\) and \(g\) and returns a substitution \(\theta\) which is the most general unifier:

\[ \operatorname{Unify}[f,g] = \theta \quad \text{such that} \quad \operatorname{Subst}[\theta,f] = \operatorname{Subst}[\theta,g] \]

or “fail” if no such \(\theta\) exists.

2.2.5 Complexity

Theorem: completeness:

Modus ponens is complete for first-order logic with only Horn clauses.

Theorem: semi-decidability:

First-order logic (even restricted to only Horn clauses) is semi-decidable.

• If \(\mathrm{KB} \models f\), forward inference on complete inference rules will prove \(f\) in finite time.
• If \(\mathrm{KB} \not\models f\), no algorithm can show this in finite time.

2.2.6 Resolution

Propositional resolution rule:

\[ \frac{f_1 \lor \cdots \lor f_n \lor p,\quad \neg p \lor g_1 \lor \cdots \lor g_m} {f_1 \lor \cdots \lor f_n \lor g_1 \lor \cdots \lor g_m} \]

Conjunctive normal form (CNF):

A CNF formula is a conjunction of clauses.

Proposition: conversion to CNF:

Every formula \(f\) in propositional logic can be converted into an equivalent CNF formula \(f'\):

\[ \mathcal{M}(f) = \mathcal{M}(f') \]

First-order conversion to CNF:

• All variable have universal quantifiers by default
• Introduce Skolem functions (e.g., \(Y(x)\)) to represent existentially quantified variables.

First-order resolution rule:

\[ \frac{ f_1 \lor \cdots \lor f_n \lor p,\qquad \neg q \lor g_1 \lor \cdots \lor g_m }{ \operatorname{Subst}[\theta,\, f_1 \lor \cdots \lor f_n \lor g_1 \lor \cdots \lor g_m] } \]

where \(\theta = \operatorname{Unify}[p,q]\).

2.3 Semantics

2.3.1 Desiderata for inference rules

Semantics:

Interpretation defines entailed/true formulas: \(\mathrm{KB} \models f\).

\[ \mathcal{M}(\mathrm{KB}) \subseteq \mathcal{M}(f) \]

Syntax:

Inference rules derive formulas: \(\mathrm{KB} \vdash f\)

2.3.2 Soundness

A set of inference rules \(\mathrm{Rules}\) is sound if:

\[ \{f : \mathrm{KB} \vdash f\} \subseteq \{f : \mathrm{KB} \models f\}. \]

2.3.3 Completeness

A set of inference rules \(\mathrm{Rules}\) is complete if:

\[ \{f : \mathrm{KB} \vdash f\} \supseteq \{f : \mathrm{KB} \models f\} \]

2.3.4 Fixing completeness

1. Option 1: Restrict the allowed set of formulas

   propositional logic \(\to\) propositional logic with only Horn clauses

2. Option 2: Use more powerful inference rules

   Modus ponens \(\to\) resolution

2.3.5 Theorem: Modus ponens on Horn clauses

Modus ponens is complete with respect to Horn clauses:

• Suppose \(\mathrm{KB}\) contains only Horn clauses and \(p\) is an entailed propositional symbol.
• Then applying modus ponens will derive \(p\).