Re: V0.1 strawman of FOL extension of SWRL

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

  • Next message: Pat Hayes: "rather drafty draft of SCL 1.0" 
    Here is a different, minimalist proposal.

peter



Syntax:

Non-terminals taken from other grammars are prefixed by that grammar
as in OWL/annotation.  The axiom non-terminal from OWL is not so
treated, as the idea here is to augment OWL axioms with an axiom that
provides for assertion of first-order formulae.

axiom ::= assertion

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

foformula ::= SWRL/atom
	    | 'and(' foformula* ')'
	    | 'or(' foformula* ')'
	    | 'not(' foformula ')'
	    | 'implies(' foformula foformula ')'
	    | 'equivalent(' foformula foformula ')'
	    | 'forall(' variable+ foformula ')'
	    | 'exists(' variable+ foformula ')'

variable ::= SWRL/i-variable
	   | 'I-variable(' RDF/URIreference OWL/description ')'
	   | SWRL/d-variable
	   | 'D-variable(' RDF/URIreference OWL/dataRange ')'

Semantics:

To be somewhat compatible with RDF, free variables in assertions are
treated existentially.  The rest of the semantic characterization is
standard.


Option:

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

atom ::= RDF/URIreference '(' object* ')'
object ::= SWRL/i-object | SWRL/d-object

The denotation of such predicates would be sets of tuples of domain
elements with the usual shorthand of identifying 1-tuples of domain
elements with domain elements.

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