Reference: Makarios, S.; Heuer, K. Building-In New Inference Rules for Computational Context Logic. 2006.
Abstract: A crude approach to incorporating equality into automated reasoners involves the naive application of the equality axiom schema: starting from a given theory, collect all of the function an predicate symbols it uses, and instantiate the monotonicity axioms, one for each function and one for each predicate. Unfortunately this can make reasoning over the resulting system computationally unattractive due to the resulting enlargement of the search space. However, an alternative [] is to devise a new rule of inference that captures the properties of equality directly, and to build these properties directly in to an automated theorem prover. Likewise, the context specialization operator is formally defined in terms of an axiom schema, one with structural similarities to the axiom schema for equality. An earlier implementation of context-logic reasoning [] took the naive approach to automated reasoning about context specialization of using the direct instantiation of the context-specialization axiom schema over the vocabulary of each particular input theory. Our subsequent work has produced a new inference rule, suitable for use in a resolution-based system, that directly captures the behavior of the {\em specializes} operator, in a fashion analogous to paramodulation capturing the behavior of equality. This technique, and other examples of {\em building-in} various aspects of context logic reasoning, are detailed in this document.
Notes:
Full paper available as pdf.