Resolution Refutation Search Strategies
Ordering Strategies
Ordering strategies generates the resolvents for clauses in an orderly manner. Some of the ordering strategies include,
- Depth-first strategy.
- Breadth-first strategy.
- Unit-preference strategy.
The Depth-first strategy initially produce first level resolvent and then produce second level resolvent with first level clause and so on. This. process also involves backtracking strategy.
The Breadth-first strategy generates resolvents level wise, i.e., it produces all the first level resolvents and then all the second level resolvents and so on.
The unit preference strategy prefer unit clauses which consist of a single literal.
Refinement Strategies
Set of Support: If α2 is resolved from a, or from descendent of α1 then α2 is said to be descendant of α1. Set of support is a set of clauses resolved from negation of theorem to be proved or descendants of those clauses. This strategy only allows resolutions in which one of them from set of support. ,
Linear Input: This strategy only allows the resolutions in which one of them from original set of clauses. The set of support strategy is refutation complete, where as linear input strategy is not refutation complete. It. can be shown by considering the following set of clauses which are inconsistent.
{P ∨ R, P ∨ ᆨR, ᆨP ∨ R, P ∨ R}
The above clauses have a resolution refutation, because they don't have model.
Ancestry Filtering: This strategy only allows the resolutions which one of them is either from original set or ancestor of other resolvents. This strategy is refutation complete.
Horn Clauses
In logic, a Horn clause is a clause (a disjunction of literals) with at most one positive literal. A Horn clause with exactly one positive literal is a definite clause; a Horn clause with no positive literals is sometimes called a goal clause especially in logic programming. A Horn formula is a conjunctive normal form formula whose clauses are all Horn; in other words, it is conjunction of Horn clauses. A dual-Horn clause is a clause with at most one negative literal. Horn clauses play a basic role in logic programming and are important for constructive logic.
The following is an example of a (definite),Horn clause,
ᆨp ∨ ᆨq ∨ .... ∨ ᆨt ∨ u
Such a formula can be rewritten in the following form, which is more common in logic programming and similar fields,
(p ∧ q ∧..... ∧ t) → u
The relevance of Horn clauses to theorem proving by first order resolution is that the resolution of two Horn clauses is a Horn clause. Moreover, the resolution of a goal clause and a definite clause is again a goal clause. In automated theorem proving, this can lead to greater efficiencies in proving a theorem (represented as a goal clause). In fact, Prolog is a programming language based on Horn clauses.
Horn clauses are also of interest in computational complexity, where the problem of finding a set of variable assignments to make a conjunction of Horn clauses true is a P-complete problem, sometimes called HORNSAT. This is P's version of the Boolean satisfiability problem, a central NP-complete problem.
