First-Order Logic in Use

This builds on First-Order Logic, which set up the language: objects, relations, and functions; the model that gives a sentence its truth value; the syntax of terms and sentences; the two quantifiers; and equality. Here we turn from writing the language to using it.

Database semantics

The reason Richard has at least two brothers needs an explicit $\ne$ is the semantics we have used so far: two distinct constant symbols may or may not name the same object, and there may be objects the vocabulary never names. This is the standard semantics (sometimes open-world), and it is the right default for representing commonsense knowledge, where our ignorance is real. But it makes even counting brothers verbose. A different set of assumptions, called database semantics, changes three things at once:¹

• Unique-names assumption. Distinct constant symbols denote distinct objects. Under this rule $John$ and $Richard$ are guaranteed different without an asserted $John\ne Richard$, and at least two brothers needs no $x\ne y$.
• Closed-world assumption. Any ground atomic sentence not known to be true is assumed false. If the knowledge base does not list $Brother(Ted,Richard)$, then Ted is not Richard's brother — negation by absence rather than by proof.
• Domain closure. The only objects are the ones named by the constant symbols. There are no unnamed people lurking in the domain.

Under database semantics, a knowledge base of ground atoms has exactly one model, found by taking every listed fact as true and every unlisted one as false — how a relational database reads a table: the rows present are the whole truth. The trade is expressiveness for decidability and speed: you lose the ability to represent genuine uncertainty (some square holds a pit, I do not know which), but queries become lookups. Prolog and the query language Datalog adopt this reading, which is why their negation is negation as failure.

First-order versus higher-order logic

First-order logic quantifies over objects. The first-order qualifier is a restriction: variables range over domain objects and nothing else. A quantifier may not range over relations or functions. The sentence there is a relation that Richard and John both stand in — $\exists PP(Richard)\wedge P(John)$, with $P$ ranging over predicates — is not a first-order sentence. Allowing it gives higher-order logic, which can quantify over relations and functions as well as objects, and can state facts like two objects are equal iff they share every property, $\forall x,y(x=y)\iff (\forall PP(x)\iff P(y))$.²

Higher-order logic is strictly more expressive, but it has no complete proof procedure of the kind first-order logic has, so the inference machinery of the next lesson does not extend to it. Much of what looks higher-order can be re-expressed at first order by reifying — turning a relation into an object. Instead of $\exists PP(Richard)\wedge P(John)$, introduce a constant naming each relation and a predicate $Holds$ relating an object to a reified relation, then quantify over the relation-objects at first order. This move recurs whenever we want to talk about relations rather than merely use them, and it keeps us inside the tractable first-order fragment.

Using first-order logic

A knowledge base is built through a Tell/Ask interface. Sentences are added with $\text{Tell}$; the added sentences are assertions. Questions are posed with $\text{Ask}$; a question is a query or goal, and any query entailed by the knowledge base should be answered affirmatively.³ Asserting that John is a king, Richard is a person, and all kings are persons:

Then $\text{Ask}(KB,King(John))$ returns true, and so does $\text{Ask}(KB,Person(John))$, because it is entailed by the first and third assertions. A quantified query $\text{Ask}(KB,\exists xPerson(x))$ also returns true — but merely knowing that some $x$ works is not very useful, like answering can you tell me the time? with yes. To recover the witnessing object we use $\text{AskVars}(KB,Person(x))$, which returns a stream of substitutions (also called binding lists), here $\{x/John\}$ and $\{x/Richard\}$.

The kinship domain

The first substantial example is the domain of family relationships. The objects are people; there are two unary predicates $Male$ and $Female$; the relations are binary predicates $Parent$, $Sibling$, $Brother$, $Sister$, $Child$, $Daughter$, $Son$, $Spouse$, $Wife$, $Husband$, $Grandparent$, $Grandchild$, $Cousin$, $Aunt$, $Uncle$; and there are functions $Mother$ and $Father$, since every person has exactly one of each.⁴ We write down what we know about each symbol in terms of the others. One's mother is one's female parent:

One's husband is one's male spouse; male and female are disjoint; parent and child are inverses; a grandparent is a parent of a parent; a sibling is another child of one's parents:

Each of these is an axiom of the kinship domain — a basic fact from which conclusions follow. Because they have the biconditional form $\forall x,yP(x,y)\iff \dots$, they are also definitions: they define $Mother$, $Husband$, and the rest in terms of a smaller set of predicates ($Child$, $Spouse$, $Female$) that bottom out as primitives. Not every axiom is a definition — some predicates, like $Person$, we cannot fully characterize, so we state partial specifications ($\forall xPerson(x)\Rightarrow \dots$) instead.

Knowledge engineering

Constructing a knowledge base for a real domain is a discipline in its own right, called knowledge engineering: analyze the domain, choose a vocabulary, and encode the axioms needed to support the inferences you want. For a special-purpose domain whose queries are known in advance, Russell & Norvig give a seven-step process.⁵

The steps, in order:

