next up previous contents
Next: Selecting the Inference System Up: The Interaction Cycle Previous: The Interaction Cycle   Contents

Reading Clauses

The commands in or add read files containing clauses and meta-logical directives. We support structured theories, the separation between logical and meta-logical items and the use of pre-saturated theory modules. The clauses in the database can have different origins. The command l displays the current saturation status of the current theory.



Harald Ganzinger 2002-12-04

Imprint | Data Protection