CARINE

From Wikipedia, the free encyclopedia

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 (DCC) and attribute sequences (ATS) in a depth-first search based algorithm. CARINE's main search algorithm is semi-linear resolution (SLR) which is based on an iteratively-deepening depth-first search (also known as depth-first iterative-deepening (DFID) [Korf 1985]). SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space.

[edit] References

[Korf 1985] Korf, Richard E., "Depth-First Iterative -Deepening: An Optimal Admissible Tree Search", Artificial Intelligence, vol. 27, (pp. 97-109), 1985.

[edit] External links

\lnot(p\land\lnot p)  This logic-related article is a stub. You can help by expanding it.
Comp Sci logo This computer science-related article is a stub. You can help Wikipedia by expanding it.