Logic and knowledge systems: forward and backward chaining, resolution and expert systems

The knowledge base, entailment and model checking, Horn clauses, forward and backward chaining, resolution, Prolog and expert systems from MYCIN to knowledge graphs — on a small system that identifies an animal.

15 minutes Matěj Žalmánek 2026-10-15

Series AI basics Part 24 of 52

Full series syllabus 52 of 83 topics published

What you will take away

What it means for something to follow from a knowledge base, and why checking all possible worlds is unusably slow.
How forward and backward chaining draw conclusions from “if–then” rules, and when to use which.
Why expert systems succeeded and then hit their limits, and where hand-written knowledge lives on today.

Useful to know first: Logic and proofs: the rules AI reasons by

Before machines started learning from data, people tried to teach artificial intelligence by hand: write down what an expert knows as “if–then” rules and let the computer draw conclusions from them. That is how the expert systems of the 1970s and 1980s came about, diagnosing infections or configuring computers to order. Then they hit their limits and an AI winter set in. Their ideas did not disappear, though — they live on in Prolog, in the knowledge bases behind search engines and in checking what language models claim.

This part follows on from Logic and proofs, where you will find connectives, implication and modus ponens.

1. The knowledge base and the inference engine

Definition — knowledge base

Let 𝒫 be a finite set of propositional symbols and 𝓛(𝒫) the set of all sentences (formulas) of propositional logic over 𝒫, i.e. expressions built from the symbols of 𝒫 with the connectives ¬, ∧, ∨, ⇒, ⇔ (see Logic and proofs). A knowledge base is a finite set of sentences

KB ⊆ 𝓛(𝒫)

that the system takes to be true. The system can do two operations with it:

tell a sentence β ∈ 𝓛(𝒫): KB ← KB ∪ {β};
ask about a sentence α ∈ 𝓛(𝒫): the answer is “yes” if and only if KB entails α (KB ⊨ α, defined in the next section), otherwise “no”.

An inference engine is an algorithm that answers the “ask” operation.

In plain words

A knowledge base is a notebook in which you write down what is true: “every animal with fur is a mammal”, “this animal has fur”. The inference engine is the one who leafs through the notebook and answers questions, even when the answer is not written in it directly.

This approach is called declarative. You do not program the procedure for reaching the answer — you only write down what is true, and the procedure is always the same inference engine. Want to teach the system something new? You add a sentence; you rewrite nothing.

Throughout this part we will be accompanied by a small expert system modelled on Patrick Winston’s textbook ZOOKEEPER: twelve rules that identify an animal from its observed properties. We have observed an animal that has fur, sharp teeth and claws, is tawny and has black stripes. What is it?

2. Entailment and models

Definition — model and entailment

Let 𝒫 be a finite set of propositional symbols. An assignment is a function m : 𝒫 → {0, 1} (1 = true, 0 = false); we extend the truth value m(α) ∈ {0, 1} to every sentence α ∈ 𝓛(𝒫) by the usual truth tables of the connectives. An assignment m is a model of the sentence α if and only if m(α) = 1. The sets of models of a sentence α and of a knowledge base KB ⊆ 𝓛(𝒫) are

M(α) = {m : 𝒫 → {0, 1} : m(α) = 1}, M(KB) = ⋂_{β ∈ KB} M(β)

(for KB = ∅, M(KB) is the set of all 2^|𝒫| assignments). KB entails α, written KB ⊨ α, if and only if

M(KB) ⊆ M(α).

In words: α holds in every assignment in which all the sentences of the base hold.

In plain words

A model is one “possible world” — one combination of what is true and what is not. Entailment means: whatever the world is like, if everything in the notebook holds in it, α holds in it too. It is not about what is likely but about what is inevitable.

KB ⊨ α ⇔ M(KB) ⊆ M(α)

KB ⊨ α: what we are asking: does α follow from the base? The symbol ⊨ speaks about truth in worlds, not about whether we can derive something
M(KB): the worlds the base allows — assignments in which all its sentences hold at once (the base is their conjunction); other worlds do not interest us, the base claims they did not happen
⊆: inclusion: α must not be missing from any allowed world; a single counterexample would be enough for α not to be entailed
M(α): the worlds in which α holds; there may be many more of them — α may also hold where the base does not

