Selecting the redundancy proof techniques

This is done with the command sarp. Redundancy proofs allow to

• simplify clauses, including
  • simplification by (contextual) reduction (demodulation),
  • simplification by totality resolution,
  • condensement,
  • applying specific propositional techniques to sets of ground clauses, and
  • simplification by applying ``noncritical'' tableau expansions;
• delete redundant clauses by
  • tautology detection,
  • subsumption,
  • case analysis over all possible orderings of variables, and
  • clausal rewriting.

More information on these techniques is contained in (Bachmair & Ganzinger, 1994 b) and a paper by Nivela and Nieuwenhuis.

Imprint | Data Protection