Carine theorem prover

CARINE is a first-order classical logic automated theorem prover.

CARINE performs an iteratively-deepening depth first search. Its main search strategy is semi-linear resolution (SLR). It employs delayed clause-construction (DCC) to achieve a high inference rate, and attribute sequences to reduce its search space.

External links

• [1]CARINE original site
• [2]CARINE new site