The more the base knows, the fewer worlds it allows and the more it entails. An empty base allows every world, so it entails only tautologies.

The most straightforward way to check entailment is model checking: go through all assignments, pick those in which the whole base holds, and see whether the query holds in them too. Our base has 24 propositional symbols (“has fur”, “mammal”, “tiger”…), so there are 2²⁴ = 16,777,216 assignments. Of these, 13,440 are models of the base — and “tiger” holds in all of them. The answer is yes, but at the cost of sixteen million rows of a truth table. Each additional symbol doubles the count; for a base with hundreds of symbols it would never finish.

Example — model checking with three symbols

Base KB = {rains ⇒ wet, wet ⇒ slippery, rains}, query α = slippery. Three symbols give 2³ = 8 assignments (1 = true, 0 = false); the implication p ⇒ q is false only for p = 1, q = 0.

rains	wet	slippery	rains ⇒ wet	wet ⇒ slippery	`KB`
0	0	0	1	1	0
0	0	1	1	1	0
0	1	0	1	0	0
0	1	1	1	1	0
1	0	0	0	1	0
1	0	1	0	1	0
1	1	0	1	0	0
1	1	1	1	1	1

The whole base holds only in the last row, so |M(KB)| = 1. “Slippery” holds in that row too — M(KB) ⊆ M(slippery), and therefore KB ⊨ slippery. The algorithm went through 8 rows and evaluated the 3 sentences of the base in each; in general, model checking costs O(2ⁿ · |KB|).

Example — where the 13,440 models come from

In every model of the base the five observed facts hold, and rules R1, R6 and R9 then force “mammal”, “carnivore” and “tiger”. Those 8 symbols are fixed as true. The remaining 16 split into groups that are not connected to each other by any rule, and the numbers of their assignments multiply:

“gives milk” (R2 is satisfied, mammal holds) and “eats meat” (R5 is satisfied, carnivore holds): free, 2 · 2 = 4;
“has dark spots”, “cheetah” with rule R8: three assignments — spots without the cheetah are not allowed;
“has hooves”, “ungulate”, “has long neck”, “giraffe”, “zebra” with R7, R10, R11: if ungulate is false, hooves must be false too and the other three symbols are free (8 options); if it is true, zebra must hold, hooves are free and neck with giraffe have 3 options (2 · 3 = 6); 14 in total;
the bird group “has feathers”, “flies”, “lays eggs”, “bird”, “does not fly”, “swims”, “penguin” with R3, R4, R12: without the bird, neither feathers nor flies-and-eggs together may hold (3 options) and the last three symbols are free (8): 24; with the bird, feathers are free (2), flies and eggs are free (4) and of the eight assignments of “does not fly, swims, penguin” only 1, 1, 0 is forbidden (7): 56; 80 in total.

Altogether 4 · 3 · 14 · 80 = 13,440 — exactly as many as model checking counted. And tiger holds in every one of them, because it is among the symbols fixed as true.

3. Inference: sound and complete

Instead of going through worlds, we can manipulate sentences: produce new ones from those we have according to inference rules such as modus ponens. That is what people do too.

Definition — inference, soundness, completeness

Let 𝓛 = 𝓛(𝒫) be the set of sentences and 𝓡 a set of inference rules; each rule determines which sentence we may derive from which already derived sentences (for example modus ponens: from β and β ⇒ γ derive γ). Let KB ⊆ 𝓛 and α ∈ 𝓛. A derivation of the sentence α from KB is a finite sequence of sentences β₁, …, β_k such that β_k = α and for every i = 1, …, k, either β_i ∈ KB, or β_i is obtained by some rule from 𝓡 from the sentences β₁, …, β_i−1. We write

KB ⊢ α ⇔ a derivation of α from KB exists.

An inference procedure (a set of rules 𝓡, or an algorithm that uses them) is

