Semi-Linear Resolution (SLR) is a search strategy (used in the automated theorem prover 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.
| Property | Value |
|---|
| dbpprop:abstract
|
- Semi-Linear Resolution (SLR) is a search strategy (used in the automated theorem prover 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.
|
| dbpprop:hasPhotoCollection
| |
| rdf:type
| |
| rdfs:comment
|
- Semi-Linear Resolution (SLR) is a search strategy (used in the automated theorem prover 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.
|
| rdfs:label
| |
| owl:sameAs
| |
| skos:subject
| |
| foaf:page
| |
| is dbpprop:redirect
of | |
| is owl:sameAs
of | |
![[RDF Data]](/statics/sw-cube.png)
