Drew --
Interesting DRS guide.....
I'm a bit vague however about what you will actually do
with formulae encoded in RDF. If you ship them around the Web, that
seems to imply that anyone receiving them has to have a suitable theorem
prover / reasoner. So, do you ship that too ? In DRS?
If so, then the recipients need perhaps to unwrap ontology RDF
and the prover RDF to get strings like the ones Bijan
suggested?
To put it another way, do you have a DRS usage scenario in mind ?
Thanks in advance for educating me about this.
BTW, Ontomerge 0.1* Ontology
Translation Server seems to be down at the moment.
Cheers
-- Adrian
*
http://www.cs.yale.edu/homes/dvm/daml/ontology-translation.html
INTERNET BUSINESS LOGIC
www.reengineeringllc.com
Dr. Adrian Walker
Reengineering LLC
PO Box 1412
Bristol
CT 06011-1412 USA
Phone: USA 860 583 9677
Cell: USA 860 830 2085
Fax: USA 860 314 1029
At 11:08 PM 1/12/04 -0500, you wrote:
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>