sound if and only if for all KB ⊆ 𝓛 and α ∈ 𝓛, KB ⊢ α ⇒ KB ⊨ α — it derives only what is really entailed;
complete if and only if for all KB ⊆ 𝓛 and α ∈ 𝓛, KB ⊨ α ⇒ KB ⊢ α — it derives everything that is entailed.

Soundness and completeness are often claimed only for a narrower class of bases and queries (for example bases of Horn clauses and queries consisting of a single symbol); the quantifiers “for all” then range only over that class.

In plain words

The symbol ⊨ means “it is so”, the symbol ⊢ means “I can derive it”. A sound engine never makes up a falsehood. A complete engine misses nothing. We want both — and for general logic that is expensive, while for a simpler form of rules it is cheap.

Definition — Horn clause

Let 𝒫 be a set of propositional symbols. A literal is a symbol p ∈ 𝒫 (a positive literal) or its negation ¬p (a negative literal). A clause is a disjunction of finitely many literals ℓ₁ ∨ … ∨ ℓ_m, m ≥ 0 (for m = 0 the empty clause □, which is always false). A clause is

Horn if and only if at most one of its literals is positive;
definite if and only if exactly one of its literals is positive.

A definite clause ¬p₁ ∨ … ∨ ¬p_k ∨ q (k ≥ 0, p₁, …, p_k, q ∈ 𝒫) is written as a rule

p₁ ∧ p₂ ∧ … ∧ p_k ⇒ q,

where p₁, …, p_k are the premises and q the conclusion. For k = 0 it is a fact q. (That it is the same sentence is shown by the breakdown below.)

In plain words

A Horn clause is a rule “if this and this and this holds, then that holds”. No “or” in the conclusion, no “not” in the premises. It sounds like a big restriction, but most expert rules have exactly this form — and inference from them is fast.

Why is “a disjunction with at most one positive literal” the same thing as a rule? The implication A ⇒ q is equivalent to ¬A ∨ q, and by De Morgan’s law ¬(p₁ ∧ … ∧ p_k) is the same as ¬p₁ ∨ … ∨ ¬p_k:

¬p₁ ∨ … ∨ ¬p_k ∨ q ≡ (p₁ ∧ … ∧ p_k) ⇒ q

¬p₁ ∨ … ∨ ¬p_k: the negative literals of the clause; together they say “some premise does not hold” — and that is exactly the negation of the conjunction of the premises
(p₁ ∧ … ∧ p_k): the premises of the rule — the disjunction of negative literals became a condition thanks to De Morgan; none of them may be negative, otherwise the rule would say “if … does not hold”
q: the only positive literal, the conclusion; if two were positive, we would get “then q or r” and the inference engine would not know which of them to add
⇒: the clause is true when some premise does not hold or the conclusion holds — that is the definition of implication; the rule form just reads the same disjunction differently

For example R6, mammal ∧ has sharp teeth ∧ has claws ⇒ carnivore, is the clause ¬mammal ∨ ¬has sharp teeth ∨ ¬has claws ∨ carnivore.

4. Forward chaining

Algorithm — forward chaining

Input: a finite set KB of definite Horn clauses over 𝒫 — facts F ⊆ 𝒫 and rules r with a set of premises P(r) ⊆ 𝒫, |P(r)| ≥ 1, and a conclusion z(r) ∈ 𝒫.
Output: the set Known ⊆ 𝒫 of all derived symbols.

For every rule r set the counter missing(r) ← |P(r)| (how many of its premises are not yet known). Set Known ← ∅ and put all facts from F on the agenda (a queue).
If the agenda is empty, stop and return Known.
Take a symbol p from the agenda. If p ∈ Known, continue with step 2; otherwise Known ← Known ∪ {p}.
For every rule r with p ∈ P(r), decrease missing(r) by 1. If it drops to 0, the rule fires: put z(r) on the agenda. Continue with step 2.

Termination: step 4 runs at most once for each symbol and each rule fires at most once, so only finitely many symbols are ever added to the agenda.

Theorem. Let KB be a finite set of definite Horn clauses over 𝒫 and q ∈ 𝒫. Then forward chaining derives q (i.e. q ∈ Known) if and only if KB ⊨ q; it is therefore sound and complete for propositional symbols. The number of its steps is linear in the total length of the clauses of the base.

