W3C W3C Member Submission

A Proposal for a SWRL Extension towards First-Order Logic

W3C Member Submission 11 April 2005

This version:
http://www.w3.org/submissions/2005/SUBM-SWRL-FOL-20050411/
Latest version:
http://www.w3.org/submissions/SWRL-FOL/
Author:
Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies

Abstract

This is a description of a proposed extension of SWRL to function-free handle unary/binary first-order logic. This is intended to be a minimal extension that fits well with SWRL, OWL, and RDF. Transformation-based techniques to handle functions and n-ary predicates are suggested in an appendix.

Status of this document

This is a member submission, offered by the National Research Council of Canada, Network Inference and Stanford University, on behalf of themselves and the authors, in association with the Joint US/EU ad hoc Agent Markup Language Committee (Joint Committee).

The W3C Team Comment discusses this submission in the context of W3C activities. Public comment on this document is invited on the mailing list www-rdf-rules@w3.org (public archive). Announcements and current information may also be available on the DAML Rules page.

By publishing this document, W3C acknowledges that the National Research Council of Canada, Network Inference and Stanford University have made a formal submission to W3C for discussion. Publication of this document by W3C indicates no endorsement of its content by W3C, nor that W3C has, is, or will be allocating any resources to the issues addressed by it. This document is not the product of a chartered W3C group, but is published as potential input to the W3C Process. Publication of acknowledged Member Submissions at the W3C site is one of the benefits of W3C Membership. Please consult the requirements associated with Member Submissions of section 3.3 of the W3C Patent Policy. Please consult the complete list of acknowledged W3C Member Submissions.


Table of contents


1. Introduction

This document contains a proposal for an extension to the SWRL extension of OWL [SWRL]. This proposal extends the set of OWL axioms to include an axiom for arbitrary function-free first-order formula over unary and binary predicates, interpreted in the usual manner. A high-level abstract syntax is provided that extends the OWL abstract syntax described in the OWL Semantics and Abstract Syntax document [OWL S&AS]. An extension of the SWRL and OWL model-theoretic semantics is also given to provide a formal meaning for OWL ontologies including formulae written in this abstract syntax.

2. Abstract Syntax

The syntax for OWL Rules in this section abstracts from any exchange syntax for OWL and SWRL and thus facilitates access to and evaluation of the language. This syntax extends the abstract syntax of SWRL which itself extends the abstract syntax of OWL.

The abstract syntax is specified here by means of a version of Extended BNF, very similar to the EBNF notation used for XML [XML]. Terminals are quoted; non-terminals are bold and not quoted. Alternatives are either separated by vertical bars (|) or are given in different productions. Components that can occur at most once are enclosed in square brackets ([…]); components that can occur any number of times (including zero) are enclosed in braces ({…}). Whitespace is ignored in the productions here.

Names in the abstract syntax are RDF URI references [RDF Concepts]. These names may be abbreviated into qualified names, using one of the following namespace names:

PrefixNamespace
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
rdfshttp://www.w3.org/2000/01/rdf-schema#
xsdhttp://www.w3.org/2001/XMLSchema#
owlhttp://www.w3.org/2002/07/owl#

The intended meaning of most constructs in this abstract syntax are just what one would expect, treating them as a first-order formula, with a few exceptions, noted below. The formal meaning of assertions is given in Section 3 via an extension of the OWL DL model-theoretic semantics [OWL S&AS].

2.1. Assertions

A SWRL ontology in the abstract syntax contains a sequence of axioms and facts, including SWRL rules. It is proposed to extend this with assertion axioms that contain first-order sentences.

axiom ::= assertion 

Assertions can be tagged with a URI reference, which only serves to provide an identifier for the assertion, and has no semantic consequence. Assertions can also have OWL-style annotations, which also do not have any semantic consequences in the model-theoretic semantics here. Assertions assert first-order sentences, i.e., formulae with no free variables. Because variables are bound using typed quantifiers, this means that every variable in an assertion must range over a given type.

assertion ::= 'Assertion(' [ URIreference ] { annotation } foformula { foformula } ')'

