Disjunctive Heads as an Implication Option

From RuleML Wiki
Jump to: navigation, search

--Athant (talk) 17:10, 17 March 2014 (ADT)

1 Issue Description

For a more fine-grained modularazation that allows sublanguages such as Disjunctive Datalog, implement the inclusion of disjunction into the heads of implications into a module that can be combined with languages at the level of Datalog expressivity and below. Then there is no need for Disjunctive Hornlog on the Expressivity Backbone. The disjunctive module already exists (dis_expansion_module.rnc), it just needs to be rewritten, and the MYNG GUI and engine modified slightly.

This change affects the following components

  1. Relax NG Schemas and their documentation
  2. Examples - a new test suite and an example of disdatalog are needed
  3. MYNG REST interface - new codes are required for the newly-created sublanguages (extend the implication options facet).
  4. MYNG GUI - a new item needs to be added to an existing facet, and one item is removed from the Expressivity Backbone facet.

The Glossary, Content Models and Normalizer are not affected. An Upgrader is not needed for this change.

See also the related issue MYNG Expressivity.

2 Options

2.1 Option 1

The new content for the "dis" module is

  Or-head-node.choice |= Or-head.Node.def
  Or-head.Node.def =
    
    ## within the head of implications
    element Or { (Or-datt.choice & reOr.attlist), Or.header, Or-head.main }
  Or-head.main |= formula_Or-head-edge.choice*
  formula_Or-head-edge.choice |= formula_Or-head.edge.def
  formula_Or-head.edge.def =
    
    ##
    element formula { formula_Or.attlist? & formula_Or-head.content }
  formula_Or-head.content |= OrHeadFormula.choice
  OrHeadFormula.choice |=
    Atom-node.choice
    | Equal-fo-node.choice
    | And-head-node.choice
    | Or-head-node.choice
    | Negation-head-node.choice
    | NegationAsFailure-node.notallowed
    | Implication-head-node.choice
    | Forall-head-node.choice
    | Exists-head-node.choice

On the MYNG GUI (index.html), the DisHornlog option is removed. Lines 13-22

                if (!(
                LanguageForm.backbone[0].checked *
                LanguageForm.backbone[1].checked *
                LanguageForm.backbone[2].checked *
                LanguageForm.backbone[3].checked *
                LanguageForm.backbone[4].checked *
                LanguageForm.backbone[5].checked)) {
                    // initialize to Full First-Order
                    LanguageForm.backbone[5].checked = true;

Line: 72

  fol = LanguageForm.backbone[5].checked;

Lines 80-111

                // In RuleML 1.01, non-default values of scope implication attributes
                // are allowed, even in fact languages with no implications
                LanguageForm.implies1.removeAttribute('disabled');
                LanguageForm.implies2.removeAttribute('disabled');                
                // for Ground Logic and up, all other implication options except existential heads are available
                // for FOL, conjunctive heads, disjunctive heads and negative constraints are implicit
                if (groundLogicAndUp) {
                    LanguageForm.implies0.removeAttribute('disabled');
                    if(fol) {
                      LanguageForm.implies3.checked = true;
                      LanguageForm.implies3.disabled = "disabled";
                      LanguageForm.implies4.checked = true;
                      LanguageForm.implies4.disabled = "disabled";
                      LanguageForm.implies5.checked = true;
                      LanguageForm.implies5.disabled = "disabled";
                    } else {
                      LanguageForm.implies3.removeAttribute('disabled');
                      LanguageForm.implies4.removeAttribute('disabled');
                      // If negative constraints are allowed, disjunctive heads are available
                     if (LanguageForm.implies4.checked) {
                       LanguageForm.implies5.removeAttribute('disabled');
                     } else {
                       LanguageForm.implies5.checked = false;
                       LanguageForm.implies5.disabled = "disabled";
                     }
                   }  
                } else {
                    LanguageForm.implies0.checked = false;
                    LanguageForm.implies0.disabled = "disabled";
                    LanguageForm.implies3.checked = false;
                    LanguageForm.implies3.disabled = "disabled";
                    LanguageForm.implies4.checked = false;
                    LanguageForm.implies4.disabled = "disabled";
                    LanguageForm.implies5.checked = false;
                    LanguageForm.implies5.disabled = "disabled";
                }
                // for Datalog and up, existential heads are available
                // for FOL, existential heads are implicit
                if (datalogAndUp) {
                    if(fol) {
                      LanguageForm.implies6.checked = true;
                      LanguageForm.implies6.disabled = "disabled";
                    } else {
                      LanguageForm.implies6.removeAttribute('disabled');
                    }  
                } else {
                    LanguageForm.implies6.checked = false;
                    LanguageForm.implies6.disabled = "disabled";
                }


Lines 211-216

                var bb = 0;
                for (i = 0; i < 5; i = i + 1) {
                    if (LanguageForm.backbone[i].checked) {
                        bb = Math.pow(2, i) - 1;
                    }
                }
                // Modification of encoding for backbone due to omission of dishornlog
                if (LanguageForm.backbone[5].checked) {
                        bb = Math.pow(2, 6) - 1;
                }

Line 224

                    if (LanguageForm.backbone[5].checked) {

Lines 276-281

                var implies = 0;
                for (i = 0; i <= 6; i = i + 1) {
                    if (eval("LanguageForm.implies" + i + ".checked")) {
                        implies = implies + Math.pow(2, i);
                    }
                }

Delete Lines 382-384

                <li>
                  <input type="radio" name="backbone" onclick="checkAll(this.form)" /> Disjunctive
                  Logic </li>

Lines 490-496

              <li>
                <input type="checkbox" name="implies3" onclick="checkAll(this.form)"
                  checked="checked" /> Conjunctive Heads </li>
              <li >
                <input type="checkbox" name="implies4" onclick="checkAll(this.form)"
                  checked="checked" /> Negative Constraints </li>
              <li style="margin-left:16px">
                <input type="checkbox" name="implies5" onclick="checkAll(this.form)"
                  checked="checked" /> Disjunctive Heads </li>
              <li>
                <input type="checkbox" name="implies6" onclick="checkAll(this.form)"
                  checked="checked" /> Existential Heads</li>
            </ol>


in schema_rnc.php Lines 104-106

  $implies_and = 3;
  $implies_nc = 4;
  $implies_dis = 5;
  $implies_ex = 6;


Lines 220-227

  //Apparent lack of monotonicity caused by containment of the
  // existential head module within the implementation of FOL.
  //Including the existential head module would be redundant in FOL.
  // Similar considerations hold for negative constraints and
  // conjunctive heads.
  $needExHead = extractBit($bimplies, $implies_ex)*(1-$needFO);
  $needNegConstraint = extractBit($bimplies, $implies_nc)*(1-$needFO);
  $needAndHead = extractBit($bimplies, $implies_and)*(1-$needFO);
  $needOrHead = ($needDis + extractBit($bimplies, $implies_or))*(1-$needFO);

Lines 304-308

    if ($needOrHead){
      echo "#\n# DISJUNCTIONS IN CONCLUSIONS INCLUDED\n";
      echo "#\n".'include "' . $modulesLocation .
          'dis_expansion_module.rnc"'."$end\n";
    }

3 Discussion

4 Resolution

This module has been integrated into the MYNG REST interface and MYNG GUI through an extension of the Implication Options facet of the MYNG-GUI, the "i" component of the myng-code and "implies" query parameter of the REST interface.

The disjunctive Horn logic bit in the myng-code is retained for backward compatibility. The bit should always be 1 whenever the expressivity is Horn logic and the disjunctive head option is enabled, so that a sublanguage containment evaluation can be properly made.