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.
Let \(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: Constant symbol, Variable, Function of terms
  • Formulas:
    • Atomic formulas (atoms): predicate applied to terms
    • Connectives applied to formulas
    • Quantifiers applied to formulas (, )

• Models A model \(w\) in first-order logic maps:

  • constant symbols to objects

    \[ w(\mathrm{alice}) = o_1,\quad w(\mathrm{bob}) = o_2,\quad w(\mathrm{arithmetic}) = o_3 \]

  • predicate symbols to tuples of objects

    \[ w(\mathrm{Knows}) = \{(o_1,o_3), (o_2,o_3), \ldots\} \]

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} \]

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}\):

• Choose set of formulas \(f_1, \ldots, f_k \in \mathrm{KB}\).
• 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}\).

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} \]

Definite clause (first-order logic): 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 (first-order logic):

\[ \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.

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.

Resolution inference 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') \]