A3PAT

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:
  1. DP or DPM in order to switch to the dependency pairs approach,
  2. SCC in order to consider dependency graphs
  3. ST or subterm in order to try the sub-term criterion.


The usual proof heuristic is as follows:
Then [ Use DPM ; Repeat Then [Use SCC ; Use ST] ]
that is use 1 and repeat the sequence 2,3 on all generated sub-problems. This heuristic is for sub-term used alone but of course you may use it in conjunction with other criteria (and orderings):
#Set_sat_solver "minisat2";
let h = heuristic
"Then [Use DPM; Repeat Then [ Use SCC; Solve[Use ST;Use RMVx;Then [ DPSG; SolveOrd ]] ] ]";
set_heuristic "h";

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.

Tools a3pat