Semantic Styles of RuleML 1.02

From RuleML Wiki
Jump to: navigation, search

Authors: Adrian Paschke, Tara Athan, Harold Boley

This version: Semantic Styles of RuleML 1.02

Copyright © RuleML Inc. 2015 - 2016 -- Licensed under the RuleML Specification License 1.0 (http://ruleml.org/licensing/RSL1.0-RuleML)


RuleML 1.02 does not define one universal semantics, but supports a mechanism for indicating the intended logical consequences of a (single) RuleML document through predefined and user-defined semantic profiles. [1]

In all RuleML familes it is possible for a semantic style attribute (@style ) to occur on the root element, with a value that is an IRI. This IRI indicates the semantic profile which constrains or defines the logical consequences of a RuleML document. The syntactic scope of a semantic profile is the syntax to which it applies. A classification indicates the form of the semantic profile definition, e.g., a model-theoretic semantics [2], proof-theoretic semantics[3], operational semantics[4] (e.g., execution semantics, selection and consumption policies).

An entailment[5] set is a set of constraints on the intended logical consequences[6], i.e. intended model-theoretic entailments or proof-theoretic entailments. These entailment sets can be used as semantic profiles, which then can be referenced by a semantic style attribute.

1 Entailment Sets

Every specification of an entailment set must state a set of constraints on a compatible semantics, typically as laws [or (meta)rules] that are required to be supported in the entailment relation of a compatible semantics.

The specification of an entailment set may optionally include the following:

  • A statement of or reference to a (formal) definition language used in the entailment set's specification
  • The constraints of the entailment set expressed in this definition language
  • A pair of functions for bidirectional translation between the RuleML language and the definition language

The RuleML language itself is the preferred definition language for an entailment set.

2 Semantic Profiles

Every semantic profile must have the following components:

  • A specification of its syntactic scope
  • A classification indicating the mathematical form that the semantics definition takes, e.g. proof-theoretic, (e.g. Tarski or Herbrand) model-theoretic, operational or algebraic
  • A body containing the actual definition of the semantics or a reference to a defining document, typically in mathematical language

This definition might optionally include the following:

  • A definition or reference to a (sub-)signature used in the definition of the profile
  • A definition or reference to a (formal) language used in the profile's definition (the definition language)
  • The intended structures, e.g. the intended semantic structures for the interpretation
  • Additional domain-independent theories, defined e.g., axiomatically by entailment sets
  • A semantics-preserving translation function from the RuleML language into the profile's definition language (and/or an inverse translation function) in order to map the semantic interpretation of RuleML into the intended semantic structure of the profile
  • Bridge rules providing hybrid laws of deduction between the definition language and the RuleML language

Note, that the RuleML language itself might be used as the definition language for a semantic profile.

3 Predefined Semantic Styles

See Predefined Semantic Styles of RuleML 1.02

4 User-defined Semantic Styles

Users may freely define their own semantic profiles and refer to them in a semantic style attribute, or to the semantic profiles defined by others, e.g. W3C OWL profiles[7], W3C RIF profiles[8], W3C SPARQL entailment regimes[9].

4.1 Appendix 2: Examples

<!-- RuleML document with semantic style referencing reasoning  and FOL Herbrand semantic profiles-->
<RuleML style="reasoning FOL-Herbrand">...</RuleML>

<!-- User defined semantic profile defining SLDNF resolution as cut-fail rule -->
<Profile key="ruleml:SLDNF" direction="backward">

  <!-- Axiomatization of negation as failure
       not(Goal) :- derive(Goal), !, fail.
       not(Goal).            
  -->

  <Rulebase> 
       <Rule>
              <if>
                <And>
                  <Atom>
                    <Rel iri="prova:derive"/>
                    <Var>Goal</Var>
                  </Atom>
                  <Atom>
                    <Rel iri="prova:cut"/>
                  </Atom>
                  <Atom>
                    <Rel iri="prova:fail"/>
                  </Atom>
                </And>
              </if>
              <then>
                <Atom>
                  <Rel iri="ruleml:Naf"/>
                  <Var>Goal</Var>
                </Atom>
              </then>
            </Rule>
            
            <Atom>
              <Rel iri="ruleml:Naf"/>
              <Var>Goal</Var>
            </Atom>
            
     </Rulebase>           
        
</Profile>

5 References

  1. Reaction RuleML 1.0 for Rules, Events and Actions in Semantic Complex Event Processing, accessed 2016-02-05
  2. Model Theory: http://plato.stanford.edu/entries/model-theory/, accessed 2016-02-05
  3. Advances in Proof-Theoretic Semantics: http://link.springer.com/book/10.1007%2F978-3-319-22686-6, accessed 2016-02-05
  4. Operational Semantics: https://www.cs.cmu.edu/~fp/courses/lp/lectures/04-opsem.pdf, accessed 2016-02-05
  5. Logical consequence (also entailment), https://en.wikipedia.org/wiki/Logical_consequence, accessed 2016-02-07
  6. Beall, JC and Restall, Greg, Logical Consequence The Stanford Encyclopedia of Philosophy (Fall 2009 Edition), Edward N. Zalta (ed.).
  7. OWL 2 Web Ontology Language Profiles (Second Edition), https://www.w3.org/TR/owl2-profiles/, accessed 2016-02-05
  8. W3C RIF generic profile, https://www.w3.org/TR/rif-rdf-owl/#Generic_Profile, accessed 2016-02-05
  9. SPARQL 1.1 Entailment Regimes, https://www.w3.org/TR/sparql11-entailment/, accessed 2016-02-05