Propositional Logic for AI: Syntax, Semantics and Inference

A knowledge-based agent keeps a knowledge base (KB) of sentences about the world and uses inference to derive new sentences. The simplest formal language that supports this is propositional logic. Although simple, it is the foundation of hardware verification, planning-as-satisfiability and many industrial solvers. Let us learn it properly.

Syntax#

Propositional logic has atomic propositions — symbols such as $P$, $Q$, Raining — each of which is either true or false. Complex sentences are built with connectives:

Precedence from highest to lowest is $\neg, \land, \lor, \Rightarrow, \Leftrightarrow$.

Semantics: models and truth#

A model assigns true or false to every symbol. The truth of a complex sentence is computed recursively. The only connective that surprises students is implication: $P \Rightarrow Q$ is false only when $P$ is true and $Q$ is false. "If the moon is made of cheese, then 2 + 2 = 5" is true, because the premise is false.

A sentence is valid (a tautology) if it is true in all models, and satisfiable if it is true in at least one. These are linked by a fundamental result:

This is proof by contradiction, and it is how most automated reasoners work.

Inference by model checking#

The simplest inference algorithm enumerates all $2^n$ models and checks that $\alpha$ holds wherever $KB$ holds. It is sound (never derives false conclusions) and complete (derives every entailed sentence), but exponential.

from itertools import product

def tt_entails(kb, alpha, symbols):
    """kb and alpha are functions from a model dict to bool."""
    for values in product([True, False], repeat=len(symbols)):
        model = dict(zip(symbols, values))
        if kb(model) and not alpha(model):
            return False
    return True

# KB: (Rain => WetGrass) and Rain.  Query: WetGrass
kb = lambda m: ((not m["Rain"]) or m["Wet"]) and m["Rain"]
print(tt_entails(kb, lambda m: m["Wet"], ["Rain", "Wet"]))   # True

Inference rules and theorem proving#

Instead of enumerating models, we can apply inference rules that are known to be sound:

• Modus Ponens: from $\alpha \Rightarrow \beta$ and $\alpha$, infer $\beta$.
• And-Elimination: from $\alpha \land \beta$, infer $\alpha$.
• Logical equivalences: De Morgan's laws, contraposition $(\alpha \Rightarrow \beta) \equiv (\neg\beta \Rightarrow \neg\alpha)$, and so on.

Resolution#

One rule alone — resolution — is complete for refutation when sentences are in Conjunctive Normal Form (CNF), a conjunction of clauses where each clause is a disjunction of literals:

To prove $KB \models \alpha$, convert $KB \land \neg\alpha$ to CNF and repeatedly resolve pairs of clauses. If you derive the empty clause, you have a contradiction, and the entailment is proved.

Horn clauses and efficient inference#

A Horn clause has at most one positive literal, e.g. $\neg A \lor \neg B \lor C$, which is equivalent to $A \land B \Rightarrow C$. Knowledge bases of Horn clauses support forward chaining (data-driven: fire rules whose premises are known) and backward chaining (goal-driven: work backwards from the query) in time linear in the size of the KB. The Prolog language is built on backward chaining over Horn clauses.

SAT solvers: logic at industrial scale#

Deciding satisfiability of a CNF formula (SAT) was the first problem proved NP-complete (Cook, 1971). Yet modern CDCL (Conflict-Driven Clause Learning) solvers routinely handle formulas with millions of variables, thanks to clever ideas: unit propagation, learning new clauses from conflicts, non-chronological backjumping and restarts. SAT solvers verify microprocessors, schedule airlines and solve planning problems.

Limitations#

Propositional logic cannot express general statements compactly. To say "every student who passes the exam gets a certificate" for 500 students, you need 500 separate sentences. First-order logic, our next lecture, fixes this by adding objects, relations and quantifiers.