new version of my FOL extension

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

  • Next message: Mike Dean: "RE: new version of my FOL extension"
    [With a better subject line:]
    
    Here is the new version.
    
    Highlights:
    - all variables bound and typed
    - XML syntax does not have i/d distinction
    
    peter
    
    
    
    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:
    http://www-db.research.bell-labs.com/usr/pfps/swrl/fol-20040624.html
    Latest version:
    http://www-db.research.bell-labs.com/usr/pfps/swrl/fol-20040624.html
    Author:
    Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies

    Abstract

    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.

    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:


    Namespace nameNamespace
    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

    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 ')'
    

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

    References

    [OWL S&AS]
    OWL Web Ontology Language Semantics and Abstract Syntax. Peter F. Patel-Schneider, Pat Hayes and Ian Horrocks, eds.
    [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.
    [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 http://www.w3.org/TR/rdf-concepts/.


    This archive was generated by hypermail 2.1.4 : 07/07/04 EST