5 Resolution in Predicate Logic

What is factoring in resolution?

A technique to unify two literals in the same clause and apply the most general unifier (mgu) to the whole clause.

Why is factoring sometimes necessary?

Some resolutions require factoring first to eliminate redundancy or reach a contradiction.

Give an example of when factoring is necessary.

To resolve {P(x), P(y)} and {¬P(u),¬P(v)}, factoring gives {P(x)} and {¬P(u)}, which can resolve to ⊥.

What is the general resolution method?

Iteratively apply resolution and factoring to clauses in Σ until ⊥ is derived.

Does resolution always terminate?

It may not terminate for satisfiable formulas; for unsatisfiable ones, it terminates with a good strategy.

What is refutation completeness?

If ⊥ is derivable from Σ, resolution will find it with a fair strategy.

Why is variable renaming necessary in resolution?

To prevent variable collisions and ensure correct unification.

What is a Horn clause?

A clause with at most one positive literal.

How is a Horn clause expressed as an implication?

(¬P ∨ ¬Q ∨ R) is written as (P ∧ Q) → R.

Why are Horn clauses important in Prolog?

They simplify inference and match Prolog's rule format.

What is the satisfiability checking algorithm for Horn formulas?

Mark ⊤; repeatedly mark Q if all premises of a clause P1 ∧ … ∧ Pn → Q are marked. If ⊥ is marked, it's unsatisfiable.

What makes satisfiability of propositional Horn formulas efficient?

It can be checked in linear time.

What is equality in automated reasoning?

A special predicate 'eq(x, y)' with axioms: reflexivity, symmetry, transitivity, and congruence.

List the axioms for equality.

x = x (reflexivity); x = y → y = x (symmetry); x = y ∧ y = z → x = z (transitivity); x = y → f(x) = f(y) and P(x) → P(y) (congruence).

Why is axiomatized equality inefficient in resolution?

It causes exponential growth due to repeated clause instantiations.

What is automated reasoning?

A field of AI using computers to perform logical inference.

What is the main question of automated theorem proving?

Given axioms A1, …, An and conjecture C, does A1, …, An ⊨ C?

What is the Robbins Conjecture?

A long-standing open algebra problem solved by a computer (McCune, 1996).

What are applications of automated reasoning?

Program verification, protocol validation, mathematical proofs.

What is refutation completeness vs completeness?

Refutation completeness means we can derive ⊥ if a contradiction exists; completeness ensures all logical consequences are derivable.

What does it mean that predicate logic is semi-decidable?

We can verify unsatisfiability (prove ⊥) but not guarantee termination for satisfiable formulas.

How is reasoning enhanced in restricted logics?

Restrictions like Horn clauses or adding types make automated reasoning more efficient.

What is the role of ordering in resolution strategies?

It prioritizes clause selection to avoid infinite loops and improve termination.

What are future extensions of resolution mentioned?

Ordered resolution, equality handling, higher-order logic, typed logic.

How is logic used in program synthesis and verification?

To prove that programs meet specifications or infer program components.