This document specifies the Rulelog Dialect of RIF, RIF-Rulelog a language for exchanging rules among systems that are based on the (vastly extended) Logic Programming paradigm with the well-founded semantics. Apart from the well-founded semantics, the main features of RIF-Rulelog include defeasible reasoning, omni-directional rules, Lloyd-Topor extensions, support for Skolem functions, formula reification, and more. Like [RIF-BLD], RIF-Rulelog supports the frame syntax. In addition, it supports higher-order syntax as in [HiLog93]. The RIF-Rulelog presentation syntax and semantics are specified as specializations of the RIF Framework for Logic Dialects (RIF-FLD). The XML serialization syntax of RIF-Rulelog is also given as a specialization of the XML syntax of RIF-FLD.
This specification develops RIF-Rulelog, the Rulelog dialect of RIF. RIF-Rulelog is intended to capture the paradigm of declarative logic programming that is based on the well-founded semantics (WFS) [GRS91,Prz94] with numerous extensions, which include defeasible reasoning, omni-directional rules, Skolem functions, frame and higher-order syntax, and Lloyd-Topor extensions. RIF-Rulelog is defined here as a specialization of the RIF framework for logic-based dialect [RIF-FLD], and high level of familiarity with RIF-FLD as well as with the well-founded semantics for default negation is assumed.
Syntactically, RIF-Rulelog corresponds to the language of rules with function symbols and negation (both default and explicit), where rule heads cannot contain disjunctions. Although RIF-Rulelog is Turing-complete, knowledge representation based on such rules is incomparable to the other popular logic programming paradigm, one that is based on answer-set programming (ASP) [GLe02]. One of the key differences is that RIF-Rulelog cannot do reasoning by cases.
Compared to standard logic programming, RIF-Rulelog has a number of syntactic extensions. These include objects and frames as in F-logic [KLW95], higher-order features [HiLog93], defeasible reasoning based on LPDA-WFS (logic programs with defaults and argumentation theories based on the well-founded semantics) [LPDA09], internationalized resource identifiers (or IRIs, defined by [RFC-3987]) as identifiers for concepts, and XML Schema datatypes [XML-SCHEMA2], Skolem functions, and omni-directional rules.
RIF-Rulelog is a proper extension of [RIF-BLD] and the Core Logic Programming Dialect based on the well-founded semantics [RIF-CLPWD] -- both syntactically and semantically. Compared to RIF-BLD [RIF-BLD], RIF-Rulelog supports two kinds of negation, Naf (default negation with the WFS semantics) and Neg (the explicit negation), and a variety of other features, such as defeasible and omni rules, typing, and others. Compared to [RIF-CLPWD], RIF-Rulelog supports the equality connective, defeasible reasoning, omni rules, and more.
The following examples, taken from [RIF-CLPWD], illustrate some basic syntactic features of RIF-Rulelog, which are not found in RIF-BLD.
The following example illustrates the use of both explicit and default negation.
The first rule here says that an individual is afraid of Math, if he is a student and it is not known (not explicitly stated) that that individual is not afraid of Math. Not being explicitly stated is expressed here by means of explicit negation Neg, while not being known is expressed by means of the default negation Naf. The second rule says that if an individual is a student majoring in Math then it is explicitly stated that that individual is unafraid of Math.
Document( Prefix(ex <http://example.com/concepts#>) Group ( Forall ?S ( ex:afraid(?S ex:Math) :- And ( ?S#ex:Student (Naf Neg ex:afraid(?S ex:Math)) ) ) Forall ?S ( Neg ex:afraid(?S ex:Math) :- And ( ?S#ex:Student ?S[ex:majors -> ex:Math] ) ) ) )
If we also had the facts ex:Joe#ex:Student and ex:Joe[ex:majors -> ex:Math] then we could conclude Neg ex:afraid(ex:Joe ex:Math) by the second rule. We will also be able to infer ex:afraid(ex:Joe ex:Math) by the first rule, which intuitively is a contradiction. In the RIF-Rulelog semantics, the well-founded model of such a knowledge base is said to be inconsistent. However, this does not destroy the KB completely in the sense that not everything is derivable. For instance, ex:afraid(ex:Nancy ex:Math) is derivable, but Neg ex:afraid(ex:Nancy ex:Math) is not. In a correctly built knowledge base, the above rules would have to be adjusted to avoid unintended conclusions (for example, by adding a conjunct of the form Naf ?S[ex:majors -> ex:Math] to the body of the first rule). ☐
The presentation syntax of RIF-Rulelog is defined by specialization from the presentation syntax of the RIF Syntactic Framework for Logic Dialects described in [RIF-FLD]. Section Syntax of a RIF Dialect as a Specialization of the RIF Framework in [RIF-FLD] lists the parameters of the syntactic framework in mathematical English, which we will now specialize for RIF-Rulelog.
All extension points of RIF-FLD are removed (specialized by replacing them with zero objects).
The alphabet of the RIF-Rulelog presentation syntax is identical to the alphabet of RIF-FLD.
Unlike RIF-BLD, RIF-Rulelog does not impose strict separation between individuals, predicates, and functions. As a result, the signature structure is much simplified. More specifically, RIF-Rulelog contains the following signatures:
The signature individual{ } represents the context in which individual objects can appear. The signature atomic is the standard signature of RIF-FLD, which represents the context where atomic formulas can occur.
In the definitions of the remaining signatures, below, the symbol Τ stands for either individual or atomic.
The above arrow expressions imply that an equality term is both an atomic formula and an individual. Therefore, such terms can occur anywhere an individual can occur, including arguments to predicates, functions, and so on.
Note that this allows frame terms to occur as arguments to predicates, functions, or as components in frame terms.
Again, this allows membership terms to occur as arguments to predicates, functions, or other terms.
As with frames and membership terms, this allows subclass terms to occur inside other terms.
Thus, a symbol can can appear in the position of an individual, a function, or a predicate without restrictions. However, the same symbol cannot represent both an external function/predicate and a regular one. This follows from the additional restrictions below.
RIF-Rulelog uses no special syntax for declaring signatures. Instead, the rule author specifies signatures contextually. That is, since RIF-Rulelog requires that each symbol can be either an external symbol or a regular symbol, if the same symbol occurs as both in different contexts then the parser must treat this as a syntax error. If no errors are found, all terms and atomic formulas are guaranteed to be well-formed. Thus, signatures are not part of the RIF-Rulelog language, and individual, atomic, list, fp, etc., are not reserved keywords.
It thus follows that a predicate or a function symbol, s, that occurs in an external term External(s(...)) cannot also occur as a non-external symbol.
RIF-Rulelog requires the symbol spaces defined in Section Constants, Symbol Spaces, and Datatypes of [RIF-DTB].
RIF-Rulelog supports the following types of formulas (see Well-formed Terms and Formulas in [RIF-FLD] for the definitions):
A RIF-Rulelog condition is an atomic formula, an external atomic formula, a negated (normal or external) atomic formula, or it is composed of such formulas using conjunctions and disjunctions. All these can be optionally preceded with existential quantifiers. A negated atomic formula has the form or either Neg φ, Naf ψ, or Naf Neg φ, where φ is a normal atomic formula and ψ is a normal or external atomic formula, i.e., classical negation cannot be applied to external atomic formulas.
A RIF-Rulelog rule is a RIF-FLD rule implication or a universally quantified RIF-FLD rule with the following restrictions:
A RIF-Rulelog rule can have free (non-quantified) variables. The semantics of RIF-Rulelog treats them as if they were implicitly quantified outside of the rule (i.e., if r is a rule with a free variable ?X then this is considered to be equivalent to Forall ?X (r)).
A RIF-Rulelog fact is a (optionally universally quantified) atomic formula or a negated atomic formula that does not include Naf. Free variables in such facts are assumed to be implicitly universally quantified.
A RIF-Rulelog group is a RIF-FLD group formula that contains only RIF-Rulelog rules, RIF-Rulelog facts, and RIF-Rulelog groups.
A RIF-Rulelog document is a RIF-FLD document that consists of directives and a RIF-Rulelog group formula. There is no Module directive. The Dialect directive must be Dialect("RIF-Rulelog"), and the Import(<loc>) directive (with one argument) can import RIF-Rulelog documents only. Here loc must be a Unicode character sequence that forms an IRI. There are no RIF-Rulelog-specific restrictions on the two-argument directive Import except that the second argument must be a Unicode sequence of characters of the form <loc>, where loc is an IRI.
Example 3 (Blocks World)
Document( Base(<http://example.com/blocksworld#>) Prefix(silk <http://vulcan.com/2008/silk#>) Prefix(dc <http://purl.org/dc/terms/>) Prefix(func <http://www.w3.org/2007/rif-builtin-function#>) Description( ![silk:tag->_mv_action dc:description->"moving blk from one square to another, if the destination square is free; the source square becomes free"] And(<loc>(func:numeric-add(?s 1) ?blk ?to) Neg <loc>(func:numeric-add(?s 1) ?blk ?from)) :- And(<move>(?s ?blk ?from ?to) <loc>(?s ?blk ?from) Naf <loc>(?s ? ?to)) ) Description( ![silk:tag->_frax1 dc:description->"frame axiom 1"] <loc>(func:numeric-add(?s 1) ?blk ?pos) :- <loc>(?s,?blk,?pos) ) Description( ![silk:tag->_frax2 dc:description->"frame axiom 2"] Neg <loc>(func:numeric-add(?s 1) ?blk ?pos) :- neg <loc>(?s ?blk ?pos) ) Description( ![silk:tag->_dloc dc:description->"each location is free, by default"] Neg <loc>(?s,?blk,?pos) ) Description( ![silk:tag->_state dc:description->"initial state"] <loc>(0,<block4>,<square7>) ) Description( ![dc:description->"no block can be in two places at once"] silk:opposes(<loc>(?s ?blk ?y) <loc>(?s ?blk ?z)) :- And(<posn>(?y) <posn>(?z) ?y != ?z) ) Description( ![dc:description->"move-action beats frame axiom 1"] silk:overrides(_mv_actn _frax1) ) Description( ![dc:description->"move-action beats frame axiom 2"] silk:overrides(_mv_actn _frax2) ) Description( ![dc:description->"move-action beats the default location"] silk:overrides(_mv_actn _dloc) ) Description( ![dc:description->"frame axiom 1 beats the default location"] silk:overrides(_frax1 _dloc) ) Description( ![dc:description->"initial state beats the default location"] silk:overrides(_state _dloc) ) Description( ![dc:description->"State 2: block4 s moved from square7 to square3"] <move>(2 <block4> <square7> <square3>) ) Description( ![dc:description->"facts about the available squares on the board"] Group( <posn>(<square1>) <posn>(<square2>) <posn>(<square3>) <posn>(<square4>) <posn>(<square5>) <posn>(<square6>) <posn>(<square7>) <posn>(<square8>) <posn>(<square9>) <posn>(<square10>) <posn>(<square11>) <posn>(<square12>) <posn>(<square13>) <posn>(<square14>) <posn>(<square15>) <posn>(<square16>) ) ) )
The example illustrates defeasible reasoning in RIF-Rulelog. Here, some rules are tagged (e.g., _mv_actn, _frax1, where the prefix _ denotes local constants, as usual in RIF). The predicate silk:overrides specifies that some rules (e.g., the ones labeled _mv_actn) defeat others (e.g., the ones labeled _frax1 and _frax2). In RIF-Rulelog, literals L and Neg L are incompatible and cannot both appear in a consistent model. The predicate silk:opposes specifies additional incompatibilities. In our example, silk:opposes says that no block can be present in two different positions on the board in the same state. The symbol ! in the position of the rule Ids is a RIF-Rulelog shortcut used to indicate that the Id is anonymous: it is generated by some algorithm and is not explicitly used in the document.
We can now see how defeasible reasoning works in RIF-Rulelog. The rule labeled _dloc is a "catch-all" low-priority default that says that all locations on the board are free. Contrary to this default, the fact labeled _state says that <block4> is at <square7> in state 0. Recall that in RIF the notation <block4> is a shorthand for IRIs in the default namespace specified in the Base directive. Therefore, in our case, this is a shorthand for "http://example.com/blocksworld#block4"^^rif:iri.
The fact tagged with _state defeats the rule rule tagged with _dloc (due to silk:overrides(_state _dloc)), so <block4> is indeed at <square7>. Other squares are free unless the "catch-all" default _dloc is overridden. Such overriding can occur due to the rule tagged with _mv_actn, which specifies the effects of the <move> action. The rule _mv_actn also defeats the frame persistence axioms, _frax1 and _frax2, which simply state that block locations persist from one state to another. Thus, in states 1 and 2 our block is still at <square7> and other squares are free. However, at state 2 a move occurs, and the rule _mv_actn derives the fact that <block4> must be at <square3> in state 3. Due to the explicit priorities specified via the predicate silk:overrides, this latter derivation defeats the derivations produced by the frame axioms and the default location fact _dloc.
The semantics of RIF-Rulelog is defined by specialization from the semantics of the RIF framework for logic dialects. Section Semantics of a RIF Dialect as a Specialization of the RIF Framework in [RIF-FLD] lists the parameters of the semantic framework that can be specialized. Thus, for RIF-Rulelog, we need to look at the following parameters:
The restrictions on the signatures of symbols, terms, or formulas in RIF-Rulelog do not affect the semantic definitions of RIF-FLD in any significant way.
The set TV of truth values in RIF-Rulelog consists of three values, t, f, and u (undefined), such that f <_{t} u <_{t} t.
The set of data types and DTS of RIF-Rulelog includes the datatypes listed in Section Datatypes of [RIF-DTB].
The semantics of the two-argument Import directive is given in [RIF-RDF+OWL]. The semantics of the one-argument directive is the same as in RIF-FLD.
Truth valuation of a rule of the form head :- body is defined as follows. This definition is a specialization of the corresponding definition in RIF-FLD for the :- connective.
TVal_{I}(head :- body) = t if and only if TVal_{I}(head) ≥_{t} TVal_{I}(body). Otherwise, TVal_{I}(head :- body) = f.
Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIF-Rulelog, this set is defined in Section Intended Models.
The well-founded semantics [GRS91,Prz94] is typically defined with respect to Herbrand domains [CL73], so we limit our attention to RIF-FLD semantic structures I = <TV, DTS, D, I_{C}, I_{V}, I_{F}, I_{NF}, I_{list}, I_{tail}, I_{frame}, I_{sub}, I_{isa}, I_{=}, I_{external}, I_{connective}, I_{truth}> that all have the same RIF-Rulelog-Herbrand domain. We say RIF-Rulelog-Herbrand domain and not simply a Herbrand domain because RIF-Rulelog has many more kinds of terms than the standard classical logic. This even includes certain formulas, such as membership, subclass, and frames. The semantics of RIF-FLD, which we are specializing here, is defined in a general way in which all such terms are mapped into the domain. Therefore, we need to define RIF-Rulelog-Herbrand domains, a generalization of the classical notion of Herbrand domains.
In what follows, we will be relying on the notions of ground terms, Herbrand Universe and Herbrand Domain, Herbrand Semantic Structure, minimal models, and other notions defined in Appendix: A Subframework for Herbrand Semantic Structures of the RIF FLD specification.
Definition (Intended Models - General).
Let Γ be a RIF-Rulelog document and Γ^{*}
be its ground instantiation. We say a RIF Herbrand semantic
multi-structure Î
of Γ is its intended model if and only
if Î is an intended model of Γ^{*}.
The remainder of this section defines the notion of intended
models of ground RIF-Rulelog documents.
☐
To define intended models for ground documents, we need to introduce the following notion of a program quotient (sometimes also called Gelfond-Lifshitz reduct). For the purpose of the next definition, we introduce three additional propositions that correspond to the three truth values of RIF-Rulelog: true, false, and undefined, such that for any RIF Herbrand semantic structure, I, TVal_{I}(true) = t, TVal_{I}(false) = f, and TVal_{I}(undefined) = u. (Note that for true we could have used And() and for false Or(). But no substitute exists in RIF-FLD for undefined.)
Definition (Quotient). Let Γ be a ground RIF-Rulelog document and Î a RIF Herbrand semantic multi-structure for it. The quotient of Γ with respect to Î, denoted Γ/ Î is a RIF-Rulelog document obtained as follows:
The resulting document is called the quotient of Γ with respect to Î and is denoted Γ/ Î.
It is easy to see that Γ/ Î does not contain atomic formulas that are negated with Naf. ☐
Observe that any quotient Γ/ Î is a Horn-like rule set in that it does not use default negation. We say Horn-like because these rules can still have explicit negation Neg. However, explicit negation behaves monotonically and this means that such rules have a unique minimal model. This model is computed by an iterative process of making all possible inferences using the rules in Γ/ Î starting with the empty RIF Herbrand semantic structure in which I_{true} maps everything to u [vEK76].
Let Γ be a ground RIF-Rulelog document and Î a RIF Herbrand semantic multi-structure. The unique minimal model of Γ/ Î will be denoted by M_{min}(Γ/ Î).
The following definition is an adaptation from [Prz94].
Definition (Well-founded Models).
The well-founded model of a ground RIF-Rulelog document, Γ, is defined as a limit of the following transfinite sequence of RIF Herbrand semantic structures I^{0}, I^{1}, ....
The initial structure, I^{0} is the
empty structure defined in Appendix: A Subframework for Herbrand Semantic Structures of the RIF FLD specification.
Suppose that I^{m} has already been defined for every m<k, where k is some ordinal number. Then:
The limit of such a sequence is known to exist [Prz94] and is unique; it is reached for some, possibly transfinite, ordinal α, such that I^{α} = I^{α+1}. ☐
Note that although the above limit exists and therefore a well-founded model is unique, it might not be consistent. Here is a simple example that illustrates that:
Group ( ex:p Neg ex:p :- Naf ex:q )
It is easy to see that the well-founded model here makes both ex:p and Neg ex;p true and therefore is inconsistent. Example 2 is another illustration of such possible inconsistency. We are now ready to define intended models for ground RIF-Rulelog documents.
Definition (Intended Models - Ground). Let Γ be a ground RIF-Rulelog document. A RIF Herbrand semantic multi-structure Î of Γ is said to be an intended model of Γ if it is a consistent Herbrand semantic multi-structure and a well-founded model for Γ/ Î. ☐
As explained just before the above definition, the intended model does not always exist, due to the consistency requirement,
Example 4 (Intended and unintended models)
Going back to Example 1, the intended model here is the one that assigns hu:person(br:barber) the truth value u and hu:person(hu:JoePublic) the truth value t. Other facts, such as hu:person(hu:Mary), are assigned the truth value f.
An example of an un-intended model would be one where hu:person(hu:Mary) is assigned t or u, as such conclusions are deemed to be unsupported. ☐
Section Mapping from the RIF-FLD Presentation Syntax to the XML Syntax of [RIF-FLD] defines a mapping, χ_{fld}, from the presentation syntax of RIF-FLD to its XML serialization. When restricted to well-formed RIF-Rulelog formulas, χ_{fld} becomes the RIF-Rulelog-to-XML mapping χ_{clpwd}. In this way, the XML serialization of RIF-Rulelog is a specialization of the RIF-FLD XML Serialization Framework defined in [RIF-FLD].
If T is a set of datatypes and symbol spaces and E a coherent set of external schemas for functions and predicates, then the general definition of conformance in RIF-FLD yields the notion of conformant RIF-Rulelog_{T,E} producers and consumers.
TBD