next up previous contents
Next: sair: Settings for Inference Up: Flag Settings Previous: saci: Settings for Constraint   Contents


saes: Settings for Eager Simplification


\begin{displaymath} \mbox{{\tt saes}} \end{displaymath}

The saes-flag specifies the list of simplification rules $S$ that are to be applied eagerly on each clause so as to ensure refutational completeness of a certain inference system. At present we have only one such inference, called ``variable elimination', and denoted by $S=1$, which should usually be turned on.

Variable elimination for orderings in Saturate is explained in (Bachmair & Ganzinger, 1994 a). Variable elimination also includes splitting of variable-disjoint parts of clauses or variable-disjoint sides of equations.


Harald Ganzinger 2002-12-04

Imprint | Data Protection