Howto sub-term criteria
Sub-term criterion is cheap to check and powerful. To use it in this
version of CiME 3, you need the following criteria:
- DP or DPM in order to switch to the dependency
- SCC in order to consider dependency graphs
- ST or subterm in order to try the sub-term criterion.
The usual proof heuristic is as
Then [ Use DPM ; Repeat Then [Use SCC ; Use ST] ]
that is use 1 and repeat the sequence 2,3 on all generated
This heuristic is for sub-term used alone but of course you
may use it in conjunction with other criteria (and orderings):
let h = heuristic
"Then [Use DPM; Repeat Then [ Use SCC; Solve[Use ST;Use RMVx;Then [ DPSG; SolveOrd ]] ] ]";
The current ST implementation requires a SAT solver (the given
example is minisat2) and the following settings:
#Set_sat_solver "minisat2"; subtermparams 0;
Heuristic subterm is to be deprecated shortly and does not require
any SAT solver.
You may then define your heuristic.
Generation of xml files is as usual, as well as their Coq certification.