Logic for Computer Scientists/Predicate Logic/Strategies for Resolution/Input and Unit Resolution

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Predicate Logic‎ | Strategies for Resolution
Jump to: navigation, search

Input and Unit Resolution[edit]

Definition 26[edit]

Given a set of clauses S. The inference rule input resolution is resolution, such that one parent clause is a clause from S. The inference rule unit resolution is resolution, such that at least one parent clause is a unit clause or a unit factor of a parent clause.

In an obvious way the notions of unit (input) derivations and refutations are defined.

Theorem 10[edit]

For a set S of clauses there exists a unit refutation iff there exists an input refutation. Unit resolution (and hence input resolution) is not complete for full first order logics!

For Horn clauses, however, it is a complete strategy and indeed, it is the basis for the SLD-resolution principle, which is the core of SLD-Resolution