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.
This is a Proposal approved 2 November 2004 by the Joint Committee of the DARPA DAML Program. The initial version was produced 7 July 2004 for consideration by the Joint Committee of the DARPA DAML Program.
Comments on this document, in particular on known issues, are invited and should be sent to the W3C RDF rules mailing list (www-rdf-rules@w3.org).
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.
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 name | Namespace |
|---|---|
| rdf | http://www.w3.org/1999/02/22-rdf-syntax-ns# |
| rdfs | http://www.w3.org/2000/01/rdf-schema# |
| xsd | http://www.w3.org/2001/XMLSchema# |
| owl | http://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].
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 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 are 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 ')'
It would not be hard to allow for predicates with arity other than 1 or 2, by extending SWRL atoms as follows:
atom ::= URIreference '(' { object } ')' object ::= i-object | d-object
The development of this extension is not considered further here.
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).
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.
| Atom | Condition 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.
The following XML concrete syntax closely follows the XML concrete syntax for First-Order-Logic Rule ML [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>
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.
See also the issues list in First-Order-Logic Rule ML [FOL Rule ML].