next up previous
Next: Lift definitions Up: KL-components Previous: Models

Resolution methods

A Resolution method specifies how a task without further subtasks gets accomplished. Resolution methods consult, generate or modify the contents of models in order to carry out a task. This makes them meta-theories of the object-theories representing those models. They exploit some relationship among the contents of their inputs to generate the contents of their outputs. This relation is formally represented by an atomic formula of the form tex2html_wrap_inline1055 , where name is the name of the resolution method and tex2html_wrap_inline1057 are terms describing the syntactical structure required for its arguments. The actual relationship is defined by a set of axioms of the form tex2html_wrap_inline1059 , where tex2html_wrap_inline1061 can be any formula constructed from atomic formulae of the form tex2html_wrap_inline1063 and other predicates. In order to capture the executable aspect of resolution methods, we formalize them as Quantified Dynamic Logic (QDL) meta-theories. The QDL test operator ? allows us to turn the atomic formula associated to a resolution method into a test program tex2html_wrap_inline1065 . The execution state of a method is represented by state variables of the form tex2html_wrap_inline1067 , which contain the list of values that have been used or computed so far for each argument. The program tex2html_wrap_inline1069 , which adds an element to the front of a list, is used to store used or computed values for arguments in their respective state variables, and therefore to modify the execution state of the method. A QDL program tex2html_wrap_inline1071 is defined in order to specify the behavior of a resolution method, i.e how it modifies its state of execution in each circumstance.

sorts sort tree
constants (constantsymbol +: sortsymbol) *
functions (functionsymbol +: sortsymb tex2html_wrap_inline977 sortsymbol) *
predicates (predicatesymbol +: sortsymbol *) *
variables (variablesymbol +: sortsymbol) *
metavariables (varsymbol +: metatype) *
axioms tex2html_wrap_inline1087
tex2html_wrap_inline1089 *
program tex2html_wrap_inline1091
a QDL program made from tex2html_wrap_inline1065
conditions and programs on tex2html_wrap_inline1097

The following examples show the formal descriptions of some resolution methods.

tex2html_wrap1121 \ tex2html_wrap1123

next up previous
Next: Lift definitions Up: KL-components Previous: Models