This document extends the model I proposed for Horn rules for RIF Phase 1 to a "kind-of-mini-PR" dialect.
It is kind of a production rule dialect because the then-part specifies actions instead of a head and because it inherits the syntax and semantics incorporates RIF Positive Conditions defined in Section Positive Conditions, thus requiring full unification instead of the pattern matching that is usual in production rule engines.
It is mini in the sense that the only actions it allows are the assertion and the retraction of a single atom.
The purpose is to explore the extension of a dialect with a feature that changes the semantics of the extended dialect: in this case, RETRACT.
Syntax
Abstract Syntax
The abstract syntax of the Horn rule language extending Positive Conditions is given in asn07 as follows:
class Ruleset property formula : list of RULE class RULE subclass Forall property declare : Var+ property formula : RULE subclass ACTION subclass Implies property if: CONDITION property then: ACTION class ACTION property fact: ATOMIC subclass ASSERT subclass RETRACT
The abstract syntax is visualized by a UML diagram extending the UML diagram of Positive Conditions as shown below.
The central RIF Ruleset class contains zero or more RULEs. RIF Core enables the interchange of rules that are universally closed Horn clauses that contain one and only one positive literal. This is represented in RIF Core by a RULE being either:
an Implies, which distinguishes if-CONDITION from then-ACTION parts;
an ACTION formula, for representing Implies where the then-part is always true and is omitted, by convention;
or a Forall, recursively. The class Forall is specified through its parts, i.e. one or more variable (Var) declarations and a RULE as the formula in its scope. RIF does not allow implicitely quantified variables: all the variables that are implicitely universally quantified in an Implies or an ATOMIC MUST be within the scope of a Forall that declares them.
RIF Core thus enables the interchange of rules that are universally closed Horn clauses with one and only one positive literal, and where the universal quantifiers that are often left implicit are made explicit.
Upload new attachment "PRmini.png"
The classes Var, CONDITION, and ATOMIC were specified in the abstract syntax of Positive Conditions.
Compatibility with RIF Core
The MiniPR RIF dialects extends RIF Core by adding the possibility to retract facts.
The semantics of a MiniPR RULE that contains a RETRACT are not defined in RIF Core. As a consequence, an implementation of RIF Core that does not implement RIF MiniPR as well MUST produce an ERROR when translating a MiniPR Ruleset that contains a RETRACT.
The semantics of a MiniPR RULE that contains an ASSERT are compatible with the semantics of RIF Core rules: when translating a MiniPR Ruleset, an implementation of RIF Core that does not implement RIF MiniPR as well MUST replace all ASSERT constructs by the asserted fact, which is an ATOMIC, thus falling back on RIF Core syntax. When applying this replacement rule, an implementation MUST produce a warning that, since the Ruleset originates from a non-monotonic dialect, it is the user's responsibility to consider the infered ATOMIC irrefragable knowledge when the Ruleset is aggregated with other sources of rules.
Conversely, when translating a RIF Core Ruleset, an implementation of RIF MiniPR MAY replace all the ATOMIC in the then-part of a RULE by an ASSERT action where the asserted fact is the replaced ATOMIC. When applying this replacement rule, an implementation MUST produce a warning that, since the Ruleset originates from a monotonic dialect, it is the user's responsibility to aggregate it with other sources of knowledge that may retract the asserted ATOMIC.
*** The point of the warnings is that, as long as a ruleset that contains only ASSERTs is not aggregated with other rulesets that may contains RETRACTs, it behaves as if the ASSERT was monotonic. ***
Concrete Syntax
TBD
Semantics
TBD