Re: Joint Committee telecon tomorrow 22 June

From: Peter F. Patel-Schneider ([email protected])
Date: 06/23/04

  • Next message: Boley, Harold: "RE: XML syntax for SWRL"
    An HTML version of my proposal is now available at
    and also attached.
    This version has a worked-out semantic section and an example formula in
    XML syntax.
    A Proposal for a SWRL Extension to First-Order Logic

    A Proposal for a SWRL Extension
    to First-Order Logic

    Draft Version of 23 June 2004

    This version:
    Latest version:
    Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies


    This is a description of a proposed extension of SWRL to handle unary/binary first-order logic. This is intended to be a minimal extension that fits well with SWRL, OWL, and RDF.

    Status of this document

    This is a Proposal produced 23 June 2004 for consideration by the Joint Committee of the DARPA DAML Program.

    Comments on this document are invited and should be sent to the author at [email protected] and discussed on the mailing list of the Joint Committee ([email protected]).

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

    A full version of this proposal will contain an XML concrete syntax similar to the XML concrete syntax for SWRL which is in turn based on the XML concrete syntax for OWL [OWL XML]. Currently there is only an example of a formula in this syntax.

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

    Namespace nameNamespace

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

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

    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 are also do not have any semantic consequences in the model-theoretic semantics here.

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

    Formulae 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 } ')'
    	    | 'not(' foformula ')'
    	    | 'implies(' foformula foformula ')'
    	    | 'equivalent(' foformula foformula ')'
    	    | 'forall(' { variable } foformula ')'
    	    | 'exists(' { variable } foformula ')'

    Variables are bound using a syntax very similar to mentions of variables in SWRL, but there is also the possibility of providing typing for variables when they are bound, as is often allowed in first-order syntaxes. The typing allowed for I-variables is, of course, an OWL description and the typing allowed for D-variables is an OWL datarange.

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

    For better compatability with RDF b-nodes, variables that occur free in assertions are treated as if they were existentially quantified.

    2.2. Arbitrary Arity for Predictaes

    It would not be hard to allow for predicates with mixed arity, by extending SWRL atoms as follows:

    atom ::= URIreference '(' { object } ')'
    object ::= i-object | d-object

    The development of this extension is not considered further here.

    3. Direct Model-Theoretic Semantics

    The model-theoretic semantics for OWL rules is a straightforward extension of the semantics for OWL given in [OWL S&AS]. The basic idea is that we define bindings, extensions of OWL interpretations that also map variables to elements of the domain. A rule is satisfied by an interpretation iff every binding that satisfies the antecedent also satisfies the consequent. 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.

    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. An 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
    not(C) B(I) does not satisfiy C
    implies(C1 C2) B(I) ⇒ or( not(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
    forall(V1 ... Vn C) B'(I) ⇒ C, for some binding B' that is the same as B except for V1 ... Vn

    One binding B' is the same as another B except for V1 ... Vn if it maps i-variables and d-variables the same as B does, except for those variables in V1 ... Vn. Further, if Vi is of the form 'I-variable('U D')' or 'D-variable('U D')' then 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 the formula 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. Example Assertion in XML Concrete Syntax

    The XML Concrete Syntax will be an extension of the XML Concrete Syntax for SWRL, and adhere as closely as possible to the philosophy of that syntax.

    Here is an example of a simple, nonsensical assertion in XML Concrete Syntax. No namespaces are given for the new XML element tags, as yet.

    <Assertion owlx:name="Example">
        <owlx:Label>Example Rule for Expository Purposes</owlx:Label>
          <ruleml:var ruleml:type="I">x1</ruleml:var>
          <ruleml:var ruleml:type="I" type="Parent">x2</ruleml:var>
          <ruleml:var ruleml:type="I">x3</ruleml:var>
    	<swrlx:individualPropertyAtom  swrlx:property="hasParent"> 
              <ruleml:var ruleml:type="I">x1</ruleml:var>
              <ruleml:var ruleml:type="I">x2</ruleml:var>
            <swrlx:individualPropertyAtom  swrlx:property="hasBrother"> 
              <ruleml:var ruleml:type="I">x2</ruleml:var>
              <ruleml:var ruleml:type="I">x3</ruleml:var>


    [OWL S&AS]
    OWL Web Ontology Language Semantics and Abstract Syntax. Peter F. Patel-Schneider, Pat Hayes and Ian Horrocks, eds.
    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.
    [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.
    [RDF Concepts]
    Resource Description Framework (RDF) Concepts and Abstract Syntax. Graham Klyne, Jeremy J. Carroll, and Brian McBride, eds. W3C Working Draft 10 October 2003. Latest version is available at

    This archive was generated by hypermail 2.1.4 : 06/23/04 EST