RIF SILK Dialect
 This version:
 $Id: RIFSILK.html 1252 20100208 15:24:25Z mdean $
 Editors:
 Jeff Sherman, Raytheon BBN Technologies, USA
 Mike Dean, Raytheon BBN Technologies, USA
This document specifies the RIF SILK Dialect, RIFSILK. The RIFSILK presentation syntax and semantics are specified as specializations of the RIF Framework for Logic Dialects (RIFFLD). The XML serialization syntax of RIFSILK is also given as a specialization of the XML syntax of RIFFLD.
This is the specification of RIFSILK, the RIF Default Logic Dialect. RIFSILK employs the paradigm of declarative logic programming that is based on the wellfounded semantics [GRS91]. RIFSILK also includes a number of other features present in more sophisticated declarative logic programming languages such as SILK [SILK].
RIFSILK is a strict superset of RIFBLD [RIFBLD], to which it adds the following features:
 Courteous rules [Gro99, WGK+09], which allow for restricted classical negation and prioritized rules.
 Two kinds of negation: Naf (default negation with wellfounded semantics) and Neg (explicit negation)
 (kary) mutexes, which are essentially integrity constraints on the knowledge base. Specifically, each such statement says that it is contradictory for a given set of literals to be inferred given an (optional) condition.
 HiLog [CKW93], which enables a high degree of metaprogramming by allowing variables to range over predicate symbols, function symbols, and even formulas.
 Externally defined actions, as in RIFPRD [RIFPRD].
 Syntax for expressing disjunction in rule bodies, conjunction in rule heads, and classical implication.
 Reification, which provides a mechanism for making objects out of a large class of formulas.
 Signatures as in FLogic [KLW95] which allow for type checking polymorphism
