--- title: First-Order Logic in Use module: Logic and Planning moduleNumber: 3 lessonNumber: 4 order: 304 summary: > With the language of first-order logic in hand, this part is about using it well. Database semantics trades expressive power for the convenience of a single intended model; higher-order logic shows what first-order logic gives up for decidability. Then we put the language to work: the Tell/Ask interface, the kinship domain axiomatized from scratch, and the seven-step knowledge-engineering process applied to a digital circuit. topics: [Logic] sources: - book: AIMA ref: "§8.2.8 Database Semantics; §8.3 Using First-Order Logic; §8.4 Knowledge Engineering in First-Order Logic" --- This builds on [First-Order Logic](/artificial-intelligence/logic-and-planning/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 $\neq$ 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:[^aima-db] - **Unique-names assumption.** Distinct constant symbols denote distinct objects. Under this rule $John$ and $Richard$ are guaranteed different without an asserted $John \neq Richard$, and "at least two brothers" needs no $x \neq 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. $$ % caption: The same three brother-facts under two semantics. Standard semantics % (left) admits many models — the two named constants may coincide, and unnamed % objects may exist — so few sentences are entailed. Database semantics (right) % admits exactly one model: distinct names, no unlisted facts, no unnamed % objects, which is how relational databases read their tables. \begin{tikzpicture}[>=stealth, font=\small, world/.style={draw, minimum width=32mm, minimum height=24mm, align=center, font=\footnotesize}, hdr/.style={font=\footnotesize, text=black}] \definecolor{acc}{HTML}{2348F2} % left: many models \node[hdr] at (0,1.9) {standard semantics}; \node[world] (m1) at (-0.5,0.3) {}; \node[world] (m2) at (0,-0.1) {}; \node[world, fill=white] (m3) at (0.5,-0.5) {many models}; \node[font=\scriptsize, anchor=north, align=center, text=black] at (0,-2.1) {names may coincide; \\ unnamed objects allowed}; % right: one model \node[hdr] at (5.5,1.9) {database semantics}; \node[world, draw=acc, text=acc] (d) at (5.5,-0.2) {one model}; \node[font=\scriptsize, anchor=north, align=center, text=black] at (5.5,-2.1) {distinct names; unlisted \\ facts false; no extras}; \end{tikzpicture} $$ 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 P \; P(Richard) \land 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) \Leftrightarrow (\forall P \; P(x) \Leftrightarrow P(y))$.[^aima-higher] 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 P \; P(Richard) \land 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 $\textsc{Tell}$; the added sentences are **assertions**. Questions are posed with $\textsc{Ask}$; a question is a **query** or **goal**, and any query entailed by the knowledge base should be answered affirmatively.[^aima-tellask] Asserting that John is a king, Richard is a person, and all kings are persons: $$ \begin{aligned} & \textsc{Tell}(KB,\ King(John)) \\ & \textsc{Tell}(KB,\ Person(Richard)) \\ & \textsc{Tell}(KB,\ \forall x \; King(x) \Rightarrow Person(x)) \end{aligned} $$ Then $\textsc{Ask}(KB, King(John))$ returns _true_, and so does $\textsc{Ask}(KB, Person(John))$, because it is entailed by the first and third assertions. A quantified query $\textsc{Ask}(KB, \exists x \; Person(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 $\textsc{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.[^aima-kinship] We write down what we know about each symbol in terms of the others. One's mother is one's female parent: $$ \forall m, c \; Mother(c) = m \Leftrightarrow Female(m) \land Parent(m, c). $$ 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: $$ \begin{aligned} & \forall w, h \; Husband(h, w) \Leftrightarrow Male(h) \land Spouse(h, w), \\ & \forall x \; Male(x) \Leftrightarrow \lnot Female(x), \\ & \forall p, c \; Parent(p, c) \Leftrightarrow Child(c, p), \\ & \forall g, c \; Grandparent(g, c) \Leftrightarrow \exists p \; Parent(g, p) \land Parent(p, c), \\ & \forall x, y \; Sibling(x, y) \Leftrightarrow x \neq y \land \exists p \; Parent(p, x) \land Parent(p, y). \end{aligned} $$ 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, y \; P(x, y) \Leftrightarrow \ldots$, 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 x \; Person(x) \Rightarrow \ldots$) instead. > **Definition (Axiom).** A sentence asserted directly into the knowledge base, > providing basic factual information from which other conclusions can be derived. > Axioms that have a biconditional form define one symbol in terms of others. > **Theorem.** A sentence entailed by the axioms rather than asserted. For > example, the symmetry of siblinghood, $\forall x, y \; Sibling(x, y) > \Leftrightarrow Sibling(y, x)$, follows logically from the definition of > $Sibling$ above; $\textsc{Ask}$-ing it returns _true_. Logically a knowledge > base needs only axioms, but recording useful theorems reduces the cost of > deriving new sentences. ## 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.[^aima-ke] $$ % caption: The seven-step knowledge-engineering process (after AIMA §8.4.1). Steps % 3 and 4 iterate — encoding the axioms routinely exposes gaps in the vocabulary % that send you back to revise it — and step 7 debugging feeds back into all the % earlier steps. \begin{tikzpicture}[>=stealth, font=\small, stepn/.style={draw, minimum width=44mm, minimum height=9mm, align=center, font=\footnotesize}] \definecolor{acc}{HTML}{2348F2} \node[stepn] (s1) at (0,0) {1. Identify the task}; \node[stepn] (s2) at (0,-1.2) {2. Assemble the knowledge}; \node[stepn, draw=acc, text=acc] (s3) at (0,-2.4) {3. Decide on a vocabulary}; \node[stepn, draw=acc, text=acc] (s4) at (0,-3.6) {4. Encode general axioms}; \node[stepn] (s5) at (0,-4.8) {5. Encode the problem instance}; \node[stepn] (s6) at (0,-6.0) {6. Pose queries to inference}; \node[stepn] (s7) at (0,-7.2) {7. Debug the knowledge base}; \draw[->, thick] (s1) -- (s2); \draw[->, thick] (s2) -- (s3); \draw[->, thick] (s3) -- (s4); \draw[->, thick] (s4) -- (s5); \draw[->, thick] (s5) -- (s6); \draw[->, thick] (s6) -- (s7); % iteration loop 4 -> 3 \draw[->, acc, thick] (s4.east) to[bend left=42] node[right, font=\scriptsize, text=acc] {revise} (s3.east); % debug feedback 7 -> 3, routed wide left of all boxes so the label clears them \draw[->, black] (s7.west) to[out=170, in=190, looseness=1.5] node[left, font=\scriptsize, text=black, pos=0.5] {debug} (s3.west); \end{tikzpicture} $$ The steps, in order: ```algorithm caption: $\textsc{Knowledge-Engineering}$ — build a special-purpose first-order knowledge base input: an informal description of a domain and its intended queries identify the task // which questions must the KB answer, which facts are given? assemble the relevant knowledge // understand how the domain works (knowledge acquisition) decide on a vocabulary of predicates, functions, and constants // fix the ontology encode general axioms over the vocabulary // settles what the terms mean; may expose gaps if the vocabulary has a gap or misconception then return to the vocabulary step and iterate encode a description of the specific problem instance // atomic sentences about this case pose queries to the inference procedure // let it derive the answers debug the knowledge base // wrong or missing answers reveal missing or too-weak axioms ``` 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 x \; NumOfLegs(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.[^aima-adder] 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. $$ % caption: The one-bit full adder $C_1$ (after AIMA Fig. 8.6): inputs $In(1)$, % $In(2)$, $In(3)$ and outputs $Out(1)$ (sum) and $Out(2)$ (carry). Two XOR gates % ($X_1$, $X_2$), two AND gates ($A_1$, $A_2$), one OR gate ($O_1$). The $Connected$ % predicate records each wire; $Signal$ gives the bit on each terminal. \begin{tikzpicture}[>=stealth, font=\small, gate/.style={draw, minimum width=15mm, minimum height=10mm, align=center, font=\footnotesize}, term/.style={font=\scriptsize, text=black}, dotj/.style={circle, fill=black, minimum size=3pt, inner sep=0pt}] \definecolor{acc}{HTML}{2348F2} % gates \node[gate, draw=acc, text=acc] (x1) at (3.2,3.6) {XOR \\ X1}; \node[gate] (a2) at (3.2,1.4) {AND \\ A2}; \node[gate, draw=acc, text=acc] (x2) at (6.6,3.6) {XOR \\ X2}; \node[gate] (a1) at (6.6,1.4) {AND \\ A1}; \node[gate] (o1) at (9.4,0.1) {OR \\ O1}; % input labels \node[term, anchor=east] at (-0.1,3.9) {In(1)}; \node[term, anchor=east] at (-0.1,3.3) {In(2)}; \node[term, anchor=east] at (-0.1,0.5) {In(3)}; % In(1): to X1 top input; branch down at x=0.4 to A2 top input \draw[->] (0.0,3.9) -- (x1.160); \node[dotj] at (0.4,3.9) {}; \draw[->] (0.4,3.9) -- (0.4,1.7) -- (a2.160); % In(2): to X1 bottom input; branch down at x=1.0 to A2 bottom input \draw[->] (0.0,3.3) -- (x1.200); \node[dotj] at (1.0,3.3) {}; \draw[->] (1.0,3.3) -- (1.0,1.1) -- (a2.200); % In(3): up at x=1.6 to X2 bottom input; branch right to A1 bottom input \draw[->] (0.0,0.5) -- (1.6,0.5) -- (1.6,3.3) -- (x2.200); \node[dotj] at (1.6,0.5) {}; \draw[->] (1.6,0.5) -- (5.0,0.5) -- (5.0,1.1) -- (a1.200); % X1 out -> X2 top input; branch down at x=4.9 to A1 top input \draw[->, acc] (x1.east) -- (4.9,3.6) -- (x2.160); \node[dotj] at (4.9,3.6) {}; \draw[->] (4.9,3.6) -- (4.9,1.7) -- (a1.160); % A2 out -> down and across below A1 -> O1 top input \draw[->] (a2.east) -- (5.5,1.4) -- (5.5,0.7) -- (8.3,0.7) -- (8.3,0.4) -- (o1.160); % A1 out -> down -> O1 bottom input \draw[->] (a1.east) -- (8.6,1.4) -- (8.6,-0.2) -- (o1.200); % outputs \draw[->, acc] (x2.east) -- node[term, above] {Out(1) sum} (10.9,3.6); \draw[->] (o1.east) -- node[term, above] {Out(2) carry} (11.7,0.1); \end{tikzpicture} $$ 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: $$ \forall t_1, t_2 \; Connected(t_1, t_2) \Rightarrow Signal(t_1) = Signal(t_2), \qquad \forall t_1, t_2 \; Connected(t_1, t_2) \Leftrightarrow Connected(t_2, t_1). $$ 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: $$ \begin{aligned} & \forall g \; Type(g, OR) \Rightarrow \big( Signal(Out(1, g)) = 1 \Leftrightarrow \exists n \; Signal(In(n, g)) = 1 \big), \\ & \forall g \; Type(g, AND) \Rightarrow \big( Signal(Out(1, g)) = 0 \Leftrightarrow \exists n \; Signal(In(n, g)) = 0 \big). \end{aligned} $$ 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 $\textsc{AskVars}$ query with the three input signals and two output signals left as variables: $$ \exists i_1, i_2, i_3, o_1, o_2 \;\; \begin{aligned}[t] & Signal(In(1, C_1)) = i_1 \land Signal(In(2, C_1)) = i_2 \land Signal(In(3, C_1)) = i_3 \\ & {}\land Signal(Out(1, C_1)) = o_1 \land Signal(Out(2, C_1)) = o_2. \end{aligned} $$ 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.[^z3] 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$. $$ % caption: Decidable islands inside undecidable first-order logic. Full FOL % validity is undecidable (Church-Turing, 1936); Datalog, the guarded fragment, % and description logics carve out fragments where satisfiability or query % answering is decidable, and SMT decides quantifier-limited formulas over % specific background theories. \begin{tikzpicture}[>=stealth, font=\small, box/.style={draw, align=center, font=\footnotesize}] \definecolor{acc}{HTML}{2348F2} \definecolor{red}{HTML}{C0392B} % outer undecidable region \node[draw=red, text=red, minimum width=86mm, minimum height=44mm, align=center, font=\footnotesize] (fol) at (0,0) {}; \node[font=\footnotesize, text=red, anchor=north west] at (-4.1,2.0) {full FOL: undecidable}; % inner decidable fragments \node[box, draw=acc, text=acc, minimum width=22mm] (dl) at (-2.4,0.4) {Datalog}; \node[box, draw=acc, text=acc, minimum width=24mm] (gf) at (0.6,0.9) {guarded \\ fragment}; \node[box, draw=acc, text=acc, minimum width=28mm] (desc) at (-1.6,-1.1) {description \\ logics / OWL}; \node[box, minimum width=26mm] (smt) at (2.3,-0.8) {SMT theories}; \end{tikzpicture} $$ **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{SHOIN}$.[^owl] 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.[^souffle] 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. [^aima-tellask]: **AIMA**, §8.3.1 — Assertions and queries in first-order logic: the Tell/Ask interface, assertions, queries/goals, and AskVars returning substitutions (binding lists) for the variables in a query. [^aima-kinship]: **AIMA**, §8.3.2 — The kinship domain: unary predicates $Male$/$Female$, binary kinship predicates, the $Mother$/$Father$ functions, biconditional axioms that are also definitions, and the axiom/theorem distinction. [^aima-ke]: **AIMA**, §8.4.1 — The knowledge-engineering process: the seven steps (identify the task, assemble knowledge, decide on a vocabulary/ontology, encode general axioms, encode the problem instance, pose queries, debug), and the difference between spotting incorrect versus missing axioms. [^aima-db]: **AIMA**, §8.2.8 — Database semantics: the unique-names assumption, the closed-world assumption, and domain closure, and how together they give a set of ground atoms exactly one model, as in a relational database. [^aima-higher]: **AIMA**, §8.2.8 (and Ch. 8 discussion) — Higher-order logic quantifies over relations and functions as well as objects; it is more expressive but lacks a complete proof procedure, and reification lets many higher-order-looking statements be expressed at first order. [^aima-adder]: **AIMA**, §8.4.2, Figure 8.6 — The digital-circuits domain: a one-bit full adder built from two XOR, two AND, and one OR gate; vocabulary of $Type$, $In$/$Out$ terminal functions, $Signal$, and $Connected$; general gate axioms; and circuit-verification queries that recover the input-output table. [^z3]: Leonardo de Moura and Nikolaj Bjørner, "Z3: An Efficient SMT Solver," _Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_, 2008. SMT combines a SAT solver over the Boolean structure of a formula with decision procedures for background theories such as linear arithmetic, bit-vectors, and arrays. [^owl]: Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter Patel-Schneider (eds.), _The Description Logic Handbook_, Cambridge University Press, 2003. The W3C published the OWL Web Ontology Language recommendation in 2004; OWL DL corresponds to the description logic $\mathcal{SHOIN}(\mathbf{D})$, a decidable fragment of first-order logic. [^souffle]: Bernhard Scholz, Herbert Jordan, Pavle Subotić, and Till Westmann, "On Fast Large-Scale Program Analysis in Datalog," _Compiler Construction (CC)_, 2016; the Soufflé engine compiles Datalog to parallel C++. Datalog restricts first-order logic to function-free Horn clauses under database semantics, keeping query answering decidable.