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 .