DRS guide from Drew McDermott on 2004-01-13 (public-sws-ig@w3.org from January 2004)

From: Drew McDermott <drew.mcdermott@yale.edu>
Date: Mon, 12 Jan 2004 23:08:08 -0500 (EST)
To: public-sws-ig@w3.org
Message-Id: <200401130408.i0D488O03303@pantheon-po01.its.yale.edu>
Several allusions have been made to the DRS system for representing
logical formulas in RDF.  DRS is a sort of generalized Owl Rules
Language.

I am at long last able to release a DRS Guide and accompanying Owl
ontology for formulas.  The Guide is included as an attached PDF
file. The URL for the ontology may be found at

    http://www.cs.yale.edu/homes/dvm/daml/drsonto040112.owl

It's been validated by BBN's vOWLidator
(http://owl.bbn.com/validator/), which helped me find a fix lots of
bugs.  (I admit that there several warnings remaining when my
endurance ran out; I don't know how important they were.)

The ontology and attached PDF follow.


-- 
                                   -- Drew McDermott
                                      Yale Computer Science Department


<?xml version='1.0' encoding='ISO-8859-1'?>
<!DOCTYPE rdf:RDF [
         <!ENTITY rdf 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
         <!ENTITY rdfs 'http://www.w3.org/2000/01/rdf-schema#'>
         <!ENTITY owl 'http://www.w3.org/2002/07/owl#'>
         <!ENTITY xsd 'http://www.w3.org/2001/XMLSchema#'>

         <!ENTITY ruleml 'http://www.daml.org/2003/11/swrl/swrl.rdf#'>
         <!ENTITY swrl 'http://www.daml.org/2003/11/swrl/swrl.rdf#'>
         <!ENTITY drs 'http://www.cs.yale.edu/homes/dvm/drsonto040112.owl#'>
]>

<rdf:RDF
  xmlns:rdf ="&rdf;"
  xmlns:rdfs="&rdfs;"
  xmlns="&owl;"
  xmlns:owl ="&owl;"
  xmlns:xsd ="&xsd;"
  xmlns:drs ="&drs;"
  xmlns:swrl="&swrl;"
>

<Ontology rdf:about="">
   <rdfs:comment>
      This ontology describes formulas in logical languages.
   </rdfs:comment>
</Ontology>

<Class rdf:ID="Type"/>
<!-- drs:Types are not owl:Classes, although for the purposes of this -->
<!-- ontology you can pretend they are -->

<drs:Type rdf:ID="Prop">
   <rdfs:comment>
      The type of Propositions
   </rdfs:comment>
</drs:Type>

<Class rdf:ID="Function"/>

<!-- These is provided for backward compatibility -->
<ObjectProperty rdf:ID="function_domain">
   <rdfs:domain resource="#Function"/>
   <rdfs:range resource="#Type"/>
</ObjectProperty>

<ObjectProperty rdf:ID="function_range">
   <rdfs:domain resource="#Function"/>
   <rdfs:range resource="#Type"/>
</ObjectProperty>

<ObjectProperty rdf:ID="FunctionDomain">
   <equivalentProperty rdf:resource="#function_domain"/>
</ObjectProperty>

<ObjectProperty rdf:ID="FunctionRange">
   <equivalentProperty rdf:resource="#function_range"/>
</ObjectProperty>

<Class rdf:ID="Predicate">
   <rdfs:subClassOf rdf:resource="#Function"/>
   <rdfs:subClassOf>
      <Restriction>
         <onProperty rdf:resource="#function_range"/>
         <hasValue rdf:resource="#Prop"/>
      </Restriction>
   </rdfs:subClassOf>
</Class>

<Class rdf:ID="Term"/>

<!-- Every resource can be a term, but we don't say that;
     it would collapse drs:Term and owl:Thing together,
     which would be confusing
  -->

<rdf:Description rdf:about="&swrl;Variable">
   <rdfs:subClassOf rdf:resource="#Term"/>
</rdf:Description>

<Class rdf:ID="Literal">
   <rdfs:subClassOf rdf:resource="#Term"/>
</Class>

<ObjectProperty rdf:ID="declare">
   <rdfs:domain resource="#Type"/>
</ObjectProperty>

<Class rdf:ID="Formula">
   <rdfs:subClassOf rdf:resource="#Term"/>
   <rdfs:subClassOf>
      <Restriction>
         <onProperty rdf:resource="#declare"/>
         <allValuesFrom rdf:resource="#Prop"/>
      </Restriction>
   </rdfs:subClassOf>
</Class>

<Class rdf:ID="Functional_term">
   <rdfs:subClassOf rdf:resource="#Term"/>
</Class>

<ObjectProperty rdf:ID="term_function">
   <rdfs:domain rdf:resource="#Functional_term"/>
   <rdfs:range rdf:resource="#Function"/>
</ObjectProperty>

<Class rdf:ID="Term_seq">
 <rdfs:subClassOf rdf:resource="&rdf;List"/>
 <rdfs:subClassOf>
   <Restriction>
     <onProperty rdf:resource="&rdf;first"/>
     <allValuesFrom rdf:resource="#Term"/>
   </Restriction>
 </rdfs:subClassOf>
 <rdfs:subClassOf>
   <Restriction>
     <onProperty rdf:resource="&rdf;rest"/>
     <allValuesFrom rdf:resource="#Term_seq"/>
   </Restriction>
 </rdfs:subClassOf>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;first"/>
      <cardinality>1</cardinality>
    </Restriction>
  </rdfs:subClassOf>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;rest"/>
      <cardinality>1</cardinality>
    </Restriction>
  </rdfs:subClassOf>
</Class>

<Class rdf:ID="Var_seq">
  <rdfs:subClassOf rdf:resource="#Term_seq"/>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;first"/>
      <allValuesFrom rdf:resource="&swrl;Variable"/>
    </Restriction>
  </rdfs:subClassOf>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;rest"/>
      <allValuesFrom rdf:resource="#Var_seq"/>
    </Restriction>
  </rdfs:subClassOf>
 </Class>

<ObjectProperty rdf:ID="term_args">
   <rdfs:domain rdf:resource="#Functional_term"/>
   <rdfs:range rdf:resource="#Term_seq"/>
</ObjectProperty>

<Class rdf:ID="Binder">
   <rdfs:subClassOf rdf:resource="#Formula"/>
</Class>

<Class rdf:ID="Atomic_formula">
   <unionOf rdf:parseType="Collection">
      <Class>
	 <intersectionOf rdf:parseType="Collection">
	    <Class rdf:about="#Formula"/>
	    <Class rdf:about="#Functional_term"/>
	    <Restriction>
	       <onProperty rdf:resource="#term_function"/>
	       <allValuesFrom rdf:resource="#Predicate"/>
	    </Restriction>
	 </intersectionOf>
      </Class>	
      <Class rdf:about="&swrl;Atom"/>
   </unionOf>
</Class>

<rdf:Description rdf:about="&swrl;Atom">
   <rdfs:subClassOf rdf:resource="#Atomic_formula"/>
</rdf:Description>

<!-- There are two ways to describe any atomic formula, as a
     functional term or as a triple.
     We'd like to say that the args = cons(subj, obj), but 
     presumably hopeless.
     In addition, we have to absorb the class swrl:Atom, which
     provides several more ways to describe atomic formulas. 
-->

<ObjectProperty rdf:about="&rdf;predicate">
   <rdfs:domain rdf:resource="#Atomic_formula"/>
   <rdfs:range rdf:resource="#Predicate"/>
</ObjectProperty>

<ObjectProperty rdf:about="&rdf;subject">
   <rdfs:domain rdf:resource="#Atomic_formula"/>
   <rdfs:range rdf:resource="#Term"/>
</ObjectProperty>

<ObjectProperty rdf:about="&rdf;object">
   <rdfs:domain rdf:resource="#Atomic_formula"/>
   <rdfs:range>
      <Class>
	 <unionOf rdf:parseType="Collection">
	    <Class>
	       <oneOf rdf:parseType="Collection">
		  <Thing rdf:about="#Null"/>
	       </oneOf>
	    </Class>
	    <Class rdf:about="#Term"/>
	    <Class rdf:about="#Term_seq"/>
	 </unionOf>
      </Class>
   </rdfs:range>
</ObjectProperty>

<Class rdf:ID="Function_skeleton">
   <rdfs:subClassOf rdf:resource="#Functional_term"/>
   <rdfs:subClassOf>
      <Restriction>
          <onProperty rdf:resource="#term_args"/>
          <allValuesFrom rdf:resource="#Var_seq"/>
      </Restriction>
   </rdfs:subClassOf>
</Class>

<Class rdf:ID="Predicate_skeleton">
   <intersectionOf rdf:parseType="Collection">
      <Class rdf:about="#Atomic_formula"/>
      <Class rdf:about="#Function_skeleton"/>
   </intersectionOf>
</Class>

<Class rdf:ID="Connective_formula">
   <rdfs:subClassOf rdf:resource="#Formula"/>
</Class>

<ObjectProperty rdf:ID="conn_args">
   <rdfs:domain rdf:resource="#Connective_formula"/>
   <rdfs:range rdf:resource="#Formula_seq"/>
</ObjectProperty>

<Class rdf:ID="And">
   <rdfs:subClassOf rdf:resource="#Connective_formula"/>
</Class>

<Class rdf:ID="Or">
   <rdfs:subClassOf rdf:resource="#Connective_formula"/>
</Class>

<Class rdf:ID="Unary_formula">
   <rdfs:subClassOf rdf:resource="#Connective_formula"/>
   <rdfs:subClassOf>
      <Restriction>
	<onProperty rdf:resource="#conn_args"/>
	<allValuesFrom rdf:resource="#Length1_list"/>
      </Restriction>
   </rdfs:subClassOf>
</Class>

<Class rdf:ID="Binary_formula">
   <rdfs:subClassOf rdf:resource="#Connective_formula"/>
   <rdfs:subClassOf>
      <Restriction>
	<onProperty rdf:resource="#conn_args"/>
	<allValuesFrom rdf:resource="#Length2_list"/>
      </Restriction>
   </rdfs:subClassOf>
</Class>

<Class rdf:ID="Not">
   <rdfs:subClassOf rdf:resource="#Unary_formula"/>
</Class>

<ObjectProperty rdf:ID="negated">
   <rdfs:domain rdf:resource="#Not"/>
   <rdfs:range rdf:resource="#Formula"/>
</ObjectProperty>
<!-- The 'negated' of a 'Not' is the 'first' of its 'conn_args' -->

<Class rdf:ID="Implies">
   <rdfs:subClassOf rdf:resource="#Binary_formula"/>
</Class>

<!-- The following are labels for the two conn_args of Implies -->

<ObjectProperty rdf:ID="antecedent">
   <rdfs:domain rdf:resource="#Implies"/>
   <rdfs:range rdf:resource="#Formula"/>
</ObjectProperty>

<ObjectProperty rdf:ID="consequent">
   <rdfs:domain rdf:resource="#Implies"/>
   <rdfs:range rdf:resource="#Formula"/>
</ObjectProperty>

<ObjectProperty rdf:ID="declaration">
   <rdfs:domain rdf:resource="#Function"/>
   <rdfs:range rdf:resource="#Function_skeleton"/>
</ObjectProperty>

<DatatypeProperty rdf:ID="value">
   <rdfs:domain rdf:resource="#Literal"/>
   <!-- range can be any XSD datatype -->
</DatatypeProperty>
<!-- type restriction: If a term is a Literal and is declared of type
     Y, then the 'value' should be a literal of type Y.
     Can this be expressed in OWL? -->

<Class rdf:ID="Forall">
   <rdfs:subClassOf rdf:resource="#Binder"/>
</Class>

<Class rdf:ID="Exists">
   <rdfs:subClassOf rdf:resource="#Binder"/>
</Class>

<ObjectProperty rdf:ID="bound_vars">
   <rdfs:domain rdf:resource="#Binder"/>
   <rdfs:range rdf:resource="#Var_bag"/>
</ObjectProperty>

<ObjectProperty rdf:ID="body">
   <rdfs:domain rdf:resource="#Binder"/>
   <rdfs:range rdf:resource="#Formula"/>
</ObjectProperty>

<!-- There's nothing to say about Null -->
<rdf:Description rdf:ID="Null"/>

<ObjectProperty ID="type">
  <rdfs:comment>Identifies the Class of a resource</rdfs:comment>
</ObjectProperty>

<Class rdf:ID="Constant">
   <rdfs:domain rdf:resource="#Term"/>
</Class>

<Class rdf:ID="Constant_bag">
  <rdfs:subClassOf rdf:resource="&rdf;List"/>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;first"/>
      <allValuesFrom rdf:resource="#Constant"/>
    </Restriction>
  </rdfs:subClassOf>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;rest"/>
      <allValuesFrom rdf:resource="#Constant_bag"/>
    </Restriction>
  </rdfs:subClassOf>
</Class>

<Class rdf:ID="Var_bag">
  <rdfs:subClassOf rdf:resource="&rdf;List"/>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;first"/>
      <allValuesFrom rdf:resource="&swrl;Variable"/>
    </Restriction>
  </rdfs:subClassOf>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;rest"/>
      <allValuesFrom rdf:resource="#Var_bag"/>
    </Restriction>
  </rdfs:subClassOf>
</Class>

<Class rdf:ID="Formula_seq">
  <rdfs:subClassOf rdf:resource="&rdf;List"/>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;first"/>
      <allValuesFrom rdf:resource="#Formula"/>
    </Restriction>
  </rdfs:subClassOf>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;rest"/>
      <allValuesFrom rdf:resource="#Formula_seq"/>
    </Restriction>
  </rdfs:subClassOf>
</Class>

<Class rdf:ID="Term_bag">
  <rdfs:subClassOf rdf:resource="&rdf;List"/>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;first"/>
      <allValuesFrom rdf:resource="#Term"/>
    </Restriction>
  </rdfs:subClassOf>
  <rdfs:subClassOf>
    <Restriction>
      <onProperty rdf:resource="&rdf;rest"/>
      <allValuesFrom rdf:resource="#Term_bag"/>
    </Restriction>
  </rdfs:subClassOf>
</Class>

<ObjectProperty  rdf:about="&rdf;first"/>  
<ObjectProperty  rdf:about="&rdf;rest"/>  
<Class rdf:about="&rdf;List"/>

<Class rdf:ID="Nonempty_list">
   <intersectionOf rdf:parseType="Collection">
      <Class rdf:about="&rdf;List"/>
      <Class>
	 <complementOf>
	    <Class>
	       <oneOf rdf:parseType="Collection">
		  <Thing rdf:about="&rdf;nil"/>
	       </oneOf>
	    </Class>
	 </complementOf>
      </Class>
   </intersectionOf>
</Class>

<Class rdf:ID="Length1_list">
   <intersectionOf rdf:parseType="Collection">
      <Class rdf:about="#Nonempty_list"/>
      <Restriction>
	<onProperty rdf:resource="&rdf;rest"/>
	<hasValue rdf:resource="&rdf;nil"/>
      </Restriction>
   </intersectionOf>
</Class>

<Class rdf:ID="Length2_list">
   <intersectionOf rdf:parseType="Collection">
      <Class rdf:about="#Nonempty_list"/>
      <Restriction>
	<onProperty rdf:resource="&rdf;rest"/>
	<allValuesFrom rdf:resource="#Length1_list"/>
      </Restriction>
   </intersectionOf>
</Class>

<DatatypeProperty rdf:ID="litdefn">
   <rdfs:domain rdf:resource="#Literal"/>
   <!-- The range is any literal, but I don't think that's a class -->
</DatatypeProperty>

</rdf:RDF>
Attachments

application/pdf attachment: DRSguide.pdf
Received on Monday, 12 January 2004 23:08:46 UTC