Two features of the process matter most. First, steps three and four iterate: writing the axioms almost always reveals that the vocabulary has a gap or a misconception, sending you back to fix it. Second, an incorrect axiom can be spotted on its own, because it is a false statement about the world independent of the rest of the knowledge base — $\forall xNumOfLegs(x,4)\Rightarrow Mammal(x)$ is simply false of tables and can be judged so in isolation. A missing axiom is harder: it shows up only as a chain of reasoning that stops unexpectedly, so debugging often means noticing which query fails and asking why.

Worked example: a one-bit full adder

AIMA carries the seven steps all the way through on a digital-circuit domain. The task (step 1) is circuit verification: given a gate-level design, confirm that it computes the function it should, and recover its input-output table by inference rather than by writing a special-purpose simulator. The device is a one-bit full adder: three inputs — two addend bits and a carry-in — and two outputs — a sum bit and a carry-out. It is built from two XOR gates, two AND gates, and one OR gate.⁶

The vocabulary (step 3) has to name gates, their types, their terminals, the signals on those terminals, and the connections between terminals. Gates and circuits are objects; terminals are objects named by functions $In(i,g)$ and $Out(i,g)$ for the $i$-th input or output of gate $g$. A predicate $Type(g,t)$ records that gate $g$ is of type $t$ (one of the constants $XOR$, $AND$, $OR$, $NOT$); a function $Signal(w)$ gives the value on a terminal, one of the two signal constants $1$ and $0$; and a predicate $Connected(t_1,t_2)$ says two terminals are wired together.

The general axioms (step 4) say how each gate type maps inputs to outputs, and how a wire equalizes the signals on the two terminals it joins. Two terminals that are connected carry the same signal, and $Connected$ is symmetric:

Every terminal carries one of the two signals, and the two signals are distinct. The behavior of an OR gate — its output is $1$ exactly when some input is $1$ — and of an AND gate — its output is $0$ exactly when some input is $0$ — are stated over the terminals of a gate of that type:

The XOR and NOT axioms are similar. The problem instance (step 5) is the specific adder $C_1$: assert $Type(X_1,XOR)$, $Type(X_2,XOR)$, $Type(A_1,AND)$, $Type(A_2,AND)$, $Type(O_1,OR)$, and the $Connected$ facts for every wire in the figure — $Connected(Out(1,X_1),In(1,X_2))$, and so on.

Now the query (step 6). To recover the full input-output behavior, ask for every assignment of the three input signals that yields a given pair of outputs — a $\text{AskVars}$ query with the three input signals and two output signals left as variables:

The inference procedure returns the substitutions — the eight rows of the adder's truth table — including $\{i_1/1,i_2/1,i_3/0,o_1/0,o_2/1\}$: adding $1+1$ with no carry-in gives sum bit $0$ and carry-out $1$. The same axioms answer the reverse question, which inputs produce carry-out $1$?, by fixing $o_2=1$ and leaving the inputs free. That one encoding serves both directions is the point of the declarative approach: encode the domain once, and the inference procedure serves every query. Debugging (step 7) here mostly catches missing $Connected$ facts, which show up as a terminal whose signal the procedure cannot derive.

Decidable fragments and modern reasoners

First-order validity is undecidable, a result due to Church and Turing in 1936: no algorithm decides, for an arbitrary FOL sentence, whether it is valid. Modern work does not fight this head-on; it identifies well-behaved fragments and builds fast engines for them, and this is where FOL now touches deployed systems.

SMT solvers decide satisfiability of quantifier-limited first-order formulas modulo a background theory — linear arithmetic, bit-vectors, arrays, uninterpreted functions — by combining a SAT solver over the Boolean structure with dedicated theory solvers. De Moura and Bjørner's Z3, presented at TACAS 2008, is the reference implementation and now underlies program verifiers, symbolic-execution engines, and type checkers.⁷ Where the previous lesson's DPLL decided propositional formulas, SMT lifts that to formulas whose atoms are first-order constraints like $x+2y\le 5$.

Description logics are decidable fragments of FOL tailored to defining concepts and reasoning about subsumption between them. Baader and colleagues' Description Logic Handbook (2003) sets out the family, and the W3C standardized one of them as OWL (Web Ontology Language, 2004), whose formal underpinning is the description logic $\mathcal{S}\mathcal{HO}\mathcal{I}\mathcal{N}$.⁸ An OWL ontology is, semantically, a set of FOL sentences restricted so that classification and consistency checking stay decidable — the trade the database-semantics discussion above made, formalized and pushed further.

Datalog restricts FOL to function-free Horn rules under database semantics, which makes query answering decidable and, in the absence of recursion through negation, computable in polynomial time. Long studied as a database query language, it has returned as a substrate for static program analysis: the Soufflé engine (Scholz and colleagues, CAV 2016) compiles Datalog to fast parallel C++, and the Doop framework uses it to specify points-to analyses for Java as a few hundred declarative rules.⁹ These are the same $Tell$/$Ask$ ideas from this lesson, narrowed to fragments where the let the inference procedure serve every query promise comes with a runtime guarantee.