incOSHL

incOSHL is an implementation of an incremental version of the OSHL algorithm.

Compiling and Linking the Source Code

All source code of incOSHL is located in one directory. To compile to the source code, go to the directory contain the source code and run the following command:

g++ -O3 -o incOSHL *. cpp

The g++ version used for development is 4.6.3. And the g++ version used for testing is 4.1.2. Other version of g++ may also work, but they are not tested.

Running the Prover

To run incOSHL, use the following command:

incOSHL <file_path> <options>

<file_path> is a relative path to the tptp path, which can be specified in <options>. <options> is a comma separated list of key value pairs of the form <key>=<value>. Most supported keys include both a long form and a short form. The supported keys are given in the following table.

Key Long Form	SF	Value Type	Usage
timeout	to	integer	This key sets the cpu clock time limit for the main loop. The prover periodically checks if the cpu time has exceeded this limit and stops the proof search. In some cases, the periodic check may not occur around the time limit, resulting a longer running time. The "timeout" command from coreutils can be used to solve this problem.
useSuperSymbol	uss	boolean	This key sets whether the prover creates supersymbols during the preprocessing phase. When enabled, it replaces multiple consecutive symbols in a flatterm with a supersymbol, which provides minor efficiency improvement on some problems.
sortSubtreesBySize	ssbs	boolean	This key sets whether the prover sorts the subtrees of every clause tree node by the size of the minimum clause instance that can be generated from those subtrees, in ascending order of the minimum clause instance size of a subtree, a value computed during preprocessing. When enabled, it allows the prover to stop looking further at other subtrees when the minimum clause instance size of a subtree is larger than the current term size limit.
stacksize	ss	integer (megabytes)	This key sets the memory size limit for the prover. The prover generates a "max memory" error if the memory usage is greater than this size plus a small constant (non-growing) memory footprint. In some case, memory leak causes the prover go over this memory usage limit.
flipLiteral	fl	boolean	This key sets whether the sign of the literals should be flipped.
randomFlipLiteral	rfl	boolean	This key sets whether the prover randomly chooses a subset of predicates and randomly flips the signs of all the literals with predicates in that set.
randomLexicalOrder	rlo	boolean	This key sets whether the prover randomly assigns the lexical order of symbols, as opposed to the order they appear in the input file.
randomClauseInsert	rci	boolean	This key sets whether the prover randomly assigns the order in which the input clauses are inserted into the clause tree, as opposed to the order they appear in the input file.
randomClauseLiteral	rcl	boolean	This key sets whether the prover randomly assigns the order in which literals appear in an input clause when the clause is inserted into the clause tree, as opposed to the order they appear in that clause in the input file.
tptppath	tp	string (with quotes)	This key sets the tptp path.

##Prover Output

The prover generates on of the following outputs:

output
time out	The prover timed out without finding a proof.
max memory	The prover reached the memory limit without finding a proof.
max term size	The prover reached the maximum term size without finding a proof.
proof found	The prover found a proof.
saturated	The prover found a model.

User Manual

For more information see the user manual.