4.15 First-order logic, and inference in it

What this is and why it exists

Propositional logic has one wall and you hit it immediately. To say that every student who submits on time passes, you need one sentence per student. Add a student and the knowledge base needs editing. The logic has no way to say anything about all of something, because it has no notion of a something — only symbols that are true or false. First-order logic adds objects, relations between them, and quantifiers, and that is enough to say a general thing once. Unification and the two chaining directions are what make reasoning over it mechanical rather than a matter of insight. Every rule engine you meet afterwards, including the expert systems at the end of this module, is a restricted version of what is here.

The vocabulary

• Constant — a name for one particular object.
• Variable — a placeholder standing for some object.
• Predicate — a relation that holds or does not hold of its arguments.
• Function — a term that names an object in terms of others.
• Universal quantifier — for every object, this holds.
• Existential quantifier — for at least one object, this holds.
• Substitution — a mapping from variables to terms.
• Unifier — a substitution making two expressions identical.
• Most general unifier — the unifier committing to the least.
• Forward chaining — from known facts towards their consequences.
• Backward chaining — from a goal towards the facts supporting it.

The mental model

The world is objects, and sentences say things about them. Constants name objects, predicates say what holds of them, functions name one object in terms of another. On top of that sit the two quantifiers, and one sentence can now cover an unbounded collection. Getting the two the right way round is where most mistakes live, and the reliable habit is that a universal statement almost always sits above an implication, while an existential statement almost always sits above a conjunction. Swap those and you have said either that everything is a student, or that some one thing happens to satisfy an implication vacuously, which is nearly always not what was meant.

Test every translation against a small world you invented. Write down four or five objects and what holds of them, then check that your sentence comes out true where it should and false where it should. Build the second world deliberately — the one where the sentence ought to fail. Almost every mistranslation survives the first test and dies in the second, which is why doing only the first is worse than doing neither.

Unification is the mechanism underneath everything that follows. Given two expressions, find the substitution that makes them identical. Knows Ram with Knows x unifies by mapping x to Ram. Knows Ram y with Knows x Sita unifies by mapping x to Ram and y to Sita. Some pairs have no unifier at all, and some have many — of which one is the most general, committing to the least and leaving every other unifier reachable from it. Always take the most general one. A unifier that decides more than it had to has thrown away conclusions you might have needed, and nothing later will tell you they are missing.

With unification in hand there are two directions to reason, and they suit different work. They reach the same conclusions and they get there by opposite routes.

Forward chaining starts from the facts. Take everything known, find every rule whose conditions are satisfied, add what those rules conclude, and repeat until nothing new appears. It suits a situation where facts arrive and you want their consequences without having been asked a question — a monitoring system watching readings and deriving that a state has been entered. Its weakness is that it derives everything derivable, including a great deal nobody wanted.

Backward chaining starts from the question. Take the goal, find rules that would conclude it, and make their conditions into new goals, recursing until you reach known facts or run out. It suits diagnosis: you have a hypothesis and want to know what would confirm it, and you would rather not derive the whole world to find out. Its weakness is repeated work on shared subgoals, and it can loop on rules that refer back to themselves.

Resolution lifts to first-order logic by adding unification to the rule. The clauses now contain variables, so two clauses combine whenever one holds something that unifies with the negation of something in the other. The proof still runs by refutation — negate the goal, derive a contradiction — and it is still complete, which is the property that made the machinery worth building. The chaining methods are the practical restrictions of this, fast because they give up generality that most real knowledge bases never use.

What you should now be able to explain or do

Write objects, relations, functions and both quantifiers in first-order syntax, and place each quantifier over the right connective. Translate English into first-order logic and check the result on a world built to make it fail. Unify two expressions and produce the most general unifier, and say what taking a less general one costs. Run forward chaining from a set of facts, and say what kind of problem it suits. Run backward chaining from a goal, name the problem it suits, and name its two weaknesses. Describe resolution with unification and explain why it is refutation-based.

Check yourself