Resolution, step by step

Resolution without matching

The core abstract syntax of the resolution system:

Clause  ::= Goal :- Goal1, ..., Goaln      (n ≥ 0)
Program ::= Clause1 ... Clausek            (k > 0)

A list of goals is called a resolvent. A clause has the form head :- body; clauses with an empty body are called facts (G.), and clauses with a non-empty body are called rules (G :- G1,..,Gn.).

Semantics: the transition relation

Start with an initial input resolvent R0 = G1, G2, ..., Gn. A valid computation step (resolution) is a transition R → R', defined as follows: if the clause G' :- G1', ..., Gm' is defined in the program, and G' = G1, then

G1, G2, ..., Gn  →  G1', ..., Gm', G2, ..., Gn

Note that, given an R, there can be many R'.

For example, with the clauses a. and a :- b, c., and the resolvent a, c, d, there are only two valid resolutions in one step:

• a, c, d → c, d: here the list of goals was reduced;
• a, c, d → b, c, c, d: here the list of goals was expanded.

Resolution trees

For each resolvent, its first goal can match the head of many clauses (always considered from top to bottom), hence several child resolvents could be generated. A resolution is successful if there is a leaf with an empty resolvent. Generally we have a (potentially unbounded) tree of resolvents, where solutions are searched left to right (depth first). The process of bringing exploration back up in the tree to find a (new) solution is called backtracking.

An example program, and its resolution trees

File resolution-trees.pl: facts, rules and recursion. Everything here is propositional: every goal is a 0-ary predicate.

Here are the resolution trees of a, b, c and d:

a          b                    c                       d
.          ├── .                ├── .                   d
           ├── .                ├── a,c                 └── d
           └── z                │   ├── c                   └── ...
                                │   │   └── ...
                                │   └── ...
                                └── b
                                    ├── .
                                    ├── .
                                    └── z

(. stands for the empty resolvent, a success.) This program is meant to misbehave, to show exactly that:

• a succeeds once.
• b answers twice (the two facts), and then the third clause raises Unknown procedure: z/0, since z is not defined at all (a Prolog system with the closed-world assumption would simply fail; SWI-Prolog complains about the undefined predicate).
• c has infinitely many solutions (we asked for 4): the clause c :- a, c. regenerates c over and over.
• d does not terminate: d :- d. only ever replaces d by d. The notebook stops it after a bounded number of steps.

Outcomes of resolution: what can we ask?

• Predicative: can we find at least one solution (reaching an empty leaf)? We do not care after the first one.
• Stream-like: how many solutions?
• Loop-aware: will the computation terminate? (Seemingly undecidable.)
• Output-oriented: what is the output of a solution? Is it related to the sequence of resolvents? What is the order of results?

Inference and knowledge with resolution

File inference-rules.pl.

Facts, though atomic, can be used to state knowledge we take as true, e.g. an axiom, similarly to propositional symbols in propositional logic.

A rule: by a resolvent, we check a composition of goals as a sort of higher-level knowledge. A rule is a way of giving such a composition a name (the head) and a definition (the body). Essentially: name-based abstraction, with the key possibility of recursion.

Shortcomings

Propositional resolution is not enough:

• goals might have a structure, not just be atomic symbols;
• goals seem to express a relationship between elements;
• we might want to express the grandfather relation in the general case;
• we might want an explicit notion of result (who is Abraham's father?);
• we need to express computations in a Turing-complete way.

Roadmap

• give a concrete, structured syntax to goals;
• provide an advanced mechanism of goal-rule matching (unification);
• add information to the status of computation beyond mere resolvents (the substitution).

This extends resolution analogously to the transition from propositional logic to first-order logic.

Resolution with unification: the core semantics

Use a tree of pairs ⟨resolvent : substitution⟩ as computation state. Start with an initial configuration C = ⟨R0 : {}⟩. A valid computation step is a transition C → C', defined as follows: if G' :- G1', ..., Gm' is a clone (a renamed copy) of a clause in the program, and θ' = mgu(G', G1) exists, then

⟨G1, G2, ..., Gn : θ⟩  →  ⟨(G1', ..., Gm', G2, ..., Gn)θ' : θθ'⟩

For simplicity, only the part of θ that mentions variables of the resolvent and of the input resolvent is needed. The transition relation induces, as usual, a possibly infinite tree. A solution is the substitution θ we have in a leaf with an empty resolvent.

File grandfather.pl:

Example 1

C1:  father(terach, X) : {}
-->
C2:  yes : {X/abraham}

The cloned fact father(terach, abraham). matches the goal with θ' = {X/abraham}, and the new resolvent is empty (yes).

Example 2

C1:  father(terach, X), father(X, Y) : {}
-->
C2:  father(abraham, Y) : {X/abraham}

The cloned fact father(terach, abraham). matches with θ' = {X/abraham}; the new resolvent is father(X, Y), which after applying θ' becomes father(abraham, Y). Here θ' must be preserved, since X is used in the goal.

Example 3

C1:  grandfather(terach, X) : {}
-->
C2:  father(terach, F'), father(F', X) : {}

The cloned rule is grandfather(GF', GS') :- father(GF', F'), father(F', GS'). with θ' = {GF'/terach, GS'/X}. The new resolvent is father(GF', F'), father(F', GS'), and after applying θ' it is father(terach, F'), father(F', X). No part of θ' must be recalled for subsequent steps: the bindings concern only the fresh variables of the clone.