Semi-linear resolution

From Wikipedia, the free encyclopedia

 This article does not cite any references or sources. (January 2007)
Please help improve this article by adding citations to reliable sources. Unverifiable material may be challenged and removed.

Semi-Linear Resolution (SLR) is a search strategy (used in the automated theorem prover (ATP) CARINE) that is based on an iteratively-deepening depth-first search. It is one method used in automated theorem proving.

SLR performs linear derivations from the input clauses and a maintained set-of-support to obtain subgoals (usually unit clauses), such that the length of each derivation is no more than an assigned depth bound.

[edit] See also

Comp Sci logo This computer science-related article is a stub. You can help Wikipedia by expanding it.