Propositional and predicate logic

A proposition is a statement that is either true (T) or false (F). Compound formulas are built with the connectives not ($\neg$), and ($\wedge$), or ($\vee$), implies ($\to$) and iff ($\leftrightarrow$). Convention: formulas are written with not, and, or, implies, iff; $\vee$ is the inclusive or; precedence from highest to lowest is $\neg$, $\wedge$, $\vee$, $\to$, $\leftrightarrow$; implication is right-associative, so $p\to q\to r$ means $p\to (q\to r)$. Use brackets whenever in doubt.

$\wedge$, $\vee$ and $\leftrightarrow$ are commutative and associative. $\to$ is neither: $p\to q\not\equiv q\to p$, and $(p\to q)\to r\not\equiv p\to (q\to r)$ (take $p$ false and $r$ false: the left side is false, the right side true).

The implication $p\to q$ is false in exactly one row: $p$ true and $q$ false. When $p$ is false the implication is true (vacuously), whatever $q$ is. A formula over $n$ distinct variables has $2^n$ rows in its truth table.

A set of connectives is functionally complete if every truth function can be written with it alone. $\{\neg ,\wedge \}$, $\{\neg ,\vee \}$, $\{\neg ,\to \}$, $\{\text{NAND}\}$ and $\{\text{NOR}\}$ are each complete (for example $p\vee q\equiv \neg p\to q$). $\{\wedge ,\vee ,\to ,\leftrightarrow \}$ is not: every formula built from these alone is true when all its variables are true, so $\neg p$ cannot be expressed.

Every tautology is satisfiable. $\phi$ is a tautology exactly when $\neg \phi$ is a contradiction, and $\phi$ is satisfiable exactly when $\neg \phi$ is not a tautology. Two formulas are logically equivalent ($\phi \equiv \psi$) when they have the same truth value under every assignment, which is the same as $\phi \leftrightarrow \psi$ being a tautology.

Three consequences of the definition: an unsatisfiable KB entails every formula (there is no assignment to check); every KB entails a tautology; and entailment is monotonic: if $\mathrm{KB}\models \alpha$ then $\mathrm{KB}\wedge \beta \models \alpha$ for any $\beta$.

A satisfying assignment is also called a model. To count models it is often quicker to count the falsifying assignments and subtract from $2^n$: an implication $\alpha \to \beta$ is false only when $\alpha$ is true and $\beta$ is false, and a disjunction is false only when every disjunct is false. For a conjunction it is usually quicker to count the models directly (every conjunct true). Checking satisfiability of a general formula is hard (SAT is NP-complete), but a truth table settles any small case.

A literal is a variable or its negation. A clause is a disjunction of literals. A formula in conjunctive normal form (CNF) is an and of clauses; in disjunctive normal form (DNF) it is an or of conjunctions of literals (terms). Every propositional formula has an equivalent CNF and an equivalent DNF, although distributing can make the result exponentially long: $(a_1\wedge b_1)\vee \cdots \vee (a_n\wedge b_n)$ has $2^n$ clauses in CNF.

A Horn clause has at most one positive literal, for example $\neg a\vee \neg b\vee c$, which reads $a\wedge b\to c$. A definite clause has exactly one positive literal (a rule or a fact); a goal clause has none. Satisfiability of a set of Horn clauses can be decided in linear time by forward chaining (unit propagation).

Resolution refutation proves $\mathrm{KB}\models \alpha$ by showing that $\mathrm{KB}\wedge \neg \alpha$ is unsatisfiable. Over a fixed finite set of variables only finitely many distinct clauses exist, so in propositional logic the procedure always stops.

1. Convert KB to CNF and put its clauses in a set S.
2. Negate the goal alpha, convert (not alpha) to CNF, and add its clauses to S.
3. Repeat:
4.     Pick two clauses in S that contain a complementary pair of literals.
5.     Resolve on ONE pair only; delete repeated literals in the resolvent.
6.     If the resolvent is the empty clause: stop, KB entails alpha.
7.     If the resolvent is not already in S: add it to S.
8.     If no pair of clauses gives a new clause: stop, KB does not entail alpha.

First-order logic adds constants (a, b), variables (x, y), function symbols (f, g), predicates (P, Q, R, with arguments) and the quantifiers $\forall$ (for all) and $\exists$ (there exists). A formula is evaluated over an interpretation, that is a non-empty domain plus a meaning for each symbol. Convention: the domain is non-empty, and $\exists$ means at least one.

In $\forall xR(x,y)$ the variable $x$ is bound by its quantifier and $y$ is free. A formula with no free variables is a sentence and is true or false in a given interpretation. A bound variable can be renamed without changing meaning ($\forall xP(x)\equiv \forall zP(z)$), but never rename it to a name that is free in the scope.

A substitution replaces variables by terms, written $\{x/t\}$ and applied to all occurrences at once (simultaneously). A unifier of two expressions is a substitution making them identical. The most general unifier (MGU) is a unifier from which every other unifier can be obtained by a further substitution; it is unique up to renaming of variables. Convention: lower-case letters from the end of the alphabet (x, y, z, w) are variables, while a, b and names like f, g, h denote constants and function symbols.

The unification algorithm, with the substitution theta starting empty:

Unify(s, t, theta):
1. Let s1 = s with theta applied, and t1 = t with theta applied.
2. If s1 and t1 are identical: return theta.
3. If s1 is a variable v:
       if v occurs inside t1: return FAIL            (the occurs check)
       else: apply v/t1 to every binding already in theta,
             add the binding v/t1 to theta, and return theta.
4. If t1 is a variable: return Unify(t1, s1, theta).
5. If s1 and t1 are compound with the same symbol and the same number of arguments:
       for i = 1 to the number of arguments:
           theta = Unify(i-th argument of s1, i-th argument of t1, theta)
           if theta is FAIL: return FAIL
       return theta
6. Otherwise return FAIL.
   (Two different constants, a constant against a compound term,
    different function or predicate symbols, or different numbers of arguments.)

For example $P(x,f(x))$ and $P(a,y)$ unify with MGU $\{x/a,y/f(a)\}$, while $P(x,f(x))$ and $P(f(y),y)$ do not unify because the occurs check fails ($y$ would equal $f(f(y))$).