next up previous contents
Next: Saving (partially) saturated set Up: The Interaction Cycle Previous: Selecting timing points   Contents

Saturating a system

The command sat saturates the current data base. When the saturation is finished, the the final set of axioms is displayed, together with the proof, if the empty clause was generated. Saturation can be forced to terminate with a partially saturated system by providing an upper bound on clause generation.



Harald Ganzinger 2002-12-04

Imprint | Data Protection