The formulae in assertions are set up in the usual fashion for first-order formulae, with some extensions, such as allowing conjunctions and disjunctions to have any number of conjuncts or disjuncts. Atomic formulae are precisely the same as atoms in SWRL.

foformula ::= atom
	    | 'and(' { foformula } ')'
	    | 'or(' { foformula } ')'
	    | 'neg(' foformula ')'
	    | 'implies(' foformula foformula ')'
	    | 'equivalent(' foformula foformula ')'
	    | 'forall(' variable { variable } foformula ')'
	    | 'exists(' variable { variable } foformula ')'

The introduction of variables in forall and exists constructs provides a type for the variable that restricts the possible mappings for that variable.

variable ::= 'I-variable(' URIreference description ')'
	   | 'D-variable(' URIreference dataRange ')'

3. Model-Theoretic Semantics

The model-theoretic semantics for OWL rules is a straightforward extension of the semantics for OWL DL given in the OWL Semantic and Abstract Syntax document [OWL S&AS]. The basic idea is that we define bindings, extensions of OWL interpretations that also map variables to elements of the domain. The semantic conditions relating to axioms and ontologies are unchanged, e.g., an interpretation satisfies an ontology iff it satisfies every axiom (including rules) and fact in the ontology.

The semantics thus obtained is a fairly standard first-order-logic semantics. The only significant tweak is the semantic separation of literals, datatyped and untyped, from other entities. The logic obtained is thus a two-sorted logic where one sort (the literal sort) has built-in predicates (the datatype predicates and the other built-ins).

3.1. Interpreting Assertions

Assertions are interpreted using bindings from SWRL. Recall that a binding B(I), where I is an abstract OWL interpretation, extends I such that S maps i-variables to elements of EC(owl:thing) and L maps d-variables to elements LV. A formula is satisfied by a binding (written B(I) ⇒ F) under the conditions given in Interpretation Conditions Table.

Interpretation Conditions Table
AtomCondition on Interpretation
and(C1 ... Cn) B(I) ⇒ Ci, for each Ci
or(C1 ... Cn) B(I) ⇒ Ci, for some Ci
neg(C) B(I) does not satisfy C
implies(C1 C2) B(I) ⇒ or( neg(C1) C2 )
equivalent(C1 C2) B(I) ⇒ and( implies(C1 C2) implies(C2 C1) )
forall(V1 ... Vn C) B'(I) ⇒ C, for all bindings B' that are the same as B except for V1 ... Vn
exists(V1 ... Vn C) B'(I) ⇒ C, for some binding B' that is the same as B except for V1 ... Vn

Binding B' is the same as another binding B except for V1 ... Vn if B' maps i-variables and d-variables the same as B does for all variables other than V1 ... Vn. For Vi of the form I-variable(U D) and for Vi of the form D-variable(U D) B' must map U to an element of the extension of D. Note that this means that repeated variables are constrained to belong to the intersection of their types.

Atoms are satisfied in a binding using the same conditions as for SWRL. An assertion is satisfied in an interpretation if there is some binding extending the interpretation that satisfies all the top-level formulae in the assertion.

The semantic conditions relating to axioms and ontologies are again unchanged. In particular, an interpretation satisfies an ontology iff it satisfies every axiom (including rules) and fact in the ontology; an ontology is consistent iff it is satisfied by at least one interpretation; an ontology O2 is entailed by an ontology O1 iff every interpretation that satisfies O1 also satisfies O2.

4. XML Concrete Syntax

The following XML concrete syntax closely follows the XML concrete syntax for First-Order-Logic RuleML [FOL Rule ML], where a DTD for first-order logic is provided. This syntax is an extension of the XML syntax for OWL, so assertions are just another kind of element that can occur in ontologies. The details of extending the XML syntax for OWL are under discussion.

The XML Schema is available as a separate document.

<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema"
	    xmlns:owl="http://www.w3.org/2003/05/owl-xml"
	    xmlns:swrlx="http://www.w3.org/2003/11/swrlx"
	    xmlns:ruleml="http://www.w3.org/2003/11/ruleml"
	    xmlns:owlf="http://www.daml.org/2004/11/fol/fol"
	    targetNamespace="http://www.daml.org/2004/11/fol/fol"
	    elementFormDefault="qualified"
	    attributeFormDefault="qualified">