RIFSILK shares a number of features with other RIF dialects. These include objects and frames as in Flogic [KLW95], internationalized resource identifiers (or IRIs, defined by [RFC3987]) as identifiers for concepts, and XML Schema datatypes [XMLSCHEMA2].
The following examples illustrate the additional features of RIFSILK.
Example 1
This example states that coauthors know each other unless they have never met. It demonstrates prioritization and negation.
Document {
Prefix(foaf http://xmlns.com/foaf/0.1/)
Prefix(pub http://example.org/pub#)
Prefix(silk http://TBD/silk#)
Group {
(* r1 *) Forall ?a1 ?a2 ?paper
(?a1[foaf:knows>?a2]
: ?paper # pub:Publication[pub:author>?a1,
pub:author>?a2}])
(* r2 *) Forall ?a1 ?a2
(neg ?a1[foaf:knows>?a2]
: ?a1[hasNeverMet>?a2])
silk:overrides(r2, r1)
}
}
ADD MORE EXAMPLES
This normative section describes RIFSILK as it relates to RIFFLD [RIFFLD].
 Alphabet.
The alphabet of the RIFSILK presentation syntax is the alphabet of RIFFLD where the flowing symbols are removed:
 "Dialect"
 "Module"
 "IRIMETA"
And the following symbols are added:
 "Label" (replaces IRIMETA and is less restrictive)

Extension points.
The following connectives are added for formulas:
 Right implication (==>)
 Left implication (<==)
 Bidirectional implication (<==>)
The following connectives are added for terms:
 Unification (:=:)
 Disunification (!=)
 Assignment of signatures to each constant and variable symbol.
The signature set of RIFSILK contains the following signatures:
 Basic
 individual { }
 atomic { }
The signature individual{ } represents the context in which individual objects can appear. The signature atomic is the standard signature of RIFFLD, which represents the context where atomic formulas can occur.
 Signatures for functions, predicates, and external functions and predicates
 Predicate signature for nonexternal symbols p. This signature has the arrow expressions for positional functions and predicates: () ⇒ atomic, (individual) ⇒ atomic, (individual individual) ⇒ atomic, ..., plus the arrow expressions for predicates with named arguments: (s1>individual ... sk>individual) ⇒ atomic, for all k>0 and all s1, ..., sk ∈ ArgNames.
 External function or predicate signature efp. This signature has the following arrow expressions, where Τ can be either individual or atomic:
() ⇒ Τ, (Τ) ⇒ Τ, (Τ Τ) ⇒ Τ, ..., plus (s1>Τ ... sk>Τ) ⇒ Τ, for all k>0 and all s1, ..., sk ∈ ArgNames.
 Signatures for lists
 The signature list for closed lists. It has the following arrow expressions: () ⇒ individual, (individual) ⇒ individual, (individual individual) ⇒ individual, ...
 The signature openlist for open lists (that have tails). It has the following arrow expressions: (individual individual) ⇒ individual, (individual individual individual) ⇒ individual, ...
 The signature for equality is ={(individual individual) ⇒ atomic}.
 The signature for signature is =>{(individual individual) ⇒ atomic}.
NOTE: THE TERM 'signature' IS OVERLOADED. IS THIS OK?
 The frame signature, >, is >{(individual individual individual) ⇒ atomic}.
NOTE: WHAT SHOULD THE SIGNATURES LOOK LIKE FOR FRAMES/SIGNATURES WITH SETVALUED METHODES?
Note that this allows for the possibility that a frame term might occur as an argument to a predicate, a function, or inside some other term.
 The membership signature, #, is #{(individual individual) ⇒ atomic}.
Note that this allows for the possibility that a membership term might occur as an argument to a predicate, a function, or inside some other term.
 The signature for the subclass relationship is ##{(individual individual) ⇒ atomic}.
As with frames and membership terms, this allows for the possibility that a subclass term might occur inside some other term.
 Assignment of signatures to symbols:
 Nondatatype symbols in Const, including the rif:iri and rif:local:
 Either have the signatures individual, atomic, and p.
 Or the signature efp.
 Thus, a symbol can represent either an external function or predicate, or it is a regular symbol. In the latter case, it can appear in the position of an individual, a function, or a predicate without any restrictions.
 Symbols that correspond to RIF datatypes (XML Schema datatypes, rdf:XMLLiteral, rdf:PlainLiteral, etc.) all have the signature individual in RIFSILK.
 All variables have the signature individual, so they can range only over individuals.
 NOTE (MK) NEED TO ADD SIGNATURES FOR MUTEXES.
 Supported types of terms.

RIFSILK supports the following types of terms defined by the syntactic framework (see the Section Terms of [RIFFLD]):
 constants
 variables
 positional
 with named arguments
 closed lists
 open lists
 equality
 frame
 membership
 subclass
 external
 formula
 aggregate

Additionally RIFSILK supports the following terms whose signatures are defined in section 2.3 of this document.
 signatures
 mutex

Required symbol spaces.
RIFSILK requires the symbol spaces defined in Section Constants, Symbol Spaces, and Datatypes of [RIFDTB].

Supported formulas.
RIFSILK supports the types of formulas described in Section Wellformed Terms and Formulas of [RIFFLD] with the following exceptions:
The semantics of the RIF Default Logic Dialect will be 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 [RIFFLD] lists the parameters of the semantic framework that can be specialized.
TBD, with significant help from Benjamin Grosof and Michael Kifer
See also [WGK+09].
Section Mapping from the RIFFLD Presentation Syntax to the XML Syntax of [RIFFLD] defines a mapping, X_{fld}, from the presentation syntax of RIFFLD to its XML serialization. What follows are additional RIFSILK specific mappings not present in RIFFLD:
Presentation Syntax
 XML Syntax

Mutex(
And (
conjunct_{1}
. . .
conjunct_{n}
) (
body?
)
)

<Mutex>
<And>
<formula>χ_{silk}(conjunct_{1})</formula>
. . .
<formula>χ_{silk}(conjunct_{n})</formula>
</And>
<formula>χ_{silk}(body)</formula>
</Mutex>

RIFSILK does not require or expect conformant systems to implement the RIFSILK presentation syntax. Instead, conformance is described in terms of semanticspreserving transformations between the native syntax of a compliant system and the XML syntax of RIFSILK.
Let Τ be a set of datatypes and symbol spaces that includes the datatypes specified in
[RIFDTB], and the symbol spaces rif:iri, and rif:local. Suppose Ε is a coherent set of external schemas that includes the builtins listed in [RIFDTB]. We say that a formula φ is a SILK_{Τ,Ε} formula iff

it is a wellformed RIFSILK formula,

all datatypes and symbol spaces used in φ are in Τ, and

all externally defined terms used in φ are instantiations of external schemas from Ε.
A RIF processor is a conformant DLC_{Τ,Ε} consumer iff it implements a semanticspreserving mapping, μ, from the set of all SILK_{Τ,Ε} formulas to the language L of the processor (μ does not need to be an "onto" mapping).
Formally, this means that for any pair φ, ψ of SILK_{Τ,Ε} formulas for which φ =_{SILK} ψ is defined, φ =_{SILK} ψ iff μ(φ) =_{L} μ(ψ). Here =_{SILK} denotes the logical entailment in RIFSILK and =_{L} is the logical entailment in the language L of the RIF processor.
A RIF processor is a conformant SILK_{Τ,Ε} producer iff it implements a semanticspreserving mapping, ν, from the language L of the processor to the set of all SILK_{Τ,Ε} formulas (ν does not need to be an "onto" mapping).
Formally, this means that for any pair φ, ψ of formulas in L for which φ =_{L} ψ is defined, φ =_{L} ψ iff ν(φ) =_{SILK} ν(ψ).
An admissible document is one which conforms to all the syntactic constraints of RIFSILK, including ones that cannot be checked by an XML Schema validator (cf. Definition Admissible RIFSILK document in XML syntax).
The above definitions are specializations to RIFSILK of the general conformance clauses defined in the RIF framework for logic dialects [RIFFLD]. The following clauses are further restrictions that are specific to RIFSILK.
TBD
 [RFC3987]

RFC 3987  Internationalized Resource Identifiers (IRIs), M. Duerst and M. Suignard, IETF, January 2005. This document is http://www.ietf.org/rfc/rfc3987.txt.
 [RIFBLD]

RIF Basic Logic Dialect Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CRrifbld20091001/. Latest version available at http://www.w3.org/TR/rifbld/.
 [RIFCore]

RIF Core Dialect Harold Boley, Gary Hallmark, Michael Kifer, Adrian Paschke, Axel Polleres, Dave Reynolds, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CRrifcore20091001/. Latest version available at http://www.w3.org/TR/rifcore/.
 [RIFDTB]
 RIF Datatypes and BuiltIns 1.0 Axel Polleres, Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CRrifdtb20091001/. Latest version available at http://www.w3.org/TR/rifdtb/.
 [RIFFLD]

RIF Framework for Logic Dialects Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CRriffld20091001/. Latest version available at http://www.w3.org/TR/riffld/.
 [RIFPRD]

RIF Production Rule Dialect Christian de Sainte Marie, Adrian Paschke, Gary Hallmark, eds. W3C Candidate Recommendation, 1 October 2009. Latest version available at http://www.w3.org/TR/rifprd/.
 [RIFRDF+OWL]

RIF RDF and OWL Compatibility Jos de Bruijn, editor. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CRrifrdfowl20091001/. Latest version available at http://www.w3.org/TR/rifrdfowl/.
 [XML1.0]

Extensible Markup Language (XML) 1.0 (Fourth Edition), W3C Recommendation, World Wide Web Consortium, 16 August 2006, edited in place 29 September 2006. This version is http://www.w3.org/TR/2006/RECxml20060816/.
 [XML Schema Datatypes]

W3C XML Schema Definition Language (XSD) 1.1 Part 2: Datatypes. David Peterson, Shudi Gao, Ashok Malhotra, C. M. SperbergMcQueen, and Henry S. Thompson, eds. W3C Candidate Recommendation, 30 April 2009, http://www.w3.org/TR/2009/CRxmlschema11220090430/. Latest version available as http://www.w3.org/TR/xmlschema112/.
 [CKW93]

HiLog: A Foundation for HigherOrder Logic Programming, W. Chen, M. Kifer and D.S. Warren. Journal of Logic Programming, 15:3, pages 187230, February 1993.
 [CURIE]

CURIE Syntax 1.0: A syntax for expressing Compact URIs, Mark Birbeck, Shane McCarron. W3C Working Draft 2 April 2008. Available at http://www.w3.org/TR/curie/.
 [Gro99]

A Courteous Compiler from Generalized Courteous Logic Programs to Ordinary Logic Programs, Benjamin N. Grosof. Technical Report RC 21472, IBM, July 1999.
 [GRS91]

The WellFounded Semantics for General Logic Programs, A. Van Gelder, K.A. Ross, J.S. Schlipf. Journal of ACM, 38:3, pages 620650, 1991.
 [KLW95]

Logical foundations of objectoriented and framebased languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July 1995, pages 741843.
 [RIFUCR]

RIF Use Cases and Requirements, Adrian Paschke, David Hirtle, Allen Ginsberg, PaulaLavinia Patranjan, Frank McCabe, eds. W3C Working Draft, 18 December 2008, http://www.w3.org/TR/2008/WDrifucr20081218/. Latest version available at http://www.w3.org/TR/rifucr/.
 [SILK]

The SILK Language, Benjamin Grosof, Michael Kifer, Mike Dean. Vulcan Inc., 2009.
 [WGK+09]

Logic Programming with Defaults and Argumentation Theories, Hui Wan, Benjamin Grosof, Michael Kifer, Paul Fodor, Senlin Liang. Proc. 25th International Conference on Logic Programming (ICLP 2009), Pasadena, California, July 2009. Available at http://www.cs.sunysb.edu/~kifer/TechReports/LPDA09.pdf.