Horn Logic Herbrand Semantic Profile of RuleML 1.02
- Identifier: http://ruleml.org/1.02/profiles/Horn-Herbrand
- Syntactic Scope: http://deliberation.ruleml.org/1.02/relaxng/myng-bf-d7-a7-l1-p0-i0-t0-q0-e1-sb.rnc
- Classification: Herbrand
- Body:
- Performatives (Assert, Retract, Query) sequentially induce effects on a dynamic global rulebase.
- The effect of Assert and Retract is to modify the state of the global rulebase.
- A "top-level" rulebase (a rulebase without a performative wrapper) is processed as an implicit Assert of that rulebase.
- Before any performative is applied, the global rulebase is empty.
- The effect of Assert is to add its formula payload (formulas contained directly or indirectly through a rulebase wrapper) to the global rulebase.
- The effect of Retract is to (syntactically) subtract its formula payload from the global rulebase.
- The effect of Query is to generate a query result w.r.t. the global rulebase. The global rulebase itself is unaffected.
- A query result is either
- a success, if one or more substitutions for the (zero or more) free variables are entailed by the global rulebase. If the query contains free variables, then additionally the query result may contain a tabulation of these substitutions. If the query contains no free variables, then the tabulation is empty.
- a failure, if no substitution for the free variables is entailed by the global rulebase.
- A query result is either
- While the semantics of performatives is defined above, the semantics of its formula payloads is defined according to Lloyd^{[1]}.
- A mapping between the definite program syntax of Lloyd^{[2]} and subset of the Assert-formula payloads of the RuleML/XML Syntactic Scope of this profile is defined in two steps:
- The RuleML/XML syntax is mapped to a RIF-like presentation syntax^{[3]} (with RuleML performatives) by χ_{horn}^{-1}, the inverse of the bijective mapping χ_{horn} defined in #Presentation-to-XML Syntax Mapping
- The Assert-formula subset of the RIF-like presentation syntax is mapped to the definite programs defined by Lloyd
- Atoms are mapped in a mostly structure-preserving manner, except:
- Atoms directly in Asserts are mapped from formulas to "←"-postfixed formulas in definite programs
- Implications are mapped by recursively mapping their conclusions (atoms) and conditions (atoms or polyadic conjunctions) in a mostly structure-preserving manner, except:
- Implications are mapped from ":-"-infixed formulas (always directly in Asserts) to "←"-infixed formulas (always directly in definite programs)
- Polyadic conjunctions are mapped from And(...)-applying formulas (always in conditions of implications in Asserts) to comma-infixed formulas (always in conditions of implications in definite programs)
- Expressions are mapped in a structure-preserving manner
- Constants are mapped from "_"-prefixed terms, _name, to terms built from the subscripted letter c, c_{name}
- Variables are mapped from "?"-prefixed terms, ?name, to terms built from the subscripted letter v, v_{name}
- Atoms are mapped in a mostly structure-preserving manner, except:
- Performatives (Assert, Retract, Query) sequentially induce effects on a dynamic global rulebase.
- Parent: Predefined Semantic Profiles of RuleML 1.02
- Example: http://deliberation.ruleml.org/1.02/exa/Hornlog/hornlog/brokerBK.ruleml
Contents
1 Presentation-to-XML Syntax Mapping
A mapping, χ_{horn}, is defined from the RIF-like presentation syntax to the XML syntax of RuleML. It is similar to the mapping χ_{bld} from the presentation syntax to the XML syntax of RIF-BLD^{[4]}. The mapping is given via tables where each row specifies the translation of a particular syntactic pattern in the presentation syntax: χ_{horn}(Presentation) = XML. These Presentation patterns appear in the first column of the tables, where the bold-italic symbols represent metavariables. The second column represents the corresponding XML patterns, which may contain applications of the mapping χ_{horn} to these metavariables. When an expression χ_{horn}(metavar) occurs in an XML pattern in the right column of a translation table, it should be understood as a recursive application of χ_{horn} to the presentation syntax represented by the metavariable. The XML syntax result of such an application is substituted for the expression χ_{horn}(metavar). A sequence of terms containing metavariables with subscript n is indicated by an ellipsis. It is understood that n≥0, i.e. the ellipsis indicates zero or more terms.
1.1 Condition Language Mapping
The χ_{horn} mapping from the presentation syntax to the XML syntax of the Horn-Herbrand Condition Language is specified by the table below. Since the RIF-like presentation syntax is context sensitive, the mapping must differentiate between the terms that occur in the position of individuals and the terms that occur as atomic formulas. To this end, in the translation table, the terms that occur in the context of atomic formulas are denoted by expressions of the form pred(...) and the terms that occur as individuals are denoted by expressions of the form func(...).
Presentation Syntax | XML Syntax |
---|---|
And ( conjunct_{1} . . . conjunct_{n} ) |
<And> <formula>χ_{horn}(conjunct_{1})</formula> . . . <formula>χ_{horn}(conjunct_{n})</formula> </And> |
Or ( disjunct_{1} . . . disjunct_{n} ) |
<Or> <formula>χ_{horn}(disjunct_{1})</formula> . . . <formula>χ_{horn}(disjunct_{n})</formula> </Or> |
Exists variable_{1} . . . variable_{n} ( condition ) |
<Exists> <declare>χ_{horn}(variable_{1})</declare> . . . <declare>χ_{horn}(variable_{n})</declare> <formula>χ_{horn}(condition)</formula> </Exists> |
pred ( argument_{1} . . . argument_{n} ) |
<Atom> <op>χ_{horn}(pred)</op> <arg> χ_{horn}(argument_{1}) </arg> . . . <arg> χ_{horn}(argument_{n}) </arg> </Atom> |
func ( argument_{1} . . . argument_{n} ) |
<Expr> <op>χ_{horn}(func)</op> <arg> χ_{horn}(argument_{1}) </arg> . . . <arg> χ_{horn}(argument_{n}) </arg> </Expr> |
_name |
<Ind>χ_{horn}(name)</Ind> |
?name |
<Var>χ_{horn}(name)</Var> |
1.2 Rule Language Mapping
The χ_{horn} mapping from the presentation syntax to the XML syntax of the Horn-Herbrand Rule Language is specified by the table below. It extends the translation table of #Condition Language Mapping.
Presentation Syntax | XML Syntax |
---|---|
RuleML( performative_{1} . . . performative_{n} ) |
<RuleML> <act>χ_{horn}(performative_{1})</act> . . . <act>χ_{horn}(performative_{n})</act> </RuleML> |
Assert( clause_{1} . . . clause_{n} ) |
<Assert> <formula>χ_{horn}(clause_{1})</formula> . . . <formula>χ_{horn}(clause_{n})</formula> </Assert> |
Retract( clause_{1} . . . clause_{n} ) |
<Retract> <formula>χ_{horn}(clause_{1})</formula> . . . <formula>χ_{horn}(clause_{n})</formula> </Retract> |
Query( clause_{1} . . . clause_{n} ) |
<Query> <formula>χ_{horn}(clause_{1})</formula> . . . <formula>χ_{horn}(clause_{n})</formula> </Query> |
Forall variable_{1} . . . variable_{n} ( rule ) |
<Forall> <declare>χ_{horn}(variable_{1})</declare> . . . <declare>χ_{horn}(variable_{n})</declare> <formula>χ_{horn}(rule)</formula> </Forall> |
conclusion :- condition |
<Implies> <if>χ_{horn}(condition)</if> <then>χ_{horn}(conclusion)</then> </Implies> |
2 References
- ↑ Lloyd, J. 1987. Foundations of Logic Programming. 2nd ed. Springer-Verlag. Chapter 2, Section §6. See https://books.google.com/books/about/Foundations_of_Logic_Programming.html?id=P10ZAQAAIAAJ
- ↑ Lloyd, J. 1987. Foundations of Logic Programming. 2nd ed. Springer-Verlag. Chapter 1, Section §2. See https://books.google.com/books/about/Foundations_of_Logic_Programming.html?id=P10ZAQAAIAAJ
- ↑ Boley, H. and Kifer, M. (Editors) 2013. RIF Basic Logic Dialect (Second Edition). W3C Recommendation. See https://www.w3.org/TR/rif-bld/#Direct_Specification_of_RIF-BLD_Presentation_Syntax.
- ↑ Boley, H. and Kifer, M. (Editors) 2013. RIF Basic Logic Dialect (Second Edition). W3C Recommendation. See https://www.w3.org/TR/rif-bld/#Mapping_from_the_Presentation_Syntax_to_the_XML_Syntax.