<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE doc [
  <!ENTITY vocab "http://ruleml.org/vocab">
]>
<?xml-model href="http://www.ruleml.org/1.0/relaxng/folog_relaxed.rnc" type="application/relax-ng-compact-syntax"?>
<!--<?xml-model href="http://www.ruleml.org/1.0/xsd/folog.xsd" type="application/xml" schematypens="http://www.w3.org/2001/XMLSchema"?>-->
<RuleML xmlns="http://ruleml.org/spec"
  xmlns:xs="http://www.w3.org/2001/XMLSchema"
  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
  xsi:schemaLocation="http://ruleml.org/spec http://www.ruleml.org/1.0/xsd/folog.xsd">

  <Assert>
    <!-- S5 Structural Axioms -->
    <Rulebase>
      <!-- K: Necessary (A->B) -> (Necessary A -> Necessary B) -->
      <Forall>
        <declare>
          <Var type="&vocab;core#Formula">?A</Var>
        </declare>
        <declare>
          <Var type="&vocab;core#Formula">?B</Var>
        </declare>
        <Implies>
          <if>
            <Atom>
              <Rel iri="&vocab;/ext#modal"/>
              <Ind iri="&vocab;/kripke#Necessary"/>
              <Reify>
                <Implies>
                  <if>
                    <!-- The RuleML folog syntax does not allow quantification over predicates,
                    therefore we use a construction equivalent to an "ist" (is true) operator:
                    
                    <Atom>
                    <Rel iri="&vocab;/ext#truthValue"/>
                    <Ind iri="&vocab;/ext#True"/>
                    <Reify>P</Reify>
                    </Atom>
                    exactly when P is a true wff.
                    See IKL semantics @@@ref
                    
                  -->
                    <Atom>
                      <Rel iri="&vocab;/ext#truthValue"/>
                      <Ind iri="&vocab;/ext#True"/>
                      <Var>?A</Var>
                    </Atom>
                  </if>
                  <then>
                    <Atom>
                      <Rel iri="&vocab;/ext#truthValue"/>
                      <Ind iri="&vocab;/ext#True"/>
                      <Var>?B</Var>
                    </Atom>
                  </then>
                </Implies>
              </Reify>
            </Atom>
          </if>
          <then>
            <Implies>
              <if>
                <Atom>
                  <Rel iri="&vocab;/ext#modal"/>
                  <Ind iri="&vocab;/kripke#Necessary"/>
                  <Var>?A</Var>
                </Atom>
              </if>
              <then>
                <Atom>
                  <Rel iri="&vocab;/ext#modal"/>
                  <Ind iri="&vocab;/kripke#Necessary"/>
                  <Var>?B</Var>
                </Atom>
              </then>
            </Implies>
          </then>
        </Implies>
      </Forall>
      <!-- T: A is necessary implies A -->
      <Forall>
        <declare>
          <Var type="&vocab;core#Formula">?A</Var>
        </declare>
        <Implies>
          <if>
            <Atom>
              <Rel iri="&vocab;/ext#modal"/>
              <Ind iri="&vocab;/kripke#Necessary"/>
              <Var>?A</Var>
            </Atom>
          </if>
          <then>
            <Atom>
              <Rel iri="&vocab;/ext#truthValue"/>
              <Ind iri="&vocab;/ext#True"/>
              <Var>?A</Var>
            </Atom>
          </then>
        </Implies>
      </Forall>
      <!-- 5: Possible A implies Necessary Possible A -->
      <Forall>
        <declare>
          <Var type="&vocab;core#Formula">?A</Var>
        </declare>
        <Implies>
          <if>
            <Atom>
              <Rel iri="&vocab;/ext#modal"/>
              <Ind iri="&vocab;/kripke#Possible"/>
              <Var>?A</Var>
            </Atom>
          </if>
          <then>
            <Atom>
              <Rel iri="&vocab;/ext#modal"/>
              <Ind iri="&vocab;/kripke#Necessary"/>
              <Reify>
                <Atom>
                  <Rel iri="&vocab;/ext#modal"/>
                  <Ind iri="&vocab;/kripke#Possible"/>
                  <Var>?A</Var>
                </Atom>
              </Reify>
            </Atom>
          </then>
        </Implies>
      </Forall>
    </Rulebase>
  </Assert>

</RuleML>
