next up previous
Next: Decomposition methods Up: KL-components Previous: Resolution methods

Lift definitions

are a particular class of resolution methods which translate between the vocabularies and representation formalisms of different models. They allow resolution methods to use the knowledge contents of different models by establishing mappings between the representation formalisms used by models (formula-schemas) and resolution method arguments (term-schemas). The possibility of establishing these mappings enhances the reusability of models and methods across domains, as we will see in section 3. Meta-variables and lift-variables are used respectively to describe the syntactical structure of formula-schemas and term-schemas. Mappings provide the translation rules between formula-schemas and term-schemas.

use tex2html_wrap_inline1127 *
sorts sort tree
metavariables (metavar +: metatype) *
liftvariables (varsymbol +: metatype) *
mappings (lift(expression) tex2html_wrap_inline1133 termschema) *

The operator use allows including a lift definition (i.e. its language and mappings) within a theory or another lift definition.


A partial order relation tex2html_wrap_inline1137 , which formalizes the notion of instance, can be defined on term and formula schemas (s denotes a substitution).

1. Let tex2html_wrap_inline1141 be two formulaschemas, tex2html_wrap_inline1143 if tex2html_wrap_inline1145
2. Let tex2html_wrap_inline1147 be two termschemas tex2html_wrap_inline1149 if tex2html_wrap_inline1151

A mapping tex2html_wrap_inline1153 is a total, bijective, bothsides order preserving function

Total: tex2html_wrap_inline1155
1. tex2html_wrap_inline1157
2. tex2html_wrap_inline1159
Bothsides order preserving:
1. tex2html_wrap_inline1161
2. tex2html_wrap_inline1163

The following examples show the formal descriptions of some lift definitions. Note that tex2html_wrap_inline1165 uses tex2html_wrap_inline1167 as part of its definition.

tex2html_wrap1187 \ tex2html_wrap1189