From: Peter F. Patel-Schneider (pfps@research.bell-labs.com)
Date: 07/07/04
Here is the new version of my fol extension. Highlights: - all variable bound and typed - XML syntax does not have i/d distinction for variables peter
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 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 pfps@research.bell-labs.com and discussed on the mailing list of the Joint Committee (joint-committee@daml.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.
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.
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 } 'Sentence(' 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 } ')' | 'not(' 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 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.
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.
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.
Atom | Condition 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 |
exists(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. 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 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 O_{2} is entailed by an ontology O_{1} iff every interpretation that satisfies O_{1} also satisfies O_{2}.
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:Annotation> <owlx:Label>Example Rule for Expository Purposes</owlx:Label> </owlx:Annotation> <Sentence> <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:individualPropertyAtom> </and> </forall> </Sentence> </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.
This archive was generated by hypermail 2.1.4 : 07/07/04 EST