W3C

RIF SILK Dialect

This version:
$Id: RIF-SILK.html 1252 2010-02-08 15:24:25Z mdean $
Editors:
Jeff Sherman, Raytheon BBN Technologies, USA
Mike Dean, Raytheon BBN Technologies, USA

Abstract

This document specifies the RIF SILK Dialect, RIF-SILK. The RIF-SILK presentation syntax and semantics are specified as specializations of the RIF Framework for Logic Dialects (RIF-FLD). The XML serialization syntax of RIF-SILK is also given as a specialization of the XML syntax of RIF-FLD.

Table of Contents

1 Overview

This is the specification of RIF-SILK, the RIF Default Logic Dialect. RIF-SILK employs the paradigm of declarative logic programming that is based on the well-founded semantics [GRS91]. RIF-SILK also includes a number of other features present in more sophisticated declarative logic programming languages such as SILK [SILK].

RIF-SILK is a strict superset of RIF-BLD [RIF-BLD], to which it adds the following features:

RIF-SILK shares a number of features with other RIF dialects. These include objects and frames as in F-logic [KLW95], internationalized resource identifiers (or IRIs, defined by [RFC-3987]) as identifiers for concepts, and XML Schema datatypes [XML-SCHEMA2].

The following examples illustrate the additional features of RIF-SILK.

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

2 RIF-SILK and its relationship to the RIF Framework for Logic Dialects

This normative section describes RIF-SILK as it relates to RIF-FLD [RIF-FLD].

  1. Alphabet.

    The alphabet of the RIF-SILK presentation syntax is the alphabet of RIF-FLD where the flowing symbols are removed:

    And the following symbols are added:

  2. Extension points.

    The following connectives are added for formulas:

    The following connectives are added for terms:

  3. Assignment of signatures to each constant and variable symbol.

    The signature set of RIF-SILK contains the following signatures:

    1. Basic
      • individual { }
      • atomic { }

      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.

    2. Signatures for functions, predicates, and external functions and predicates
      • Predicate signature for non-external 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, ..., skArgNames.
      • 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, ..., skArgNames.
    3. 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, ...
    4. The signature for equality is ={(individual individual) ⇒ atomic}.
    5. The signature for signature is =>{(individual individual) ⇒ atomic}.

      NOTE: THE TERM 'signature' IS OVERLOADED. IS THIS OK?

    6. The frame signature, ->, is ->{(individual individual individual) ⇒ atomic}.

      NOTE: WHAT SHOULD THE SIGNATURES LOOK LIKE FOR FRAMES/SIGNATURES WITH SET-VALUED 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.

    7. 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.

    8. 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.

    9. Assignment of signatures to symbols:
      • Non-datatype 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 RIF-SILK.
        • All variables have the signature individual, so they can range only over individuals.
    10. NOTE (MK) NEED TO ADD SIGNATURES FOR MUTEXES.
  4. Supported types of terms.

  5. Required symbol spaces.

    RIF-SILK requires the symbol spaces defined in Section Constants, Symbol Spaces, and Datatypes of [RIF-DTB].

  6. Supported formulas.

    RIF-SILK supports the types of formulas described in Section Well-formed Terms and Formulas of [RIF-FLD] with the following exceptions:

3 The Semantics of RIF-SILK as a Specialization of RIF-FLD

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 [RIF-FLD] 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].

4 The XML Serialization of RIF-SILK as a Specialization of RIF-FLD

Section Mapping from the RIF-FLD Presentation Syntax to the XML Syntax of [RIF-FLD] defines a mapping, Xfld, from the presentation syntax of RIF-FLD to its XML serialization. What follows are additional RIF-SILK specific mappings not present in RIF-FLD:

Presentation Syntax XML Syntax
Mutex(
  And (
    conjunct1
    . . .
    conjunctn
   )  (
        body?  
      )
)
<Mutex>
  <And>
    <formula>χsilk(conjunct1)</formula>
    . . .
    <formula>χsilk(conjunctn)</formula>
  </And>
  <formula>χsilk(body)</formula>
</Mutex>


5 RIF-SILK Conformance as a Specialization of RIF-FLD

RIF-SILK does not require or expect conformant systems to implement the RIF-SILK presentation syntax. Instead, conformance is described in terms of semantics-preserving transformations between the native syntax of a compliant system and the XML syntax of RIF-SILK.

Let Τ be a set of datatypes and symbol spaces that includes the datatypes specified in [RIF-DTB], and the symbol spaces rif:iri, and rif:local. Suppose Ε is a coherent set of external schemas that includes the built-ins listed in [RIF-DTB]. We say that a formula φ is a SILKΤ,Ε formula iff

A RIF processor is a conformant DLCΤ,Ε consumer iff it implements a semantics-preserving 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 RIF-SILK 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 semantics-preserving 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 RIF-SILK, including ones that cannot be checked by an XML Schema validator (cf. Definition Admissible RIF-SILK document in XML syntax).

The above definitions are specializations to RIF-SILK of the general conformance clauses defined in the RIF framework for logic dialects [RIF-FLD]. The following clauses are further restrictions that are specific to RIF-SILK.

6 Acknowledgements

TBD

7 References

7.1 Normative References

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

[RIF-BLD]
RIF Basic Logic Dialect Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-bld-20091001/. Latest version available at http://www.w3.org/TR/rif-bld/.

[RIF-Core]
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/CR-rif-core-20091001/. Latest version available at http://www.w3.org/TR/rif-core/.

[RIF-DTB]
RIF Datatypes and Built-Ins 1.0 Axel Polleres, Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-dtb-20091001/. Latest version available at http://www.w3.org/TR/rif-dtb/.

[RIF-FLD]
RIF Framework for Logic Dialects Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-fld-20091001/. Latest version available at http://www.w3.org/TR/rif-fld/.

[RIF-PRD]
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/rif-prd/.

[RIF-RDF+OWL]
RIF RDF and OWL Compatibility Jos de Bruijn, editor. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-rdf-owl-20091001/. Latest version available at http://www.w3.org/TR/rif-rdf-owl/.

[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/REC-xml-20060816/.

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

7.2 Informational References

[CKW93]
HiLog: A Foundation for Higher-Order Logic Programming, W. Chen, M. Kifer and D.S. Warren. Journal of Logic Programming, 15:3, pages 187-230, 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 Well-Founded Semantics for General Logic Programs, A. Van Gelder, K.A. Ross, J.S. Schlipf. Journal of ACM, 38:3, pages 620-650, 1991.

[KLW95]
Logical foundations of object-oriented and frame-based languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July 1995, pages 741--843.

[RIF-UCR]
RIF Use Cases and Requirements, Adrian Paschke, David Hirtle, Allen Ginsberg, Paula-Lavinia Patranjan, Frank McCabe, eds. W3C Working Draft, 18 December 2008, http://www.w3.org/TR/2008/WD-rif-ucr-20081218/. Latest version available at http://www.w3.org/TR/rif-ucr/.

[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.