Users can make formulas, rewrite rules, and deduction rules immune or ancestor-immune to protect them from automatic normalization, both to enhance the performance of LP and to preserve particular forms for use in a proof. Users can also deactivate rewrite rules to prevent them from being applied automatically. Whenever a new deduction rule is added to its logical system, LP automatically applies that deduction rule to all formulas and rewrite rules. Likewise, whenever a formula or rewrite rule is normalized, LP automatically applies all deduction rules to the new normal form. Inactive deduction rules are not used for automatic deduction, and immune formulas and rewrite rules are not subject to automatic deduction.
Users can also apply deduction rules explicitly, for example, to immune formulas.
It is generally impossible or overly costly to complete a rewriting system. However, the completion procedure can be used to look for inconsistencies in a system, or to perform the final steps in some proofs. The instantiate command enables users to eliminate universal quantifiers, or to replace free variables by terms, in formulas, rewrite rules, and deduction rules. The fix command enables users to eliminate existential quantifiers in formulas and rewrite rulest to produce a conservative extension of LP's logical system.