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 .

jsierra@cs.stanford.edu