Semi-linear resolution
From Wikipedia, the free encyclopedia
 |
This article does not cite any references or sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. (January 2007) |
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
 |
This formal methods-related article is a stub. You can help Wikipedia by expanding it. |
