CARINE: Автоматический доказыватель теорем первого порядка с использованием стратегий DCC и ATS.

CARINE (Computer Aided Reasoning Engine) is a first order classical logic automated theorem prover. It was 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)) and used in theorem provers like THEO. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space.

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. DCC is useful when too many intermediate clauses (especially first order clauses) are being constructed and discarded in a short period of time because the operations performed to construct such short lived clauses are avoided. DCC may not be very effective on theorems with only propositional clauses.

After every application of an inference rule, certain variables may have to be substituted by terms (e. g. x → f(a)) and thus a substitution set is formed. Instead of constructing the resulting clause and discarding the substitution set, the theorem prover simply maintains the substitution set along with some other information, like what clauses where involved in the inference rule and what inference rule was applied, and continues the derivation without constructing the resulting clause of the inference rule. This procedure keeps going along a derivation until the theorem provers reaches a point where it decides, based on certain criteria and heuristics, whether to construct the final clause in the derivation (and probably some other clause(s) along the path) or discard the whole derivation i. e., deletes from memory the maintained substitution sets and whatever information stored with them.