CARINE performs an iteratively-deepening depth-first search (IDDFS) using a resolution refinement called semi-linear resolution (SLR). The delayed clause-construction strategy is implemented to allow CARINE to achieve a high inference-rate. Attribute sequences are used to reduce the search space and thereby, improve the efficiency of CARINE.
Benefits of IDDFS
At every iteration, clauses inferred from previous iterations are repeatedly inferred again. This implies that redundancies occur. However, the algorithm does ensure a systematic search process which uses storage space equivalent to a depth-first search (DFS). Its advantage over DFS is that the search is bounded by the iteration depth. This bounded search explores all paths up to the iteration depth leading to the discovery of the optimal proof length. This is a characteristic of a breadth-first search. Therefore, the benefits of IDDFS are low memory requirements, bounded search, and (theoretically) optimal proof lengths.
An attribute sequence is a sequence of length k (k>0) that is a projection of one or more search paths.
CARINE is written in ANSI-C for portability and speed. It has been tested under several operating systems and processors and it appears to be stable and consistent in its performance. It now runs under Microsoft Windows, Linux, SunOS, FreeBSD and Cygwin. The program is about 10,000 lines of code spread over 25 modules and header files.
CARINE does not generate any temporary files during the search and all output is directed to the standard output (which is usually the screen). No input file other than the theorem file is needed. The input file should be provided in a specific format. All settings of the control parameters should be provided at the command line.