In plain words

You start from what you know and look at which rule that has “unlocked”. Every new conclusion can unlock another rule — like dominoes. You stop when nothing new falls. This is called data-driven inference.

Forward chaining: facts in the order they were processed, derived ones in green steps: 8

The very first observation, “has fur”, unlocks rule R1, which adds “mammal” to the end of the agenda. The remaining four observations do not trigger anything yet, but they lower the counters. When mammal’s turn comes, it unlocks R6 (sharp teeth and claws are already known) — and “carnivore” appears. Carnivore unlocks R9 and we have a tiger. In eight steps, not millions of rows. Rule R5 (“a mammal that eats meat is a carnivore”) never fired: we do not know that the animal eats meat — and we do not need to know it.

def dopredne(fakta, pravidla):
    chybi = {r.id: len(r.kdyz) for r in pravidla}
    zname, agenda = set(), list(fakta)
    while agenda:
        p = agenda.pop(0)
        if p in zname:
            continue
        zname.add(p)
        for r in pravidla:
            if p in r.kdyz:
                chybi[r.id] -= 1
                if chybi[r.id] == 0:          # all premises are known
                    agenda.append(r.pak)
    return zname

The heart of the algorithm is the counter of each rule r with premises P(r):

missing(r) = |P(r)| − |P(r) ∩ Known|

missing(r): how many premises we do not know yet; at missing(r) = 0 the rule fires — thanks to the number the engine notices it without going through the list of premises
|P(r)|: the initial value: at the start we know nothing, all premises are missing
|P(r) ∩ Known|: premises that have already been processed; each processed symbol lowers the counter by 1 for every rule in which it occurs — and it is processed only once, so nothing is counted twice

Each symbol is processed at most once and each occurrence of a premise lowers a counter at most once — hence linear time: the number of steps is proportional to the total length of the rules.

How the counters missing(r) drop during our run (after processing the symbol in the given row; zero, that is firing, in bold). In row 0 we still have missing(r) = |P(r)| (colours as in the formula above):

step	processed symbol	R1	R5	R6	R9	R8
0	—	1	2	3	3	3
1	has fur	0	2	3	3	3
2	has sharp teeth	0	2	2	3	3
3	has claws	0	2	1	3	3
4	is tawny	0	2	1	2	2
5	has black stripes	0	2	1	1	2
6	mammal	0	1	0	1	2
7	carnivore	0	1	0	0	1
8	tiger	0	1	0	0	1

R5 stops at one (“eats meat” is missing) and so does R8 for the cheetah (“has dark spots” is missing). The other rules are not in the table; their premises either did not appear in the run at all or only partly.

Theorem — forward chaining is sound and complete (proof)

Let KB be a finite set of definite Horn clauses over 𝒫 and Known the output of forward chaining. Then for every q ∈ 𝒫, q ∈ Known ⇔ KB ⊨ q.

Soundness (⇒). Every derived symbol came from the firing of a rule all of whose premises were already known. In every model of the base the facts hold and (by induction on the order of derivation) so do the previously derived symbols, so by the rule the new conclusion holds too — this is modus ponens.

Completeness (⇐). When the run ends, take the assignment m: true for the derived symbols (and facts), false for all others. This is a model of the base: if some rule p₁ ∧ … ∧ p_k ⇒ q did not hold in m, all the p_i would be derived and q not — but then the counter of the rule would have dropped to zero and q would have been derived. So if q is entailed by the base, it holds in the model m, and therefore it was derived. ∎

The model m is the “most modest” one: it believes only what it must. For our base it is the assignment in which exactly the 5 observations, mammal, carnivore and tiger hold.

5. Backward chaining

Algorithm — backward chaining

Input: a finite set KB of definite Horn clauses over 𝒫 (facts F ⊆ 𝒫 and rules), a goal q ∈ 𝒫 and a set C ⊆ 𝒫 of goals currently being proved higher up in the tree (at the start C = ∅).
Output: “proved” or “not proved”.

The procedure BACK(q, C):

