An instantiated resolution method (IRM) applies the generic inference capability of a resolution method to the specific contents of some models in order to carry out a particular task. It is a KL-structure constituted by a resolution method and a (possibly empty) set of models and lifts. It establishes input/output relations between its models and certain roles (arguments) of its resolution method. In particular, it uses input/output axioms and lift definitions to enable the communication and translation of knowledge contents between its resolution method and the models it uses.
A resolution method input axiom is a formula of the form
which, in combination with a reflection rule called ask, reduces the deduction of the atomic formula to a test for axiom-hood in the object theory of the formula to which associates the meta-name .
A resolution method output axiom is a formula of the form
which, in combination with a reflection rule called tell, ensures that each time a new value for the output role is computed by the method and added to its state variable , an axiom reflecting the contents of the new value is added to the object theory . The axiom which reflects down (in the object theory ) the contents of is obtained by applying backwards to the appropriate mapping of .