Splittable Head Conjunction Semantic Profile of RuleML 1.03

From RuleML Wiki
Jump to: navigation, search
  • Identifier: http://ruleml.org/1.03/profiles/splittableHeadConjunction
  • Consequence Relation
    The logic must support a consequence relation between sets of logical formulas.
  • Laws of Deduction:
    Laws of deduction supported by the @@@consequence relation of the@@@ logic must satisfy the following properties. The properties apply to RuleML elements (in the namespace http://ruleml.org/spec) as specified below, and also to such elements decorated with unqualified attributes and child elements in the RuleML namespace, provided these attributes and elements are declared as annotational in the glossary of the appropriate specification. The inferences from premises with attributes may not be assumed to inherit these attributes. The properties are stated in terms of XML fragments in the normalized serialization, but also apply to any set of XML fragments that would be mapped to these by the official normalizer XSLT transformation.
    The laws are stated in a non-traditional form in order to allow the greatest flexibility in accommodating non-monotonic (esp. non-reflexive), as well as monotonic, logics. The law template is as follows:
    If Q is inferred from theory G union S, then Q is inferred from theory G union T, where G is an arbitrary set of logical formulas, Q is an arbitrary logical formula, and S, T are sets of logical formulas of a specified form.
    In the case that the semantics is reflexive, the law premises would be satisfied if Q is a member of S and G is the empty set. If the law premises are satisfied in this way, then the law conclusion holds and therefore T entails S, which is the traditional form of these laws.
    In all of the following laws, G is an arbitrary set of logical formulas.
    1. Conjunctive Head Joining:
      Let P, Q, and R denote logical formulas and ... denote a sequence of zero or more logical formulas enclosed in <formula> tags, with @index values adjusted as necessary.
      • If Q is inferred from {G, <Implies><if>R</if><then><And>P ...</And></then></Implies>}, then Q is inferred from {G, <Implies><if>R</if><then>P</then></Implies>, <Implies><if>R</if><then><And>...</And></then></Implies>}.
    2. Conjunctive Head Splitting:
      Let P, Q, and R denote logical formulas and ... denote a sequence of zero or more logical formulas enclosed in <formula> tags, with @index values adjusted as necessary.
      • If Q is inferred from {G, <Implies><if>R</if><then>P</then></Implies>, <Implies><if>R</if><then><And>...</And></then></Implies>}, then Q is inferred from {G, <Implies><if>R</if><then><And>P ...</And></then></Implies>}.
  • Parent: Predefined Semantic Profiles of RuleML 1.03
  • Example: http://deliberation.ruleml.org/1.03/exa/DatalogPlus/datalogplus-key-keyref.ruleml

References