Propositional Logic

Models

Model $w$ : an assignment of values to propositional symbols
Interpretation function: for a formula $f$ and a model $w$ , $I (f, w) = 1 {w satisfies f}$
- Define $M (f) = {w : I (f, w) = 1}$

Knowledge base KB: $M (KB) = \cap_{f \in KB} M (f)$
Add a formula to the knowledge base:
- From KB to KB $\cup f$
- Shrinks the set of models: from $M (KB)$ to $M (KB) \cap M (f)$
Relationships between a KB and a formula $f$

Relationship	Notation	Definition	Meaning
Entailment	KB $⊨ f$	$M (KB) \subseteq M (f)$	Already knew that.
Contradiction		$M (KB) \cap M (f) = \emptyset$	Don’t believe that.
Contingency		$\emptyset ⊊ M (KB) \cap M (f) ⊊ M (KB)$	Learned something new.
Inference

KB contradicts with $f$ $⟺$ KB entails $\neg f$
Probabilistic interpretation $P (f ∣ KB) = \frac{\sum_{w \in M (KB \cup {f})} P (W = w)}{\sum_{w \in M (KB)} P (W = w)}$
A KB is satisfiable if $M (K B) \neq \emptyset$

Inference rule: if the premises $f_{1}, \dots, f_{k}$ are in the KB, then your can add the conclusion $g$ to the KB. Formula: $\frac{f_{1}, \dots, f_{k}}{g} \frac{(premises)}{(conclusion)}$
Modus ponens inference rule: captures the if-then reasoning pattern. For any propositional symbols $p$ and $q$ , we have $\frac{p, p \to q}{q}$
Derivation: KB derives $f$ , written as $K B ⊢ f$ , iff $f$ eventually gets added to KB.
- Inference rules operate directly on syntax, not on semantics.

A set of inference rules is sound if ${f : KB ⊢ f} \subseteq {f : KB ⊨ f}$
- Nothing but the truth
- Showing soundness is easy
A set of inference rules is complete if ${f : KB ⊢ f} \supseteq {f : KB ⊨ f}$
- Whole truth
- Showing completeness if hard
Fixing completeness
- Option 1: restrict the allowed set of formulas, to propositional logic with only Horn clauses
- Option 2: use more powerful inference rules, change from Modus ponens to resolution

Formulas allowed	Inference rules	Complete?
Propositional logic	modus ponens	No
Propositional logic (only Horn clauses)	modus ponens	Yes
Propositional logic	resolution	Yes

Horn clauses: is either a definite clause, $(p_{1} \land \dots \land p_{k}) \to q,$ or a goal clause $(p_{1} \land \dots \land p_{k}) \to false$
A more generic version of the modus ponens inference rule $\frac{p_{1}, \dots, p_{k}, (p_{1} \land \dots \land p_{k}) \to q}{q}$
Theory: Modus ponens is complete with respect to Horn clauses. This is, if KB contains only Horn clauses, then $KB ⊨ p (entailment) ⟺ KB ⊢ p (derivation)$

Rewrite implication $A \to C$ to disjunction $\neg A \lor C$
- In this way, we can rewrite modus ponens as $\frac{A, \neg A \lor C}{C}$ Note that $A$ and $\neg A$ are cancelled out.
Resolution inference rule: cancel out $p$ and $\neg p$ in the middle $\frac{f_{1} \lor \dots \lor f_{n} \lor p, \neg p \lor g_{1} \lor \dots \lor g_{m}}{f_{1} \lor \dots \lor f_{n} \lor g_{1} \lor \dots \lor g_{m}}$

CNF is a conjunction ( $\land$ ) of clauses ( $\lor$ )

Every formula in propositional logic can be converted into an equivalent CNF formula
Conversion rules

Syntax of first-order logic
- Terms (object)
  - constant symbol (e.g., arithmetic)
  - variable (e.g., $x$ )
  - function of terms (e.g., Sum(3, $x$ ))
- Formulas (truth values)
  - Atomic formulas (atoms): predicate applied to terms, e.g., Knows( $x$ , arithmetic)
  - Connectives applied to formulas: e.g., Student( $x$ ) $\to$ Knows( $x$ , arithmetic)
  - Quantifiers applied to formulas: e.g., $\forall x$ Student( $x$ ) $\to$ Knows( $x$ , arithmetic)
Quantifiers: for all ( $\forall$ ) and exists ( $\exists$ )
- Note the different connectives:
  - $\forall$ Student $(x) \to$ Knows( $x$ , arithmetic)
  - $\exists$ Student $(x) \land$ Knows( $x$ , arithmetic)

Definite clause in first-order logic for variables $x_{1}, \dots, x_{n}$ and atomic formuas $a_{1}, \dots, a_{k}, b$ which contain those variables, has the following form $\forall x_{1} \dots \forall x_{n} (a_{1} \land \dots \land a_{k}) \to b$
Substitution $θ$ is a mapping from variables to terms Subst $[θ, f]$ returns the result of performing substitution $θ$ on $f$ .
- E.g., Subst $[{x / alice}, P (x)] = P (alice)$
Unification: takes two formulas $f$ and $g$ and returns a substitution $θ$ which is the most general unifier: $Unify [f, g] = {\begin{cases} θ, & such that Subst [θ, f] = Subst [θ, g] \\ fail, & if no such θ exists \end{cases}$
First-order modus ponens with substitution: Let $θ = Unify [a_{1}^{'} \land \dots \land a_{k}^{'}, a_{1} \land \dots \land a_{k}]$ and $b^{'} = Subst [θ, b]$ , then $\frac{a_{1}^{'} \land \dots \land a_{k}^{'}, \forall x_{1} \dots \forall x_{n} (a_{1} \land \dots \land a_{k}) \to b}{b^{'}}$