If q ∈ F, return “proved”.
If q ∈ C, return “not proved” (the goal would prove itself — a cycle).
For every rule p₁ ∧ … ∧ p_k ⇒ q in KB: call BACK(p_i, C ∪ {q}) for i = 1, …, k in turn; if all the calls return “proved”, return “proved” (at the first failure, abandon this rule).
If no rule succeeded, return “not proved”.

Termination: each nested call has C larger by one symbol and 𝒫 is finite, so the depth of the recursion is at most |𝒫|.

Theorem. Let KB be a finite set of definite Horn clauses over 𝒫 and q ∈ 𝒫. Then BACK(q, ∅) returns “proved” if and only if KB ⊨ q. Backward chaining is thus sound and complete, and it examines only the symbols connected to the goal through the rules.

In plain words

You start with the question “is it a tiger?” and ask what would confirm it: a tiger is a tawny carnivore with black stripes. Is it a carnivore? A carnivore is a mammal that eats meat, or a mammal with sharp teeth and claws. Is it a mammal? … Until you reach what you know. This is called goal-driven inference.

def zpetne(cil, fakta, pravidla, cesta=()):
    if cil in fakta:
        return True                           # we know it directly
    if cil in cesta:
        return False                          # cycle: the goal proves itself
    for r in pravidla:
        if r.pak == cil:                      # OR: one rule is enough
            if all(zpetne(p, fakta, pravidla, cesta + (cil,))
                   for p in r.kdyz):          # AND: all premises must succeed
                return True
    return False                              # we do not know how to prove it

The function all stops at the first premise that fails — which is why, for R5, nothing more is examined after the failure with “eats meat”. The list cesta (path) makes sure that rules like “a ⇒ b, b ⇒ a” do not loop.

Backward chaining for the goal “tiger”: the labels under the nodes are rules

The algorithm examined 11 goals. It first tried to prove carnivore with rule R5 — it proved mammal, but ran into “eats meat”: we do not know that, so it gave up on R5 and tried R6, which succeeded. This is where backward chaining is strong: it knows what it is missing. At such a moment an expert system asks the user: “Does the animal eat meat?” The whole conversation with an expert system is really backward chaining out loud.

When to use which? Forward chaining suits situations where data keep arriving and you want to know what follows from them — monitoring a production line, say. Backward chaining suits a specific question — a diagnosis, a database query. If we asked “is it a zebra?”, backward chaining would refute it after examining just 5 goals: a zebra is an ungulate, and our animal has no hooves.

6. Resolution: inference for all of logic

Horn clauses are not enough for everything. The sentence “the animal is a mammal or a bird” has an “or” in its conclusion, and you cannot write it as a rule. For arbitrary propositions there is a single rule that is enough for everything.

Definition — resolution

Let 𝒫 be a set of propositional symbols. A sentence is in conjunctive normal form (CNF) if and only if it is a conjunction of finitely many clauses K₁ ∧ … ∧ K_s (for clauses see the definition of a Horn clause); we treat a clause as the set of its literals, so a repeated literal counts once.

The resolution rule. Let p ∈ 𝒫, let ℓ ∈ {p, ¬p} be a literal, ¬ℓ the literal opposite to it (we read ¬¬p as p), and A, B clauses (possibly empty). From the clauses (A ∨ ℓ) and (B ∨ ¬ℓ) we may derive their resolvent

(A ∨ ℓ), (B ∨ ¬ℓ) ⊢ (A ∨ B).

A sentence γ is unsatisfiable if and only if it has no model (M(γ) = ∅); likewise for a set of sentences.

Theorem (proof by contradiction). Let KB ⊆ 𝓛(𝒫) and α ∈ 𝓛(𝒫). Then KB ⊨ α if and only if KB ∪ {¬α} is unsatisfiable.

Theorem (Robinson, 1965). Let S be a finite set of clauses. Then S is unsatisfiable if and only if the empty clause □ can be derived from S by repeated application of the resolution rule.

A resolution proof of KB ⊨ α therefore converts KB ∪ {¬α} to CNF and derives resolvents until □ appears (a contradiction is found, α is entailed) or until no new clauses are added (α is not entailed; over a finite 𝒫 there are finitely many clauses, so this happens). The procedure is sound and refutation-complete.

