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

Copyright © 2004 Lucent Technologies. All Rights Reserved.
This document is available under the W3C Document License. See the W3C Intellectual Rights Notices and Disclaimers for additional information.

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.

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:

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

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.

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.

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.

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

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
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 O₂ is entailed by an ontology O₁ iff every interpretation that satisfies O₁ also satisfies O₂.

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.

5. Example Assertion in XML Concrete Syntax

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:

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

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:

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.