CARINE

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

CARINE (Computer Aided Reasoning engINE) 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 [Haroun 2005]. 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]) and used in theorem provers like THEO [Newborn 2001]. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space.

Delayed Clause Construction (DCC)

Delayed Clause Construction is a stalling strategy that enhances a theorem prover's performance by reducing the work to construct clauses to a minimum. Instead of constructing every conclusion (clause) of an applied inference rule, the information to construct such clause is temporarily stored until the theorem prover decides to either discard the clause or construct it. If the theorem prover decides to keep the clause, it will be constructed and stored in memory, otherwise the information to construct the clause is erased. Storing the information from which an inferred clause can be constructed require almost no additional CPU operations. However, constructing a clause may consume a lot of time. Some theorem provers spend 30%-40% of their total execution time constructing and deleting clauses. With DCC this wasted time can be salvaged.