In plain words

If “it rains or it is dry” holds and at the same time “it is not dry or it is windy”, then “it rains or it is windy” — the dryness cancels out (colours as in the formula below). Resolution proves by contradiction: it assumes the opposite of what it wants to prove and cancels clauses until an empty one is left — a contradiction. So the opposite does not hold.

( A ∨ ℓ ), ( B ∨ ¬ℓ ) ⊢ ( A ∨ B )

ℓ, ¬ℓ: complementary literals — in every world exactly one of them is true, so it fails to satisfy one of the clauses; that clause must be satisfied by its remainder. That is why ℓ is missing from the result
A: the remainder of the first clause: it holds whenever ℓ is false (then only A keeps the first clause true)
B: the remainder of the second clause: it holds whenever ℓ is true (then ¬ℓ does not hold and B keeps the second clause true)

Whatever ℓ is, one of the remainders must hold — that is the whole proof that resolution is sound. From (ℓ) and (¬ℓ) we get the empty clause, which nothing satisfies: a contradiction.

Algorithm — conversion to conjunctive normal form

Input: a sentence φ ∈ 𝓛(𝒫). Output: a sentence in CNF that has the same models as φ. Each step is repeated as long as it can be applied; each preserves the models and terminates, because it removes or moves finitely many connectives.

Eliminate equivalences: replace α ⇔ β with (α ⇒ β) ∧ (β ⇒ α).
Eliminate implications: replace α ⇒ β with ¬α ∨ β.
Move negations inwards to the symbols: ¬¬α ≡ α, ¬(α ∧ β) ≡ ¬α ∨ ¬β, ¬(α ∨ β) ≡ ¬α ∧ ¬β (De Morgan).
Distribute ∨ over ∧: α ∨ (β ∧ γ) ≡ (α ∨ β) ∧ (α ∨ γ).

Example: (rains ∨ snows) ⇒ wet

step 2: ¬(rains ∨ snows) ∨ wet

step 3: (¬rains ∧ ¬snows) ∨ wet

step 4: (¬rains ∨ wet) ∧ (¬snows ∨ wet) — two clauses, both of them even Horn clauses.

Distributing in step 4 can make the formula exponentially longer; in practice solvers therefore use the Tseitin transformation with auxiliary symbols, which gives a result that is only linearly longer (and satisfiable exactly when the original formula is).

Example: the base {rains ⇒ wet, wet ⇒ slippery, rains}, query “slippery”. In normal form and with the negated query added:

(¬rains ∨ wet), (¬wet ∨ slippery), (rains), (¬slippery)

(rains) and (¬rains ∨ wet) give (wet); (wet) and (¬wet ∨ slippery) give (slippery); (slippery) and (¬slippery) give the empty clause □. A contradiction — “slippery” is entailed by the base. (Colours as in the breakdown of the resolution rule above: in every step A is empty, ℓ, ¬ℓ cancel out and B remains.)

Resolution is universal but expensive in general: for propositional logic the satisfiability problem (SAT) is NP-complete. Modern SAT solvers nevertheless handle millions of variables — we talked about them in the part on constraint satisfaction.

7. Rules with variables and Prolog

Propositional logic has a flaw: “Rex is a mammal” and “Kitty is a mammal” are two unrelated symbols for it. A rule about all mammals would have to be copied out for every animal separately. Predicate logic from the part on logic and proofs solves this with variables: ∀x : has_fur(x) ⇒ mammal(x).

Definition — unification

Let sets of variables (X, Y, …), constants (jan, petr, …) and function and predicate symbols be given. A term is a variable, a constant, or f(t₁, …, t_k) for a function symbol f and terms t₁, …, t_k; an atomic formula is P(t₁, …, t_k) for a predicate symbol P. Together we call both expressions.

A substitution is a finite set θ = {X₁ / t₁, …, X_n / t_n}, where X₁, …, X_n are pairwise distinct variables and t_i ≠ X_i are terms; we read X / t as “substitute t for X” (it is not division). For an expression E, Eθ is the expression obtained by simultaneously replacing every occurrence of X_i with the term t_i.