<xsd:import namespace="http://www.w3.org/2003/05/owl-xml"
            schemaLocation="owlx/schema/owl1-dl.xsd" />

<xsd:import namespace="http://www.w3.org/2003/11/ruleml"
            schemaLocation="ruleml.xsd" />

<xsd:import namespace="http://www.w3.org/2003/11/swrlx"
            schemaLocation="swrlx.xsd" />

<xsd:element name="Ontology"> 
  <xsd:annotation>
    <xsd:documentation>
      This is the root element of SWRL FOL documents 
      in the XML Concrete Syntax.  It extends swrlx:Ontology
    </xsd:documentation>
  </xsd:annotation>
  <xsd:complexType> 
    <xsd:sequence>
      <xsd:sequence minOccurs="0" maxOccurs="unbounded">
        <xsd:choice>
          <!-- Header elements --> 
          <xsd:element ref="owlx:VersionInfo" />
          <xsd:element ref="owlx:PriorVersion"  />
          <xsd:element ref="owlx:BackwardCompatibleWith" />
          <xsd:element ref="owlx:IncompatibleWith" />
          <xsd:element ref="owlx:Imports" />
          <xsd:element ref="owlx:Annotation" />

          <!-- Class elements --> 
          <xsd:element ref="owlx:Class" />
          <xsd:group   ref="owlx:classElements" />
  
          <!-- Property elements --> 
          <xsd:element ref="owlx:DatatypeProperty" />
          <xsd:element ref="owlx:ObjectProperty" />
          <xsd:element ref="owlx:SubPropertyOf" />
          <xsd:element ref="owlx:EquivalentProperties" /> 
   
          <!-- Instances --> 
          <xsd:element ref="owlx:Individual" />
          <xsd:element ref="owlx:SameIndividual" />
          <xsd:element ref="owlx:DifferentIndividuals" />

          <!-- SWRL extensions -->
          <xsd:element ref="ruleml:imp" />
          <xsd:element ref="ruleml:var" />

          <!-- FOL extension -->
          <xsd:element ref="Assertion" />
        </xsd:choice>
      </xsd:sequence>
    </xsd:sequence>
    <xsd:attribute ref="owlx:name" />
  </xsd:complexType>
</xsd:element>

<xsd:complexType name="formulae">
  <xsd:sequence minOccurs="0" maxOccurs="unbounded">
    <xsd:group name="owlf:formula" />
  </xsd:sequence>
</xsd:complexType>

<xsd:complexType name="twoformulae">
  <xsd:sequence minOccurs="2" maxOccurs="2">
    <xsd:group name="owlf:formula" />
  </xsd:sequence>
</xsd:complexType>

<xsd:group name="formula">
  <xsd:choice>
    <xsd:element name="And" type="owlf:formulae" minOccurs="1" maxOccurs="1" />
    <xsd:element name="Or" type="owlf:formulae" minOccurs="1" maxOccurs="1" />
    <xsd:element name="Neg" type="owlf:formula" minOccurs="1" maxOccurs="1" />
    <xsd:element name="Implies" type="owlf:twoformulae" minOccurs="1" maxOccurs="1" />
    <xsd:element name="Equivalent" type="owlf:twoformulae" minOccurs="1" maxOccurs="1" />
    <xsd:element name="Forall" type="owlf:quantifiedformula" minOccurs="1" maxOccurs="1" />
    <xsd:element name="Exists" type="owlf:quantifiedformula" minOccurs="1" maxOccurs="1" />
    <xsd:group ref="swrlx:atom" />
  </xsd:choice>
</xsd:group>

<xsd:complexType name="quantifiedformula">
  <xsd:sequence>
    <xsd:element name="ruleml:Var" type="ruleml:var" minOccurs="1" maxOccurs="unbounded" />
    <xsd:group name="formula" minOccurs="1" maxOccurs="1" />
  </xsd:sequence>
</xsd:complexType>

