Limitations and final remarks

Metaformulas extend the expressive power of defining rules and constraints for ConceptBase Objectbases. The implementation of this mechanism is not complete at the moment, but should enable the use of the most frequently requested concepts like single and necessary. Some limitations are listed below:

• limited partial evaluation
  The partial evaluation procedure is limited to a conjunction of literals, preceeded by forall-quantors.
• no source-to-source transformation
  Formulas are not converted automatically into the form mentioned above supported by the metaformula mechanism, even if they could be transformed. If the class-variables can't be bound using partial evaluation of the input-formula, the formula is rejected, even if there exists an equivalent formula, in which partial evaluation could be used to bind the class-variables.
• not all classes are supported
  Generated formulas where variables are quantified over instances of the following classes or attributes of them will be ignored. Those classes are:
  Boolean,Integer,Real,String,TransactionTime,
  MSFOLassertion,MSFOLrule,MSFOLconstraint,
  metaMSFOLconstraint,metaMSFOLrule,
  BDMConstraintCheck,BDMRuleCheck,LTruleEvaluator,ExternalReference,
  QueryClass, BuiltinQueryClass,AnswerRepresentation,
  GraphicalType,X11_Color,ATK_TextAlign,
  ATK_Fonts,ATK_LineCap,ATK_ShapeStyle
  The justification is twofold. Some of these generated formulas, e.g. a formula beginning with

   $ forall x/1 ...$

  are regarded as redundant, because the object 1 as instance of Integer should have no instances. Another justification is, that the use of metaformulas should be restricted to user-defined modeling tasks. Manipulation of the most system classes is disabled for reasons of efficiency and safety.

In the case of deductive rules, additional problems arise similar to the straticfication problem. At the moment only monotonous transactions are allowed. This means that generated formulas can only be inserted or deleted during one transaction, both operations at the same time are not permitted.

The metaformula mechanism also influences the efficiency of the system: every transaction has to be supervised wether it affects the metaformulas or one of the generated formulas. If the preconditions of the generated formulas don't hold anymore, e.g. if the instances of EntityType!eAttr are no longer instances of Proposition!necessary in the previous model, the corresponding generated formula has to be deleted. If additional attributes are instantiated to Proposition!necessary, additional formulas have to be created. The process of supervising the transactions is quite expensive and if it slows down the overall performance too much, some of the metaformuals can be disabled temporarily (Untelling a metaformula removes all the code generated).

We encourage to use metaformulas for modelling tasks, but we discourage their use them to define for example additional Telos-Axioms yet. If any problem arises, please don't hesitate to contact us.