Semantic Styles of RuleML 1.02
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. 
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 , proof-theoretic semantics, operational semantics (e.g., execution semantics, selection and consumption policies).
An entailment set is a set of constraints on the intended logical consequences, 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
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, W3C RIF profiles, W3C SPARQL entailment regimes.
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>
- Reaction RuleML 1.0 for Rules, Events and Actions in Semantic Complex Event Processing, accessed 2016-02-05
- Model Theory: http://plato.stanford.edu/entries/model-theory/, accessed 2016-02-05
- Advances in Proof-Theoretic Semantics: http://link.springer.com/book/10.1007%2F978-3-319-22686-6, accessed 2016-02-05
- Operational Semantics: https://www.cs.cmu.edu/~fp/courses/lp/lectures/04-opsem.pdf, accessed 2016-02-05
- Logical consequence (also entailment), https://en.wikipedia.org/wiki/Logical_consequence, accessed 2016-02-07
- Beall, JC and Restall, Greg, Logical Consequence The Stanford Encyclopedia of Philosophy (Fall 2009 Edition), Edward N. Zalta (ed.).
- OWL 2 Web Ontology Language Profiles (Second Edition), https://www.w3.org/TR/owl2-profiles/, accessed 2016-02-05
- W3C RIF generic profile, https://www.w3.org/TR/rif-rdf-owl/#Generic_Profile, accessed 2016-02-05
- SPARQL 1.1 Entailment Regimes, https://www.w3.org/TR/sparql11-entailment/, accessed 2016-02-05