<xsd:element name="Assertion">
  <xsd:complexType>
    <xsd:complexContent>
      <xsd:extension base="owlx:annotated">
        <xsd:sequence minOccurs="1" maxOccurs="unbounded">
	  <xsd:group ref="owlf:formula" />
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="optional" />
      </xsd:extension>
    </xsd:complexContent>
  </xsd:complexType>
</xsd:element>

</xsd:schema>

5. Example Assertion in XML Concrete Syntax

Here is an example of a simple, nonsensical assertion in XML Concrete Syntax.

<Assertion owlx:name="Example">
  <owlx:Annotation>
    <owlx:Label>Example Rule for Expository Purposes</owlx:Label>
  </owlx:Annotation>
    <Forall>
      <ruleml:Var type="Person">x1</ruleml:Var>
      <ruleml:Var type="Parent">x2</ruleml:Var>
      <ruleml:Var type="Person">x3</ruleml:Var>
      <ruleml:Var type="xsd:int">x4</ruleml:Var>
      <And>
	<swrlx:individualPropertyAtom  swrlx:property="hasParent"> 
          <ruleml:Var>x1</ruleml:Var>
          <ruleml:Var>x2</ruleml:Var>
        </swrlx:individualPropertyAtom> 
        <swrlx:individualPropertyAtom  swrlx:property="hasBrother"> 
          <ruleml:Var>x2</ruleml:Var>
          <ruleml:Var>x3</ruleml:Var>
        </swrlx:individualPropertyAtom> 
        <swrlx:datatypePropertyAtom  swrlx:property="hasAge"> 
          <ruleml:Var>x2</ruleml:Var>
          <ruleml:Var>x4</ruleml:Var>
        </swrlx:datatypePropertyAtom> 
      </And>
    </Forall>
</Assertion>

Note that the distinction between i-variables and d-variables does not show up in this concrete syntax. However, it can be easily recovered from the variable bindings, by determining whether the binding type is an OWL description or datatype.

Appendix A. Functions and Arbitrary Arity for Predicates

A.1 Abstract Syntax

Neither predicates with arbitrary arity nor functions fit into the RDF or OWL paradigm and thus do not immediately fit into SWRL FOL. However, (almost all of) the effect of both predicates with arbitrary arity and functions can be captured via simple transformations. These transformations, in effect, reify the predication or functional relationship (e.g., a book-selling relationship between a bookstore, a customer, and a book) by requiring an individual that represents the predication or functional relationship (e.g., an instance of the book-selling class) and having role values of this individual being the participants in the predication or functional relationship. These transformations mirror the W3C Semantic Web Best Practices and Deployment Working Group note on n-ary relations [N-ary].

This method works best with named arguments, and thus the syntax uses named arguments. The syntax for n-ary predicates is as follows:

atom ::= description '(' {named-argument} ')'
named-argument ::= individualvaluedPropertyID '=' i-object
                 | datavaluedPropertyID '=' d-object

The meaning of this construct is defined by a translation, as follows:
D( s1=x1 s2=x2 ... sn=xn ) is translated to exists( I-variable(a D) s1(a x1) s2(a x2) ... sn(a xn) ).

There is no requirement that each argument of the predicate is mentioned or mentioned at most once. Neither is there a requirement that the underlying binary relationships are functional, although OWL itself is sufficiently adequate to state functionality of the relationships. Such unusual predication constructs and relationships are simply given meaning by the above translation, which provides a reasonably-intuitive meaning.

Functions are also not part of RDF or OWL. They can be added here by a similar, but slightly more complex, translation process.

The syntax for functions is:

i-object ::= description'(' {named-argument} ')'
d-object ::= builtinID'(' {d-object} ')'

The translation transforms an atom that contains a functional i-object, ...f( s1=x1 s2=x2 ... sm=xm )... into exists( I-variable(x) and( ...I-variable(x)... f( rdf:value=x s1=x1 s2=x2 ... sn=xn ) ) ) where x is a URIreference that does not appear in the atom.

The translation transforms an atom that contains a functional d-object, ... b( x1 x2 ... xm ) ... into exists( D-variable(x) and( ...D-variable(x)... f( x x1 x2 ... xn ) ) ) where x is a URIreference that does not appear in the atom.

A.2 Example

