Automated Synthesis of a Finite Complexity Ordering for Saturation

Yannick Chevalier, Mounira Kourjieh

We present in this paper a new procedure to saturate a set of clauses with respect to a well-founded ordering on ground atoms such that A < B implies Var(A) {\subseteq} Var(B) for…