Logic for Artificial Intelligence

Propositional logic builds sentences out of proposition symbols — atomic statements such as Rain or WumpusAhead that are either true or false — combined with the logical connectives negation, conjunction, disjunction, implication, and biconditional. The syntax is recursive: any proposition symbol is a sentence, and combining sentences with a connective produces a new, larger sentence. What gives these sentences meaning is a model, defined as an assignment of a truth value to every proposition symbol in the language. Once a model fixes the truth value of each symbol, the truth value of any compound sentence built from those symbols is determined mechanically by the standard truth-table definition of each connective: a conjunction is true exactly when both conjuncts are true, a disjunction when at least one disjunct is true, and so on. This separation between syntax, the rules for building well-formed sentences, and semantics, the rules for evaluating their truth in a model, is the backbone of every logic used in artificial intelligence, propositional or otherwise, and it is what allows a logic's inference procedures to be judged independently of any particular domain they happen to be applied to.

Entailment is the central relation a reasoning system cares about: a knowledge base KB entails a sentence α, written KB⊨α, exactly when α is true in every model in which KB is true. This definition says nothing yet about how a machine would check entailment; it is a purely semantic statement about which models are possible given what is known. The most direct way to test it is model checking: enumerate every possible truth assignment to the proposition symbols that appear, and confirm that α comes out true in every one of those assignments where KB also comes out true. Model checking is sound and complete for propositional logic — it never approves a false conclusion and it never misses a true one — but its cost grows as O(2^n) for n proposition symbols, since every symbol doubles the number of models that must be checked. That exponential blowup is not a minor implementation detail; it is the concrete reason propositional logic, on its own, cannot represent large domains efficiently.

A knowledge-based agent is organized around a knowledge base that can be told new sentences (TELL) and asked what follows from what it has been told (ASK), so that any answer the agent gives is guaranteed to follow logically from its accumulated knowledge rather than being invented on the spot. The scaling problem becomes concrete in even a small domain: representing a 4×4 grid world with propositional logic alone requires on the order of 155 separate sentences built from 64 distinct proposition symbols, one cluster of symbols and rules for every square and every time step, because propositional logic has no way to say something once and have it apply everywhere. Doubling the grid to 8×8 does not merely double this cost; it multiplies the number of squares, and therefore the number of symbols and rules needed to describe them, by roughly four. That combinatorial cost is exactly what motivates moving to a logic that can quantify over objects instead of naming each one individually — the subject of the next lesson.

First-order logic makes a richer ontological commitment than propositional logic. Propositional logic assumes only that the world consists of facts that happen to be true or false; first-order logic additionally commits to the existence of objects and of relations that hold among them. A first-order model consists of a domain of objects together with relations, where each relation is simply the set of tuples of objects for which it holds — a unary relation behaves like a property of single objects, while an n-ary relation connects several objects at once. The language adds three kinds of symbols to express this: constant symbols naming particular objects (John, Richard), predicate symbols naming relations (King, Person, Brother), and function symbols naming mappings from objects to objects (LeftLeg, Mother). A function symbol applied to arguments produces a complex term that is best understood as simply a more elaborate name for an object, not as an instruction to compute something — LeftLeg(John) names an object the same way John does, it just names it via its relationship to John rather than directly.

Quantifiers are what let a single sentence stand in for what would otherwise require one sentence per object. The universal quantifier ∀x King(x)⇒Person(x) asserts that for every object in the domain, if that object is a king then it is a person — the sentence is checked against every possible way of assigning a domain object to x. The existential quantifier ∃x Crown(x)∧OnHead(x,John) asserts that at least one object in the domain is a crown that is on John's head — the sentence only needs one assignment of x to a domain object that makes it true. An interpretation fixes what each constant, predicate, and function symbol refers to in a given model, and the truth of an atomic sentence then depends on whether the named relation actually holds among the named objects in that model. Universal and existential quantification are duals connected through negation, so that a claim about "not all" can always be restated as a claim about "at least one" and vice versa.

This added expressiveness has a cost. Propositional logic's model-checking procedure is decidable because there are only finitely many proposition symbols and therefore finitely many models to enumerate. First-order logic has no such guarantee: Alonzo Church's 1936 result on the Entscheidungsproblem showed that there is no general algorithm that can always decide, for an arbitrary pair of first-order sentences, whether one follows from the other. First-order entailment is only semi-decidable — a sound and complete proof procedure is guaranteed to eventually find a proof whenever one exists, but if no proof exists the procedure may simply run forever without ever announcing failure. That asymmetry between provable truths and undecidable non-entailments is a structural fact about first-order logic itself, not a limitation of any particular theorem prover or any particular choice of inference rules, and it shapes every automated reasoning system built on top of it, from hand-verified proofs to the resolution-based provers introduced later in this course.

There are two fundamentally different ways to answer the question "does KB entail α". The semantic route, model checking, works directly with the definition of entailment by examining models. The syntactic route, proof, instead manipulates sentences using inference rules — such as Modus Ponens, which lets P and P⇒Q be combined to derive Q, or Universal Instantiation, which lets a universally quantified sentence be applied to a specific object to derive a ground sentence about it. A proof procedure is sound if every sentence it derives is genuinely entailed by the knowledge base, and complete if every entailed sentence is one it can eventually derive. Soundness and completeness are the two properties that make proof a trustworthy substitute for exhaustive model checking: a sound and complete procedure never derives a wrong answer, and it never fails to find a right one that exists to be found.

Proof can be understood as search through a space of sentences, where each inference rule is an operator that produces new sentences from ones already established, and the goal is to reach the target sentence α through a finite chain of such steps. As a knowledge base grows, the branching factor of this search — how many inference rules could apply at each step, and to which sentences — grows with it, so the choice of inference rules and search strategy matters enormously in practice, in much the same way that the choice of search strategy matters for any other search problem in artificial intelligence. One influential response to this problem, developed in detail in the module on automated reasoning, is to convert every sentence in the knowledge base into a single uniform clausal normal form and rely on one mechanical inference rule, resolution, instead of a large hand-picked collection of rules tailored to particular sentence shapes and requiring separate justification for each.

Church's undecidability result has a direct proof-theoretic consequence: because first-order entailment is only semi-decidable, a complete proof procedure is guaranteed to terminate and report success whenever KB does entail α, but there is no guarantee it will ever terminate when KB does not entail α — it may simply keep searching forever. This is a sharp contrast with propositional logic, where model checking always terminates because the space of models, though exponential, is finite; first-order logic trades that termination guarantee away for the expressive power of quantifying over unboundedly many objects. Real theorem-proving systems cannot wait indefinitely for an answer that may never come, so they combine formally sound and complete inference rules with resource bounds, heuristics, and search-ordering strategies that trade some theoretical guarantees for practical termination, and many practical systems additionally restrict themselves to tractable sublanguages, such as knowledge bases built entirely from definite clauses, specifically to regain stronger guarantees. Understanding this tension between what is logically knowable in principle and what is computable in practice is essential background for the resolution, unification, and chaining strategies covered in the next module.