Here is a simple example of a formula that uses an n-ary relationship, namely the purchase relationship from the note on n-ary relations [N-ary].

forall( I-variable(x ex:FantasyNovel)
      Purchase(buyer=ex:peter seller=ex:amazon object=x quantity="1"^^xsd:int))

Note that Purchase has five ``arguments''. This formula does not mention the purpose argument, and thus places no restrictions on either the existence or identity of values for this argument. Note also that there is no functionality restriction on object in the note, and thus the above formula is satisfied by an single purchase of all fantasy novels or individual purchases of each fantasy novel, or, indeed any set of purchases that together cover all fantasy novels. This example uses a quantity argument, which is not in the initial example, but this does not provide any problems here.

A.3 XML Syntax

The XML syntax for SWRL FOL can be extended to encompass these constructs, using the method for slotted arguments in [FOL Rule ML]. Here is the XML Syntax in Slotted FOL RuleML for the previous example:

<Forall>
  <Var type="ex:FantasyNovel">x</Var>
  <Atom>
    <Rel>Purchase</Rel>
    <slot>
      <Ind>buyer</Ind>
      <Ind wref="ex:peter"/>
    </slot>
    <slot>
      <Ind>seller</Ind>
      <Ind wref="ex:amazon"/>
    </slot>
    <slot>
      <Ind>object</Ind>
      <Var>x</Var>
    </slot>
    <slot>
      <Ind>quantity</Ind>
      <Ind type="xsd:int">1</Ind>
    </slot>
  </Atom>
</Forall>

A.4 SWRL

The above syntax can also be used to provide n-ary relationships and functions for SWRL itself. Because SWRL does not have explicit quantifiers the above syntactic transformations cannot be used directly, and the meaning of the constructs may have to be specified via a semantic constraint.

Issues

Naming of constructs
Surprisingly, names of constructs can be quite contentious. The current names are designed to be consistent with those from RuleML and thus are close to those from the logic programming community. The most contentious of the names here is the name for "classical" negation, which is neg as in logic programming, and not not.

See also the issues list in First-Order-Logic RuleML [FOL RuleML].

References

[OWL S&AS]
OWL Web Ontology Language Semantics and Abstract Syntax. Peter F. Patel-Schneider, Pat Hayes and Ian Horrocks, eds. W3C Recommendation 10 February 2004. Latest version is available at http://www.w3.org/TR/owl-semantics/.
[SWRL]
SWRL: A Semantic Web Rule Language Combining OWL and RuleML. Ian Horrocks, Peter F. Patel-Schneider, Harold Boley, Said Tabet, Benjamin Grosof, and Mike Dean. W3C Member Submission 21 May 2004. Latest version is available at http://www.w3.org/submissions/SWRL/.
[OWL XML]
OWL Web Ontology Language XML Presentation Syntax. Masahiro Hori, Jérôme Euzenat, and Peter F. Patel-Schneider. W3C Note 11 June 2003. Latest version is available at http://www.w3.org/TR/owl-xmlsyntax/.
[RDF Concepts]
Resource Description Framework (RDF) Concepts and Abstract Syntax. Graham Klyne, Jeremy J. Carroll, and Brian McBride, eds. W3C Recommendation 10 February 2004. Latest version is available at http://www.w3.org/TR/rdf-concepts/.
[FOL RuleML]
FOL RuleML: First-Order Logic RuleML Language. Harold Boley, Mike Dean, Benjamin Grosof, Michael Sintek, Bruce Spencer, Said Tabel, and Gerd Wagner. W3C Member Submission 25 January 2005. Latest version is available at http://www.w3.org/submissions/FOL-RuleML/.
[N-ary]
Defining N-ary Relations on the Semantic Web: Use With Individuals. Natasha Noy and Alan Rector, eds. W3C Working Draft 21 July 2004. Latest version is available at http://www.w3.org/TR/swbp-n-aryRelations/.
[XML]
Extensible Markup Language (XML) 1.0 (Third Edition). Tim Bray, Jean Paoli, C. M. Sperberg-McQueen, Eve Maler, and Francois Yergeau, eds. W3C Recommendation 04 February 2004. Latest version is available at http://www.w3.org/TR/REC-xml/.