Contents

• Installation
  • Copying the System
  • Installing the System
  
  
• Overview
  • Applications
  • Inference System
  • Redundancy
  • Associative-Commutative Operators
  
  
• Getting started
• Formula Syntax
• The Interaction Cycle
  • Reading Clauses
  • Selecting the Inference System
  • Selecting Ordering and Selection Function
  • Selecting the redundancy proof techniques
  • Selecting the output information
  • Selecting timing points
  • Saturating a system
  • Saving (partially) saturated set
  • Proof Printing
  
  
• Saturate Commands
  • add: Adding Input
  • cd
  • cl: Clearing the Database
  • Flag Settings
  • help
  • in, insrc: Reading Input Files
  • l: Listing
  • lprec: Listing of the Precedence
  • out: Dumping Theories to Files
  • prec: Precedence Definition
  • prove: Theorem Proving
  • rp: Displaying Proofs
  • sat: Starting Saturation
  • translate: Translating Modal Logic Formulas
  
  
• Heuristics for the Definition of Meta-Logical Directives
  • General
  • Settings for Refutational Theorem Proving
  • Saturation of a Theory
  • Establishing Complexity Bounds
  
  
• Bibliography
• Release Notes
• Known Bugs

Imprint | Data Protection