Let E₁, E₂ be expressions. A substitution θ is their unifier if and only if

E₁θ = E₂θ.

A unifier θ is the most general one if and only if for every unifier σ of the expressions E₁, E₂ there is a substitution λ such that Eσ = (Eθ)λ for every expression E — every other unifier is just a further refinement of it. For example rodič(jan, Y) and rodič(X, petr) (rodič = parent) are unified (most generally) by the substitution {X / jan, Y / petr}. The unification algorithm (below) finds the most general unifier if any unifier exists, and otherwise reports failure.

In plain words

Unification is “find what to substitute so that it fits”. When a rule talks about some x and you ask about Rex, unification substitutes x = Rex and the rule can be used. Chaining then works just as in propositional logic, only with substitution.

def unifikuj(a, b, s):                    # s: substitution found so far (a dict)
    if s is None:
        return None                           # it already failed earlier
    a, b = dosad(a, s), dosad(b, s)           # apply what we already know
    if a == b:
        return s
    if je_promenna(a):
        return None if vyskytuje_se(a, b) else {**s, a: b}
    if je_promenna(b):
        return None if vyskytuje_se(b, a) else {**s, b: a}
    if slozeny(a) and slozeny(b) and a.jmeno == b.jmeno and len(a.args) == len(b.args):
        for x, y in zip(a.args, b.args):      # arguments one after another
            s = unifikuj(x, y, s)
        return s
    return None                               # different constants or predicates

On the example rodič(jan, Y) and rodič(X, petr): the predicates match, so the arguments are compared. jan and X give {X / jan}, Y and petr add Y / petr. On the other hand rodič(jan, Y) and rodič(petr, eva) do not unify — jan and petr are different constants. The vyskytuje_se (occurs) check prevents a substitution like X / f(X), which would lead to an infinite expression. (Prolog leaves it out by default for speed.)

Prolog (Alain Colmerauer, Marseille, 1972) is built on backward chaining with unification — a language in which the program is a knowledge base and running the program is a query (rodic = parent, prarodic = grandparent, kdo = who):

rodic(jan, petr).
rodic(petr, eva).

prarodic(X, Z) :- rodic(X, Y), rodic(Y, Z).

?- prarodic(jan, Kdo).
Kdo = eva.

Prolog works its way to the goal prarodic(jan, Kdo) exactly like our tree for the tiger: it finds the rule, unifies X = jan, proves rodic(jan, Y), finds Y = petr and then rodic(petr, Z) with the result eva.

8. Expert systems

An expert system is a knowledge base written down together with an expert plus an inference engine, usually with backward chaining and with the ability to explain why it reached a conclusion — it is enough to read the tree we drew above. The three best known were:

DENDRAL (Stanford, from 1965) determined the structure of molecules from mass spectrometer data — the first system that did scientists’ work according to their own rules.
MYCIN (Stanford, 1970s) diagnosed bacterial blood infections and recommended antibiotics. It had about six hundred rules, and in an evaluation from 1979 its recommendations held up as well as or better than those of Stanford specialists. Even so, it was never used in a hospital.
XCON (DEC, from 1980) put together configurations of VAX computers according to the order. It had thousands of rules and, according to the company, saved tens of millions of dollars a year.

Medicine, however, rarely knows certainty. MYCIN therefore attached to each rule a number saying how much the expert trusts it:

Definition — certainty factor

The certainty factor of a statement is a number CF ∈ [−1, 1] that expresses the degree of belief in the statement: CF = 1 certainly true, CF = −1 certainly false, CF = 0 unknown. It is not a probability — it is assigned by an expert.

Let two different rules support the same conclusion with factors CF₁, CF₂ ∈ (0, 1]. The resulting factor of the conclusion is

CF = CF₁ + CF₂ · (1 − CF₁).

For negative and mixed factors MYCIN has other combination formulas, which we do not need in this part.

In plain words

One clue convinces you to 0.6, a second, independent one to 0.5. Together 0.6 + 0.5 · 0.4 = 0.8 (colours as in the formula below) — the second clue takes away half of the remaining uncertainty. Certainty factors are not probabilities and do not satisfy Bayes’ theorem; they were later replaced by Bayesian networks, which have their own part in the syllabus.

