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.
[1] 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))[2] and used in theorem provers like THEO.
[3] 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.
Storing the information from which an inferred clause can be constructed require almost no additional CPU operations.
Some theorem provers spend 30%–40% of their total execution time constructing and deleting clauses.
DCC may not be very effective on theorems with only propositional clauses.
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.
(An informal definition of) a clause in theorem proving is a statement that can result in a true or false answer depending on the evaluation of its literals.
The above example states that if Y is wealthy AND smart AND beautiful then X loves Y.
Note that the above representation comes from the logical statement: For all Y, X belonging to the domain of human beings:
By using some transformation rules of formal logic we produce the disjunction of literals of the example given above.
has: An attribute sequence is a sequence of k n-tuples of clause attributes that represent a projection of a set of derivations of length k. k and n are strictly positive integers.
The set of derivations form the domain and the attribute sequences form the codomain of the mapping between derivations and attribute sequences.
Note: An n-tuple of clause attributes is similar (but not the same) to the feature vector named by Stephan Schulz, PhD (see E equational theorem prover).