next up previous
Next: Rule I Up: Composition rules and KL-structures Previous: Composition rules and KL-structures

Instantiated resolution methods

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 askgif, reduces the deduction of the atomic formula tex2html_wrap_inline1249 to a test for axiom-hood in the object theory tex2html_wrap_inline1251 of the formula to which tex2html_wrap_inline1253 associates the meta-name tex2html_wrap_inline1255 .

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 tex2html_wrap_inline1255 is computed by the method and added to its state variable tex2html_wrap_inline1259 , an axiom reflecting the contents of the new value is added to the object theory tex2html_wrap_inline1251 . The axiom which reflects down (in the object theory tex2html_wrap_inline1251 ) the contents of tex2html_wrap_inline1255 is obtained by applying backwards to tex2html_wrap_inline1255 the appropriate mapping of tex2html_wrap_inline1253 .