First-Order Resolution and Theorem Proving

Propositional resolution manipulates fixed atoms. First-order resolution must also decide which terms can denote the same objects for an inference step, and how existential witnesses depend on universally quantified variables. FIT3080’s second logic lecture develops substitution, unification, clause conversion, resolution, and a worked theorem-proving example; this note follows that route and makes its correctness conditions explicit [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5..

Read Formal Logic and Natural Deduction for syntax and quantifiers, and Propositional Automated Reasoning for clauses and refutation. Unless stated otherwise, the resolution calculus here is for classical first-order logic without built-in equality, over nonempty domains and ordinary finite terms. Equality requires additional treatment later in the note.

Substitution: replace variables consistently

A substitution is a finite map from variables to terms. Write $\theta=\{x\mapsto a,y\mapsto f(z)\}$ and $E\theta$ for its application to expression $E$. All free occurrences of the same variable receive the same term, with capture avoided under quantifiers.

Substitution is simultaneous. With $\theta=\{x\mapsto y,y\mapsto a\}$,

$$R(x,y)\theta=R(y,a),$$

not $R(a,a)$. The replacement inserted for $x$ is not recursively reprocessed by that same substitution. Composition is a separate operation. Define $E(\theta\sigma)=(E\theta)\sigma$; for $\theta=\{x\mapsto y\}$ and $\sigma=\{y\mapsto a\}$, $x(\theta\sigma)=a$, whereas $x(\sigma\theta)=y$. Composition order therefore matters.

Before resolving two clauses, standardize their variables apart. The universal variable $x$ in one clause is not a shared free parameter with an $x$ written in another. Rename the second clause’s variables freshly before combining them; this prevents accidental identifications that can block legitimate inferences.

Unification and most general unifiers

A unifier $\theta$ makes two expressions syntactically identical after substitution. A most general unifier, or MGU, imposes no unnecessary additional commitments: every other unifier is an instance of it, on the variables of the problem.

ExampleSolve the term equations

Unify $R(x,f(y))$ with $R(g(a),f(b))$. The predicate and arity match, leaving equations $x=g(a)$ and $f(y)=f(b)$. Decompose the latter to obtain $y=b$. Thus an MGU is

$$\theta=\{x\mapsto g(a),\ y\mapsto b\}.$$

Both expressions become $R(g(a),f(b))$. In contrast, $R(x,x)$ and $R(a,b)$ do not unify when $a,b$ are distinct constant symbols: the same variable would have to receive two different syntactic terms. This is about syntactic matching, not an assumption that distinct names must denote different objects in every interpretation.

A practical unifier maintains pending term equations and a substitution. Its core operations are:

1. Delete an equation whose sides are already identical.
2. Decompose matching function symbols with matching arities into equations between their arguments.
3. Orient a variable equation as $x=t$. If $x$ does not occur in $t$, replace $x$ by $t$ throughout the remaining equations and previously recorded replacement terms.
4. Fail on mismatched function symbols or arities, or when the occurs check fails.

The occurs check rejects $x=f(x)$: no finite term equals a proper term containing itself. Some programming systems support cyclic terms by using different term semantics; that is not the unification problem defined here. For finite first-order terms, the standard unification algorithm terminates with an MGU or failure.

ExampleOne binding can force another

The equations $x=f(y)$ and $y=a$ first give a provisional binding for $x$, then refine it when $y$ is solved. The resulting substitution is $\{x\mapsto f(a),y\mapsto a\}$. Recording the two bindings without propagating the second into the first would not produce this normalized simultaneous substitution.

From a quantified formula to clauses

To prove $K\models q$, refute $K\land\neg q$. For a finite first-order knowledge base and sentence query, the preprocessing pipeline is:

1. Eliminate $\to$ and $\leftrightarrow$.
2. Move negations to atoms, using the quantifier negation laws.
3. Rename bound variables so separate quantifiers use separate names.
4. Move quantifiers to a prenex prefix, observing free-variable restrictions.
5. Remove existential quantifiers by introducing fresh Skolem symbols with the correct universal dependencies.
6. Convert the remaining matrix to CNF.
7. Treat remaining variables as universally quantified, split the conjunction into clauses, and standardize variables apart between clauses.

Steps involving Skolemization preserve satisfiability in an expanded signature, not literal equivalence in the original signature. “Drop the universal quantifiers” is a notation convention for clauses; it does not turn universal variables into arbitrary constants or existential variables. Direct CNF distribution can still be expensive, so this simple pipeline is a teaching procedure rather than an optimized implementation.

Skolem functions record witness dependence

Compare

$$\forall x\exists y\,R(x,y) \qquad\text{and}\qquad \exists y\forall x\,R(x,y).$$

For the first, introduce a fresh function $f$ and use $\forall x\,R(x,f(x))$: the witness may depend on $x$. For the second, introduce a fresh constant $c$ and use $\forall x\,R(x,c)$: one witness must serve every $x$. Replacing $f(x)$ by a constant in the first formula would impose a stronger requirement than the original.

Why is satisfiability preserved? A model of the Skolemized formula supplies witnesses through the new function or constant; forgetting that new symbol leaves a model of the original sentence. Conversely, a model of the original can be expanded by selecting suitable witnesses as interpretations of the fresh symbols, using the usual background assumptions of model theory. Existing symbols cannot be reused indiscriminately, because that could impose relations between witnesses which the original formula never required.

ExampleDependencies survive clause splitting

Consider

$$\forall x\exists y\, \bigl(R(x,y)\land\neg S(x,y)\bigr).$$

After Skolemization the clauses can be written

$$\{R(x_1,f(x_1)),\quad\neg S(x_2,f(x_2))\}.$$

The clause variables have been renamed apart, but the Skolem function remains the same $f$. Renaming it independently in each clause would lose the requirement that the same witness satisfy both conditions for each input.

First-order resolution

Let $C\lor L$ and $D\lor\neg M$ be clauses with variables standardized apart, where the atoms $L,M$ have MGU $\theta$. Binary resolution derives

$$\frac{C\lor L\qquad D\lor\neg M} {(C\lor D)\theta}.$$

The substitution applies to the entire remaining resolvent, not only the selected literals. The rule is sound because universally quantified parent clauses permit the substituted instances, and propositional resolution is sound on those instances.

ExampleLift a ground inference to variables

Resolve $\neg P(x)\lor Q(x)$ with $P(f(a))$. The selected atoms unify under $\{x\mapsto f(a)\}$, yielding $Q(f(a))$. Deriving $Q(x)$ with an uninstantiated universal $x$ would be an unjustified strengthening.

For a standard complete first-order resolution calculus, binary resolution is accompanied by factoring. If same-sign literals in a clause unify, apply their MGU to the whole clause and merge them. For example, $P(x)\lor P(y)$ factors to $P(x)$ under $\{y\mapsto x\}$. Factoring is more than deleting already identical literals; it can create a useful instance by unifying them. The usual refutation-completeness result assumes the full calculus and suitable fair search, not just arbitrary binary steps.

Factoring is sound because a universally quantified clause entails every substitution instance; after the unifier is applied, repeated identical literals have the same truth value as a single copy. The general first-order refutation-completeness theorem still requires Herbrand’s theorem and the lifting lemma, neither proved here. The worked refutation below does not establish that metatheorem.

A complete proof with an existential query

ExampleFrom a supplier rule to the existence of a certified item

Use a signature with constant $a$, unary predicate $A$, binary predicate $R$, and unary predicate $C$. The premises are

$$A(a),$$$$\forall x\bigl(A(x)\to \exists y\,(R(x,y)\land C(y))\bigr).$$

Think of $A(x)$ as “$x$ is an approved supplier,” $R(x,y)$ as “$x$ supplies $y$,” and $C(y)$ as “$y$ is certified.” The goal is $\exists z\,C(z)$.

In the rule, eliminate the implication and move the existential quantifier outward through the disjunction, which is allowed because $y$ is not free in $A(x)$. Introduce a fresh Skolem function $f(x)$. Split the resulting CNF into two clauses, retaining the same $f$. Negate the goal to get $\forall z\,\neg C(z)$.

Clause	Formula	Source
1	$A(a)$	Fact
2	$\neg A(x_1)\lor R(x_1,f(x_1))$	Skolemized rule
3	$\neg A(x_2)\lor C(f(x_2))$	Skolemized rule
4	$\neg C(z)$	Negated goal
5	$C(f(a))$	Resolve 1 and 3, $x_2\mapsto a$
6	$\square$	Resolve 4 and 5, $z\mapsto f(a)$

The empty clause refutes the negated query, proving that a certified object exists. Its name in the extended language is $f(a)$, but the original theory did not name a particular object. Clause 2 is valid input but unnecessary for this query; a search strategy need not use every available premise.

Search strategy and the limits of termination

A finite propositional vocabulary yields finitely many different clauses. First-order function symbols can instead produce unbounded terms such as $a,f(a),f(f(a)),\ldots$. A search that derives more and more clauses may therefore never saturate.

Classical first-order validity is semidecidable: a complete, fairly organized proof search eventually finds a proof when the sentence is valid, but need not terminate when it is invalid. Correspondingly, resolution can eventually refute an unsatisfiable clause set under the completeness assumptions, while a satisfiable input may run forever. Soundness and completeness do not imply a decision procedure for every first-order input [2][2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf.

FIT3080 introduces several ways of guiding resolution. Their restrictions must be stated precisely:

Technique	Purpose and qualification
Unit preference	Try short/unit parents early; preference should not starve required inferences
Unit resolution	Require a unit parent in every step; this restriction is not complete for arbitrary clause sets
Set of support	Require a parent from the support set or its descendants; the usual completeness guarantee requires the clauses outside that set to be satisfiable
Input resolution	Require an original input clause as a parent; not complete for general clause sets
Subsumption	Remove a clause made redundant by a more general retained clause; finding such a match itself takes work

For example, $P(x)$ subsumes $P(a)\lor Q(a)$ because an instance of the first clause is a subset of the second. Preserve proof provenance when deleting redundant clauses. Setting the negated goal as the initial support is useful when the remaining knowledge base is satisfiable; if it is already inconsistent, that justification no longer applies automatically.

Equality, logic programming, and SMT

If equality is built into the logic, ordinary predicate resolution alone does not capture all its properties. One needs equality axioms or specialized rules such as paramodulation or superposition. For example, $a=b$ and $P(a)$ entail $P(b)$ under identity semantics, but treating equality as an unrelated predicate would miss the connection.

Definite first-order clauses also lead to logic programming and SLD resolution. A procedure may be sound yet loop because it repeatedly chooses the same recursive branch; ordinary depth-first Prolog search does not inherit a blanket termination or completeness guarantee. Function-free finite-domain settings offer stronger termination properties, but those restrictions must be explicit.

SMT extends propositional search with reasoning in specified theories, such as linear arithmetic, equality with uninterpreted functions, or arrays. It is not a universal solution to first-order logic. The supported theory fragment determines guarantees; quantified or difficult inputs may produce an unknown result. These topics extend the course’s introductory path, rather than being prerequisites for the examples above [3][3] C. Trippel and H. Lachnitt, “CS 257: Introduction to Automated Reasoning,” 2026. Winter 2026 course: propositional reasoning, first-order resolution and unification, and satisfiability modulo theories. https://web.stanford.edu/class/cs257/.

What to preserve in a proof certificate

For each derived clause, record its parent identifiers, the renamed variables, the resolved or factored literals, and the substitution. A checker verifies that the substitution actually unifies the selected expressions and that the resulting clause is correct. It should also validate the preprocessing steps, including freshness and dependence of Skolem symbols; a flawless refutation of the wrong encoding does not prove the original claim.

Return a checked refutation when one is found. If a model is reported, verify it against the original sentences. A time or resource limit should yield “unknown,” not “false.” This is the smallest useful distinction between a demonstration of proof search and an accountable theorem-proving pipeline.

Exercises

ExerciseCompute an MGU

Unify $R(x,f(x))$ with $R(g(y),f(g(a)))$. State an MGU and verify both substituted expressions.

Show solution

Solution

The argument equations give $x=g(y)$ and $x=g(a)$, hence $y=a$. An MGU is $\{y\mapsto a,x\mapsto g(a)\}$. Both atoms become $R(g(a),f(g(a)))$.

ExerciseKeep witness dependencies

Skolemize $\forall x\exists y\forall z\exists w\,T(x,y,z,w)$. Which arguments do the new functions need in the standard construction?

Show solution

Solution

Use fresh functions $f,g$ to obtain $\forall x\forall z\,T(x,f(x),z,g(x,z))$. The witness for $y$ depends on preceding universal $x$; the witness for $w$ may depend on preceding universals $x,z$. The earlier witness $y$ has already been represented by $f(x)$, so no separate existential argument is needed.

ExerciseCatch a missing substitution

Someone resolves $\neg R(x,y)\lor S(y)$ with $R(a,f(a))$ and writes $S(y)$. Repair the step.

Show solution

Solution

The MGU is $\{x\mapsto a,y\mapsto f(a)\}$. It applies to the remaining literal too, giving $S(f(a))$. Leaving $y$ universally quantified would claim the predicate holds of every object.

ExerciseInterpret an unfinished run

An unrestricted first-order prover keeps generating terms without finding a contradiction. Does completeness imply that it must eventually report a satisfying model?

Show solution

Solution

No. Refutation completeness guarantees eventual discovery of a refutation for unsatisfiable input under fair search. It does not guarantee termination or model production for satisfiable input. Without an independently checked model or a suitable complete decision procedure for the fragment, the result remains unknown.

CounterexampleWhy unit and input resolution are incomplete

The four clauses $P\lor Q$, $P\lor\neg Q$, $\neg P\lor Q$, $\neg P\lor\neg Q$ are jointly unsatisfiable: every assignment falsifies one of them. Unit resolution cannot start, since none is a unit. Input resolution may derive units, but a final binary step deriving the empty clause must have two complementary unit parents. Neither can be an original input clause, so that final step is forbidden. Unrestricted resolution derives $P$ from the first pair, $\neg P$ from the second pair, and then the empty clause.

References

1. [1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5. ↩
2. [2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf ↩
3. [3] C. Trippel and H. Lachnitt, “CS 257: Introduction to Automated Reasoning,” 2026. Winter 2026 course: propositional reasoning, first-order resolution and unification, and satisfiability modulo theories. https://web.stanford.edu/class/cs257/ ↩