SELECTED STRATEGIES: -------------------- Some typical strategies are proposed together with their main characteristics. strategy_DCMA: triangulation, connected, static strategy_DCJqmgudynA: jump, connected, dynamic strategy_DCRqmgudynA: jump, non-connected, dynamic strategy_DCSRqmgustatA: quasi-division, non-connected, static strategy_DCSRtmgudynA: quasi-division, non-connected, dynamic TYPES of STRATEGIES: ------------------- 1-SIMPLIFICATION rules, other than taking repetitions or rational equality are obtained by: TRIANGULATION (close to TC from [Senizergues, TCS 2002]) computes an unifier and JUMP: the comp tree remains CONNECTED (uses TCJ in [HS, CIAA paper, 2013]) launch a new node that computes an unifier and JUMP: the comp tree is now a NON-CONNECTED forest (uses TCR in [HS, CIAA paper, 2013]) QUASI-DIVISION: this is a kind of n-dimensional transformation TB from [Hopcroft-Korenjac 1966]; see [HS, paper CIAA 2013]; this transformation launches a new node that computes an unifier; the comp tree is now a NON-CONNECTED forest. 2-UNIFIER computations: static: it means that the mgu's are guessed by a combinatorial exploration up to some depth (usually 10 or 20 for the below examples); their exactness is tested by the proof-construction; in case of incorrect guess, " failure" is returned. dynamic: it means that the mgu' s are guessed (the stupid guess: mgu:= Id can be used) by any means; their exactness is tested by the proof-construction; in case of incorrect guess, a witness of error is lifted from a leaf of the comp-forest to the root that stores the unifier; this witness is turned into a new dependency; the dependency is turned into an updating of the mgu, the rank of which decreases by one. When a witness of error is lifted up to the starting node of the comp-forest, a witness of error for the initial equation is returned. POSITIVE EXAMPLES: ----------------- ex0,ex1,ex2,ex3,ex4,ex5,ex6 (from the file WEB_pos_examples.py) (all strategies apply, in principle; but some strategies are too slow, see section 5 in CIAA-submission) NEGATIVE EXAMPLES: ----------------- ex2n,ex4n,ex4nn,ex4nnn,ex6n (from the file WEB_neg_examples.py) Only dynamical strategies can produce a witness of falsity; The static strategies just answer "failure".