owl axioms, otter form from Sandro Hawke on 2003-01-08 (www-archive@w3.org from January 2003)

From: Sandro Hawke <sandro@w3.org>
Date: Wed, 08 Jan 2003 15:17:16 -0500
To: connolly@w3.org
Cc: www-archive@w3.org
Message-Id: <200301082017.h08KHGx15821@wadimousa.hawke.org>
rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/description>', '<md5:821f59c4d08564bb37d62c58b49f0d03>').
rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/description>', '<md5:1f0efb73e107e9313dcc5f6dfbe9892a>').
rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/source>', '<http://www.w3.org/TR/2002/WD-owl-features-20020729/>').
rdf('<file:/tmp/ontAx.n3>', '<http://purl.org/dc/elements/1.1/source>', '<http://www.agfa.com/w3c/euler/owl-rules>').
rdf('<file:/tmp/ontAx.n3>', rdfs_seeAlso, '<http://www.w3.org/2000/10/swap/util/rdfs-rules.n3>').
rdf(daml_Class, rdfs_label, '<md5:9bd81329febf6efe22788e03ddeaf0af>').
rdf(daml_Class, rdfs_subClassOf, rdfs_Class).
rdf(daml_sameClassAs, rdf_type, daml_TransitiveProperty).
rdf(daml_sameClassAs, rdf_type, daml_SymmetricProperty).

all A B (
   rdf(A, daml_sameClassAs, B) <-> rdf(B, rdfs_subClassOf, A) & rdf(A, rdfs_subClassOf, B)
).
rdf(daml_samePropertyAs, rdf_type, daml_TransitiveProperty).
rdf(daml_samePropertyAs, rdf_type, daml_SymmetricProperty).

all A B (
   rdf(A, daml_samePropertyAs, B) <-> rdf(B, rdfs_subPropertyOf, A) & rdf(A, rdfs_subPropertyOf, B)
).
rdf(daml_sameIndividualAs, rdf_type, daml_TransitiveProperty).
rdf(daml_sameIndividualAs, rdf_type, daml_SymmetricProperty).

all A B C D (
   rdf(A, daml_sameIndividualAs, B) & rdf(A, C, D) -> rdf(B, C, D)
).

all A B C D (
   rdf(A, daml_sameIndividualAs, B) & rdf(C, D, A) -> rdf(C, D, B)
).
rdf(daml_differentIndividualFrom, rdf_type, daml_SymmetricProperty).
rdf(daml_differentIndividualFrom, ontAx__converse, daml_sameIndividualAs).
rdf(ontAx__converse, rdf_type, daml_SymmetricProperty).

all A B C (
    -(exists s (rdf(s, ontAx__converse, A) & rdf(B, s, C))) -> rdf(B, A, C)
).

all A B C (
   (exists s (rdf(s, ontAx__converse, A) & rdf(B, s, C))) ->  -rdf(B, A, C)
).
rdf(daml_inverseOf, rdf_type, daml_SymmetricProperty).

all A B C (
   (exists s (rdf(s, daml_inverseOf, A) & rdf(B, s, C))) -> rdf(C, A, B)
).

all A B C D (
   rdf(A, rdf_type, daml_FunctionalProperty) -> (rdf(B, A, C) & rdf(B, A, D) -> rdf(C, daml_equivalentTo, D))
).

all A B C D (
   rdf(A, rdf_type, daml_InverseFunctionalProperty) -> (rdf(B, A, C) & rdf(D, A, C) -> rdf(B, daml_equivalentTo, D))
).

all A B C D (
   (exists s (((rdf(s, daml_allValuesFrom, A) & rdf(s, daml_onProperty, B)) & rdf(C, rdf_type, s)) & rdf(C, B, D))) -> rdf(D, rdf_type, A)
).

all A B C (
   (exists s ((rdf(s, daml_onProperty, A) & rdf(s, daml_someValuesFrom, B)) & rdf(C, rdf_type, s))) -> (exists t (rdf(t, rdf_type, B) & rdf(C, A, t)))
).
rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:298e17a6fc6db286af85fedc40e8d132>').
rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:bfbe1f1d0c2a32c63467e34db15b3e38>').

all A B (
   (exists s (rdf(s, daml_item, A) & rdf(B, daml_oneOf, s))) -> rdf(A, rdf_type, B)
).

all A B C D (
   (rdf(A, daml_oneOf, B) & rdf(C, daml_oneOf, D)) & rdf(B, daml_rest, D) -> rdf(C, rdfs_subClassOf, A)
).
rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:8425c7c4e78a0b61ca0177cba0fc28fd>').
rdf(daml_first, rdf_type, daml_FunctionalProperty).
rdf(daml_rest, rdf_type, daml_FunctionalProperty).

