Next: Saving (partially) saturated set
Up: The Interaction Cycle
Previous: Selecting timing points
Contents
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