CF = CF₁ + CF₂ · (1 − CF₁)

CF₁: the belief from the first rule; the second rule cannot lower it, only add to it
CF₂: what part of the remaining uncertainty the second rule removes; if we simply added, two clues of 0.6 each would give a nonsensical 1.2
1 − CF₁: the uncertainty left after the first rule; only that can still be reduced, which is why the result never exceeds 1

Equivalently 1 − CF = (1 − CF₁) · (1 − CF₂): the remaining uncertainties multiply. That is why the order of the rules does not matter.

Example — three clues and a rule with uncertain premises

Three clues 0.6, 0.5 and 0.5: first 0.6 + 0.5 · (1 − 0.6) = 0.8, then 0.8 + 0.5 · (1 − 0.8) = 0.9 (colours as in the formula above). Check via the uncertainties: 1 − 0.4 · 0.5 · 0.5 = 0.9.

Uncertain premises. In MYCIN (Shortliffe and Buchanan, 1975) a conjunction of premises gets the factor of its weakest link, and the conclusion of a rule gets the factor of the rule times this minimum factor (the rule is used only if the minimum exceeds 0.2): CF(conclusion) = CF(rule) · min_i CF(p_i). A rule with factor 0.7 whose premises have factors 0.9 and 0.6 thus contributes 0.7 · min(0.9, 0.6) = 0.42 to the conclusion.

By the end of the 1980s the limits had become clear. Knowledge acquisition was the bottleneck: experts often cannot put their know-how into words as rules, and every rule cost hours of interviews. The systems were brittle: one step outside their domain they knew nothing, and they did not even know that they knew nothing. And thousands of rules were hard to maintain — a new rule could silently contradict an old one. The market for expert systems collapsed and the second AI winter set in. The answer that came afterwards is the opposite: do not write knowledge down, learn it from data.

9. Knowledge in today’s artificial intelligence

Knowledge graphs. Since 2012 Google has answered many queries from its knowledge graph — a network of facts such as (Prague, capital, Czechia). The freely available Wikidata has more than a hundred million items. It is a knowledge base, only facts prevail over rules.
Rules where things must be checkable. Tax calculations, insurance terms, loan approval or security policies are still written as rules to this day: every decision can be explained and defended.
Language models and knowledge. A language model holds an enormous amount of knowledge, but spread across the weights of the network — it cannot be read or corrected piece by piece, and the model sometimes confidently makes things up. That is why it is connected to knowledge base retrieval (RAG) or to tools and inference engines that check the result.
Neurosymbolic AI combines both: the network recognises what it sees and logic derives what follows from it. Examples are systems that search for mathematical proofs: the model proposes a step and a formal tool checks it mechanically.

10. Summary

A knowledge base is a set of sentences; KB ⊨ α means that α holds in all models of the base. Model checking verifies this, but at the cost of 2ⁿ assignments.
Inference (⊢) works with sentences instead of worlds. We want it to be sound (it makes nothing up) and complete (it misses nothing).
For Horn clauses, forward chaining (from the facts, data-driven) or backward chaining (from the goal, driven by the question) is enough; forward chaining runs in linear time, backward chaining examines only what is relevant to the goal.
For all of propositional logic there is resolution and proof by contradiction; for rules with variables, unification and Prolog.
Expert systems showed both the power and the limits of hand-written knowledge — and prepared the ground for learning from data.

Want to get a feel for it? Have an AI agent write an expert system with backward chaining that asks about missing facts — and come up with your own rules for something you understand.

Do you see it differently? Write to support@coden-app.com.

Logic and knowledge systems: forward and backward chaining, resolution and expert systems

1. The knowledge base and the inference engine

2. Entailment and models

3. Inference: sound and complete

4. Forward chaining

5. Backward chaining

6. Resolution: inference for all of logic

7. Rules with variables and Prolog

8. Expert systems

9. Knowledge in today’s artificial intelligence

10. Summary

An Agent on your computer, driven from your phone