all A B (
   rdf(A, daml_first, B) -> rdf(A, ontAx__item, B)
).
rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:6f05a3e924c4636761b0bddc7ee46f69>').
rdf('<file:/tmp/ontAx.n3>', ontAx_note, '<md5:bcc79261d87a60c1f21ef1b0b91d2692>').

all A B (
   rdf(A, daml_equivalentTo, B) -> rdf(B, daml_equivalentTo, A)
).

all A B C D (
   ((rdf(A, log_notEqualTo, log_forAll) & rdf(A, log_notEqualTo, log_forSome)) & rdf(B, daml_equivalentTo, C)) & rdf(B, A, D) -> rdf(C, A, D)
).

all A B C D (
   ((rdf(A, daml_equivalentTo, B) & rdf(A, log_notEqualTo, log_forAll)) & rdf(A, log_notEqualTo, log_forSome)) & rdf(C, A, D) -> rdf(C, B, D)
).

all A B C D (
   ((rdf(A, log_notEqualTo, log_forAll) & rdf(A, log_notEqualTo, log_forSome)) & rdf(B, A, C)) & rdf(C, daml_equivalentTo, D) -> rdf(B, A, D)
).

all A B (
   rdf(A, daml_sameIndividualAs, B) -> rdf(B, daml_sameIndividualAs, A)
).

all A B C (
   (exists s (rdf(s, daml_sameIndividualAs, A) & rdf(s, B, C))) -> rdf(A, B, C)
).

all A B (
   rdf(A, daml_samePropertyAs, B) -> rdf(B, daml_samePropertyAs, A)
).

all A B C D (
   rdf(A, rdf_type, daml_UnambiguousProperty) -> (rdf(B, A, C) & rdf(D, A, C) -> rdf(B, daml_equivalentTo, D))
).

all A (
   rdf(A, rdf_type, daml_Nothing) -> rdf(A, rdf_type, ontAx_SymptomOfInconsistency)
).

all A B C D (
   (rdf(A, daml_hasValue, B) & rdf(A, daml_onProperty, C)) & rdf(D, C, B) -> rdf(D, rdf_type, A)
).

all A B C (
   (exists s (exists t (exists u (((((rdf(u, daml_intersectionOf, t) & rdf(t, daml_first, A)) & rdf(t, daml_rest, s)) & rdf(s, daml_first, B)) & rdf(s, daml_rest, daml_nil)) & rdf(C, rdf_type, u))))) -> rdf(C, rdf_type, A) & rdf(C, rdf_type, B)
).

all A B (
   rdf(A, daml_differentIndividualFrom, B) -> rdf(A, rdf_type, daml_Thing)
).
rdf(daml_Nothing, daml_oneOf, daml_nil).
rdf(daml_Thing, daml_complementOf, daml_Nothing).

all A B C (
   (exists s ((rdf(s, A, B) & rdf(A, rdf_type, daml_TransitiveProperty)) & rdf(C, A, s))) -> rdf(C, A, B)
).

all A B C (
   rdf(A, rdf_type, daml_SymmetricProperty) & rdf(B, A, C) -> rdf(C, A, B)
).

all A B C D E (
   (((rdf(A, daml_hasAtMostOne, B) & rdf(C, log_notEqualTo, D)) & rdf(E, rdf_type, A)) & rdf(E, B, C)) & rdf(E, B, D) -> rdf(C, daml_equivalentTo, D)
).

all A B (
   (exists s (rdf(s, ontAx__item, A) & rdf(B, daml_rest, s))) -> rdf(B, ontAx__item, A)
).

all A B (
   rdf(A, daml_equivalentTo, B) -> rdf(A, daml_equivalentTo, B)
).

all A B C (
   (exists s (rdf(s, daml_sameIndividualAs, A) & rdf(B, C, s))) -> rdf(B, C, A)
).

all A B C (
   (exists s (rdf(s, daml_samePropertyAs, A) & rdf(B, s, C))) -> rdf(B, A, C)
).

all A B C D (
   (exists s (exists t (((((((rdf(t, daml_first, A) & rdf(t, daml_rest, s)) & rdf(s, daml_first, B)) & rdf(s, daml_rest, daml_nil)) & rdf(C, daml_intersectionOf, t)) & rdf(A, log_notEqualTo, B)) & rdf(D, rdf_type, A)) & rdf(D, rdf_type, B)))) -> rdf(D, rdf_type, C)
).

all A B C D (
   (exists s (exists t (exists u (exists s0 (((((((rdf(s0, daml_complementOf, u) & rdf(u, daml_oneOf, A)) & rdf(t, daml_oneOf, s)) & rdf(s, daml_first, B)) & rdf(s, daml_rest, A)) & rdf(C, daml_complementOf, t)) & rdf(D, rdf_type, s0)) & rdf(D, daml_differentIndividualFrom, B)))))) -> rdf(D, rdf_type, C)
).
end_list.
Received on Wednesday, 8 January 2003 15:22:35 UTC