Semi-linear resolution
Encyclopedia
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.
Carine theorem prover
CARINE is a first-order classical logic automated theorem prover.CARINE is a resolution based theorem prover initially built for the study of the enhancement effects of the strategies delayed clause-construction and attribute sequences in a depth-first search based algorithm [Haroun 2005]...
) that is based on an iteratively-deepening depth-first search. It is one method used in automated theorem proving
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
.
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.