This document presents a formalization of an OWL version in the ACL2 logic, based on the original specification provided in:
The Web Ontology Language (OWL), RDF compatible
Peter F. Patel-Schneider
Bell Labs Research
4 January 2002
One result of this exercise is that we can be assured that there exists an interpretation (a set of values for EXT, CEXT, etc.) that satisfies the axioms as stated in the original document (subject to the notes on completeness).
It would have been simpler to use ACL2's defaxiom construct to simply write down an axiomatic description. I chose to use ACL2's encapsulation mechanism instead. Encapsulation requires that the user exhibit witnesses for the primitive functions so that the encapsulated theorems can be proven. This guarantees that there exists at least one interpretation that satisifies the OWL axioms stated here.
I use constant functions to define the witnesses for the necessary sets and mappings (R, CEXT, etc.).
The items labeled as theorems in the body of this report should be considered axioms that have been demonstrated to be mutually satisfiable. The theorems in the appendices hold generally, that is they are not in the scope of the encapsulation.
To quote from the ACL2 documentation:
ACL2 is a mathematical logic together with a mechanical theorem prover to help you reason in the logic.
As a logic, ACL2 is a formal system with rigorously defined syntax and semantics. In mathematical parlance, the ACL2 logic is a first-order logic of total recursive functions providing mathematical induction on the ordinals up to epsilon-0 and two extension principles: one for recursive definition and one for constrained introduction of new function symbols, here called encapsulation. The syntax of ACL2 is that of Common Lisp;ACL2 has been used to prove properties of a wide assortment of software and hardware systems, including a mechanically verified proof of correctness of the floating-point multiplication, division, and square root instructions of the AMD K7 microprocessor. It has also been used to formalize the Java Virtual Machine and a subset of the Ada programming language.
The current version of this specification is incomplete in two ways.
The transitive-closure function for swol:TransitiveProperty has not been written. A stub is provided that returns the single argument. The function has been defined (the easy part) but I need to prove termination in order to have it accepted by ACL2. The proof is fairly clear, but the details of mechanizing the proof are not worth the effort on this preliminary version.
Several items, W13, W14, W15, W18, and W19, required the construction of unpleasantly large witnesses in order to prove the IFF in both directions. The correct approach here is to write routines that create witness values that ensure these properties. I have not yet done this. This would be similar to the use of rdfs-closures in the RDF Model Theory.
The existing witnesses guarantee that the theorems hold in one direction,
but not in the other. For example, I have shown that all classes in EXT(S(swol:disjointWith)) have no members in common. I have not show that for all empty classes, c, (which are "disjointWith" themselves), <c,c> is an element of EXT(S(swol:disjointWith)).<x,y> in EXT(p) -> relation
Because ACL2 is first-order, we cannot directly assert properties about the domain and range of functions. We use constants to define the functions whose domain and range are of interest and demonstrate range and domain properties based on these constants. We also use theorems of the form
Theorem cext-domain-sub-c CEXT(x) -> x in C() ;to capture the notion that the elements of the domain of CEXT are in C. The theorem states that if CEXT(x) returns a non-NIL value, then x is an element of C(). If we were to attempt to prove theorems based on the assertions exported from the encapsulation, this statement would not cover the case where x is a defined class but has no elements.
After running the original ACL2 source through the ACL2 Theorem Prover to validate it, I applied a mechanical translation process to map the ACL2 prefix syntax to an infix presentation in HTML (this document). This process also translated comments to running text. I edited the result somewhat for presentation and included the W3C stylesheet, W3C-WD.css.
Literals in ACL2 are either characters, numbers, strings, or quoted atoms. So names and elements of the various sets that are not RDF literals exhibit a surface syntax of the form
'name
Like RDF, ACL2 uses a colon (":") to delimit namespaces in identifiers. As a lexical simplification, I have replaced all occurrences of "rdf:", "rdfs:", and "swol:" with "rdf-", "rdfs-", and "swol-", respectively.
This file is a list of commented events. The basic events include:
Events are processed sequentially. In order to be admitted, a function must be proven to terminate. For a non-recursive functions, this is trivial. For recursive functions in this file we normally induct over the length of a list.
Constant definition: Constant name value ; Function definition: Function name args body ;
Theorem to be proved: Theorem name clause ;
Note that all variables in theorems are universally quantified. E.g.
Theorem FOO P(x) -> Q(x, y);is equivalent to
forall x,y . P(x) -> Q(x,y)
Unless indicated otherwise, all theorems are proved before we proceed. Those theorems are then available to support the proof of later theorems. The proofs in this exercise tend to be trivial, as most of them just require evaluation over ground terms. While some of them have many cases (~1000), they do not require clever proof tactics or supporting lemmas.
[ ... ] Brackets surround sets (lists). [ ] The empty set (list) or NIL. Logically, NIL is false and non-NIL is true. (x . y) Create a pair (the cons operation). x @ y Concatenate two lists (the append operation). [x y ... z] Shorthand for (x . (y . ... (z . nil))) '[x y z] Shorthand for ['x 'y 'z] first((x . y)) First element of list. Returns x. (the car function). rest((x . y)) Tail of list. Returns y. (the cdr function). null(s) Test if s is an empty set (list). x in l Test if x is a member of set (list) l (member). x sub y Test if x is a subset of y. endp(l) Test if l is not a pair (not a cons). This is normally used to indicate the end of recursion over a list. list \ v Given a list of lists, list = [(x0. y0) ... (xn . yn)]
list \ v returns the first pair (xi . yi) such that v = xi.
This is the assoc operation.x - y When x and y are sets, this is set difference. a X b Cartesian product.
Declare the package (namespace) to be used by default.
In-Package("ACL2");
Load a library of simple set theory functions and proven theorems about them.
Include("/app/acl2/newest/acl2-sources/books/data-structures/set-defthms");
Load a library of additional set operations and function support, including range, domain, and Cartesian product.
Include("ACL2/function-defuns");
We define constants to be witnesses for EXT, CEXT, S, and the various datatype properties. These sets are defined as functions that return the value of the respective constants, *EXT*, *CEXT*, *S*, etc.
The bindings of the constants satisfy the theorems in this file. Using encapsulation, once we have exhibited this set of witnesses and proven the associated theorems, we can use the theorems going forward, without a commitment to the literal bindings provided by the witnesses. Then we have a nice collection of abstract sets, and theorems, as in the Patel-Schnieder's original semantics. For the purposes of this presentation I have suppressed the syntactic details of the surrounding ACL2 encapsulate.
An alternative would be to declare these properties as axioms. But it is safer to demonstrate that the axioms can be satisfied.
We are using lists to implement sets. In general we don't care if the data values are actually bags, but we prefer no-duplicates(s) to be true for all sets, s.
The witnesses are contained in an appendix.
Include("ACL2/witness");
We repeat some of the forms in the witness file in order to provide a sense the witness' content. None of the witness constants will be visible outside of the encapsulation.
We provided just one datatype in the witness.
Constant *dt* = '[integerdt];
U(d), URI for the datatype;
Constant *du* = '[(integerdt . http://integer)];
L(d), the lexical space for the datatype;
Constant *dl* = '[[integerdt lexone lextwo]];
V(d), value space for d
Constant *dv* = '[[integerdt 1 2]];
LV(d), datatypeName -> ( L(d) -> V(d) )
Constant *dlv* = '[[integerdt (lexone . 1) (lextwo . 2)]];
These functions will be visible outside of the encapsulate, but the only properties about them that will be visible are captured by the theorems exported from the encapsulation.
List of all datatype ids.
Function DT() *dt* ;
U(d), URI for the datatype.
Map a datatype name to a URL. We use DU rather than U, since U is predefined in ACL2.
Function DU(d) rest(*du* \ d ) ;
V(d), value space for datatype d.
Map datatype name to values. We use DV for consistency with DU.
Function DV(d) rest(*dv* \ d ) ;
L = union over d in DT of L(d), lexical values
Function L() union-all(range(*dl*)) ;
V = union over d in DT of V(d), data values
Function V() union-all(range(*dv*)) ;
LV = union over d in DT of LV(d)
Look up the first occurrence of name a in the union of datatype mappings.
Function LV(a) rest(union-all(range(*dlv*)) \ a ) ;
Mapping property names to a relation (set of pairs).
EXT : P -> 2^(Rx(RuV))
*EXT* is a mapping from property name to the set of pairs that identify the elements of the relation.
Witness : Constant *EXT* ...
Function EXT(p) rest(*EXT* \ p ) ;
Mapping class names to their elements.
CEXT : C -> 2^(RuV)
Witness : Constant *CEXT* ...
Function CEXT(c) rest(*CEXT* \ c ) ;
Mapping from names to denotation
S : N -> R
S must be complete, since we use it to compute N.
Witness : Constant *S* = ...;
Function S(u) rest(*S* \ u ) ;
R, the domain of resources. R is nonempty and disjoint from V
Function R() CEXT(S('rdfs-resource) ;
Theorem r-nonempty ¬(null(R())) ;
Theorem r-disjoint-v null(R() intersect V()) ;
P, properties.
Function P() CEXT(S('rdf-property)) ;
P <= R and P is nonempty
Theorem p-subset-r P() sub R() ;
Theorem p-nonempty ¬(null(P())) ;
C, classes.
Function c() CEXT(S('rdfs-class)) ;
For export from the encapsulate. set equality is indicated by =s.
Theorem p-eq-class-property P() =s CEXT(S('rdf-property)) ;
Theorem c-subset-r C() sub R() ;
Theorem c-nonempty ¬(null(C())) ;
For export from the encapsulate. Because ACL2 is first-order, we cannot directly assert properties about the domain of functions. The axioms below don't capture the original statement of the property as well as the internal versions for the simple reason that a property can be in the domain of EXT, but have no elements. Thus EXT(x) might return NIL (false), even though x is an element of P.
Theorem c-eq-class-class C() =s CEXT(S('rdfs-class)) ;
Theorem s-mapsto-r S(x) -> S(x) in R(x) ;
Theorem ext-domain-sub-p EXT(x) -> x in P() ;
Theorem cext-domain-sub-c CEXT(x) -> x in C() ;
Not for export, since the constants are not exportable.
Theorem s-mapsto-r-int x in domain(*S*) -> (S(x) in R() ) ;
Theorem ext-domain-sub-p-int domain(*EXT*) sub P() ;
Theorem cext-domain-sub-c-int domain(*CEXT*) sub C() ;
Theorem cext-range-sub-ruv x in range(*CEXT*) -> (CEXT(x) sub (R() union V() ) ) ;
Theorem ext-range-sub-rxruv
x in range(*EXT*)
-> (EXT(x) sub (R() X (R() union V() ) ) ) ;
The following conditions must be satisfied by an interpretation.
R1: CEXT(S(rdf:Property)) = P
Theorem r1 CEXT(S('rdf-property)) = P() ;
R2: S(rdf:type) in P
Theorem r2 S('rdf-type) in P() ;
R3: for x in R, x in CEXT(y) iff <x,y> in EXT(S(rdf:type))
Theorem r3
x in R()
-> (x in CEXT(y) iff (x . y) in EXT(S('rdf-type))) ;
Theorem s1 CEXT(S('rdfs-resource)) = R() ;
S2: CEXT(S(rdfs:Class)) = C
Theorem s2 CEXT(S('rdfs-class)) = C() ;
S3: CEXT(S(rdfs:Literal)) = V
Theorem s3 CEXT(S('rdfs-literal)) = V() ;
S4: C\DT contains S(rdfs:Resource), S(rdf:Property), S(rdfs:Class),
S(rdfs:Literal)
Theorem s4
S('rdfs-resource) in (C() - DT())
and S('rdf-property) in (C() - DT())
and S('rdfs-class) in (C() - DT())
and S('rdfs-literal) in (C() - DT()) ;
S5: P contains S(rdfs:subClassOf), S(rdfs:subPropertyOf)
S(rdfs:domain), S(rdfs:range)
Theorem s5
S('rdfs-subclassof) in P()
and S('rdfs-subpropertyof) in P()
and S('rdfs-domain) in P()
and S('rdfs-range) in P() ;
S6: EXT(S(rdfs:subClassOf)) contains < S(rdfs:Class), S(rdfs:Resource) >,
< S(rdfs:Property), S(rdfs:Resource) >
Theorem s6
(S('rdfs-class) . S('rdfs-resource)) in EXT(S('rdfs-subclassof))
and (S('rdf-property) . S('rdfs-resource)) in EXT(S('rdfs-subclassof)) ;
S7: EXT(S(rdfs:domain)) contains < S(rdf:type), S(rdfs:Resource) >
< S(rdfs:subClassOf), S(rdfs:Class) >
< S(rdfs:subPropertyOf), S(rdfs:Property) >
< S(rdfs:domain), S(rdfs:Property) >
< S(rdfs:range), S(rdfs:Property) >
Theorem s7
(S('rdf-type) . S('rdfs-resource)) in EXT(S('rdfs-domain))
and (S('rdfs-subclassof) . S('rdfs-class)) in EXT(S('rdfs-domain))
and (S('rdfs-subpropertyof) . S('rdf-property)) in EXT(S('rdfs-domain))
and (S('rdfs-domain) . S('rdf-property)) in EXT(S('rdfs-domain))
and (S('rdfs-range) . S('rdf-property)) in EXT(S('rdfs-domain)) ;
S8: EXT(S(rdfs:range)) contains < S(rdf:type), S(rdfs:Class) >
< S(rdfs:subClassOf), S(rdfs:Class) >
< S(rdfs:subPropertyOf), S(rdfs:Property) >
< S(rdfs:domain), S(rdfs:Class) >
< S(rdfs:range), S(rdfs:Class) >
Theorem s8
(S('rdf-type) . S('rdfs-class)) in EXT(S('rdfs-range))
and (S('rdfs-subclassof) . S('rdfs-class)) in EXT(S('rdfs-range))
and (S('rdfs-subpropertyof) . S('rdf-property)) in EXT(S('rdfs-range))
and (S('rdfs-domain) . S('rdfs-class)) in EXT(S('rdfs-range))
and (S('rdfs-range) . S('rdfs-class)) in EXT(S('rdfs-range)) ;
S9: <x,y> in EXT(S(rdfs:subClassOf)) implies CEXT(x) <= CEXT(y)
Theorem s9
(x . y) in EXT(S('rdfs-subclassof)) -> (CEXT(x) sub CEXT(y) ) ;
S10: <r,s> in EXT(S(rdfs:subPropertyOf)) implies EXT(r) <= EXT(s)
Theorem s10
(r . s) in EXT(S('rdfs-subpropertyof)) -> (EXT(r) sub EXT(s) ) ;
S11: if <x,y> in EXT(p) and <p,c> in EXT(S(rdfs:domain))
then x in CEXT(c)
Theorem s11
(x . y) in EXT(p)
and (p . c) in EXT(S('rdfs-domain))
-> x in CEXT(c) ;
S12 requires that 'class be in CEXT('property).
S12: if <x,y> in EXT(p) and <p,c> in EXT(S(rdfs:range))
then y in CEXT(c)
Theorem s12
(x . y) in EXT(p)
and (p . c) in EXT(S('rdfs-range))
-> y in CEXT(c) ;
D1: DT <= C
Theorem d1 DT() sub C() ;
D2: for d in DT, S(U(d)) = d
Theorem d2 d in DT() -> S(DU(d)) = d ;
D3: S(swol:Datatype) in C\DT
Theorem d3 S('swol-datatype) in (C() - DT()) ;
D4: CEXT(S(swol:Datatype)) = DT
Theorem d4 DT() = CEXT(S('swol-datatype)) ;
D5 requires datatypes to be classes.
D5: for d in DT, CEXT(d) = V(d)
Theorem d5 d in DT() -> CEXT(d) = dv(d) ;
W1: C\DT contains S(swol:Class)
S(swol:ObjectProperty), S(swol:DatatypeProperty),
S(swol:UniqueProperty), S(swol:UnambiguousProperty)
S(swol:TransitiveProperty)
Theorem w1
[S('swol-class),
S('swol-objectproperty),
S('swol-datatypeproperty),
S('swol-uniqueproperty),
S('swol-unambiguousproperty),
S('swol-transitiveproperty)]
sub (C() - DT()) ;
W2: P contains S(swol:sameClassAs), S(swol:disjointWith),
S(swol:samePropertyAs),
S(swol:sameIndividualAs), S(swol:differentIndividualFrom)
Theorem w2
[S('swol-sameclassas),
S('swol-disjointwith),
S('swol-samepropertyas),
S('swol-sameindividualas),
S('swol-differentindividualfrom)]
sub P() ;
W3: EXT(S(rdfs:subClassOf)) contains
<S(swol:Class), S(rdfs:Class)>
<S(swol:ObjectProperty), S(rdf:Property)>
<S(swol:DatatypeProperty), S(rdf:Property)>
<S(swol:UniqueProperty), S(rdf:Property)>
<S(swol:UnambiguousProperty),S(swol:ObjectProperty)>
<S(swol:TransitiveProperty), S(swol:ObjectProperty)>
Theorem w3
[(S('swol-class) . S('rdfs-class)) ,
(S('swol-objectproperty) . S('rdf-property)) ,
(S('swol-datatypeproperty) . S('rdf-property)) ,
(S('swol-uniqueproperty) . S('rdf-property)) ,
(S('swol-unambiguousproperty) . S('swol-objectproperty)) ,
(S('swol-transitiveproperty) . S('swol-objectproperty))]
sub EXT(S('rdfs-subclassof)) ;
W4: EXT(S(rdfs:subPropertyOf)) contains
<S(swol:sameClassAs), S(rdfs:subClassOf)>
<S(swol:samePropertyAs), S(rdfs:subPropertyOf)>
Theorem w4
[(S('swol-sameclassas) . S('rdfs-subclassof)) ,
(S('swol-samepropertyas) . S('rdfs-subpropertyof))]
sub EXT(S('rdfs-subpropertyof)) ;
W5: EXT(S(rdfs:domain)) contains
<S(swol:sameClassAs),S(rdfs:Class)>,
<S(swol:disjointWith),S(rdfs:Class)>
<S(swol:samePropertyAs),S(rdf:Property)>
<S(swol:sameIndividualAs),S(rdfs:Resource)>
<S(swol:differentIndividualFrom),S(rdfs:Resource)>
Theorem w5
[(S('swol-sameclassas) . S('rdfs-class)) ,
(S('swol-disjointwith) . S('rdfs-class)) ,
(S('swol-samepropertyas) . S('rdf-property)) ,
(S('swol-sameindividualas) . S('rdfs-resource)) ,
(S('swol-differentindividualfrom) . S('rdfs-resource))]
sub EXT(S('rdfs-domain)) ;
W6: EXT(S(rdfs:range)) contains
<S(swol:sameClassAs),S(rdfs:Class)>,
<S(swol:disjointWith),S(rdfs:Class)>
<S(swol:samePropertyAs),S(rdf:Property)>
<S(swol:sameIndividualAs),S(rdfs:Resource)>
<S(swol:differentIndividualFrom),S(rdfs:Resource)>
Theorem w6
[(S('swol-sameclassas) . S('rdfs-class)) ,
(S('swol-disjointwith) . S('rdfs-class)) ,
(S('swol-samepropertyas) . S('rdf-property)) ,
(S('swol-sameindividualas) . S('rdfs-resource)) ,
(S('swol-differentindividualfrom) . S('rdfs-resource))]
sub EXT(S('rdfs-range)) ;
W7: x in CEXT(S(swol:Class)) -> x in C and CEXT(x) <= R
Theorem w7
x in CEXT(S('swol-class))
-> x in C() and (CEXT(x) sub R() ) ;
W8: x in CEXT(S(swol:ObjectProperty)) -> x in P and EXT(x) <= R x R
Theorem w8
x in CEXT(S('swol-objectproperty))
-> x in P() and (EXT(x) sub (r X r ) ) ;
W9: x in CEXT(S(swol:DatatypeProperty)) -> x in P and EXT(x) <= R x V
Theorem w9
x in CEXT(S('swol-datatypeproperty))
-> x in P() and (EXT(x) sub (r X v ) ) ;
A relation is functional IFF all x,y : x = y iff f(x) = f(y)
Function is-functional(l)
if endp(l) then t
elif rest(l) \ caar(l) then [ ]
else is-functional(rest(l)) ;
W10: x in CEXT(S(swol:UniqueProperty)) -> x in P and EXT(x) is functional
Theorem w10
x in CEXT(S('swol-uniqueproperty))
-> x in P() and is-functional(EXT(x)) ;
Function converse(mapping)
if endp(mapping) then [ ]
else ( (rest(first(mapping)) . first(first(mapping))) . converse(rest(mapping))) ;
W11: x in CEXT(S(swol:UnambiguousProperty))
-> x in CEXT(S(swol:ObjectProperty))
and converse EXT(x) is functional
Theorem w11
x in CEXT(S('swol-unambiguousproperty))
-> x in CEXT(S('swol-objectproperty))
and is-functional(converse(EXT(x))) ;
Use this for now, since the only closures we are considering are empty. I have defined the function, the easy part, but need to prove termination in order to have it accepted by ACL2.
Function transitiveclosure(l) l ;
W12: x in CEXT(S(swol:TransitiveProperty))
-> x in CEXT(S(swol:ObjectProperty))
and EXT(x) o EXT(x) <= EXT(x)
Theorem w12
x in CEXT(S('swol-transitiveproperty))
-> x in CEXT(S('swol-objectproperty))
and (transitiveclosure(EXT(x)) sub EXT(x) ) ;
W13: <x,y> in EXT(S(rdfs:subClassOf))
iff x,y in C\DT and CEXT(x) <= CEXT(y)
Theorem w13a
((x . y) in EXT(S('rdfs-subclassof)) )
-> x in (C() - DT())
and y in (C() - DT())
and (CEXT(x) sub CEXT(y) ) ;
This is a very large, non-intuitive set. I chose not to build the witness. It is computable, if ugly.
W13b unproven
Theorem w13b
x in (C() - DT())
and y in (C() - DT())
and (CEXT(x) sub CEXT(y) )
-> ((x . y) in EXT(S('rdfs-subclassof)) ) ;
W14: <x,y> in EXT(S(swol:sameClassAs))
iff x,y in C\DT and CEXT(x) = CEXT(y)
Theorem w14a
((x . y) in EXT(S('swol-sameclassas)) )
-> x in (C() - DT())
and y in (C() - DT())
and CEXT(x) = CEXT(y) ;
W14b unproven, for the same reasons as W13b.
Theorem w14b
x in (C() - DT())
and y in (C() - DT())
and CEXT(x) = CEXT(y)
-> ((x . y) in EXT(S('swol-sameclassas)) ) ;
W15: <x,y> in EXT(S(swol:disjointWith))
iff x,y in C\DT and CEXT(x)^CEXT(y) =
Theorem w15a
((x y) in EXT(S('swol-disjointwith)) )
-> ([x, y] sub (C() - DT()) )
and null(CEXT(x) intersect CEXT(y))) ;
W15b unproven, for the same reasons as W13b.
Note that classes with no members are disjoint from themselves.
Theorem w15b
([x, y] sub (C() - DT()) )
and null(CEXT(x) intersect CEXT(y))
-> ((x . y) in EXT(S('swol-disjointwith)) ) ;
W16: <x,y> in EXT(S(rdfs:subPropertyOf)) -> x,y in P and EXT(x) <= EXT(y)
Theorem w16
((x . y) in EXT(S('rdfs-subpropertyof)) )
-> ([x, y] sub P() ) and (EXT(x) sub EXT(y) ) ;
W17: <x,y> in EXT(S(swol:samePropertyAs)) -> x,y in P and EXT(x) = EXT(y)
Theorem w17
((x . y) in EXT(S('swol-samepropertyas)) )
-> ([x, y] sub P() ) and EXT(x) = EXT(y) ;
W18: <x,y> in EXT(S(swol:sameIndividualAs)) iff x,y in R and x=y
Theorem w18a
((x . y) in EXT(S('swol-sameindividualas)) )
-> x in R() and y in R() and x = y ;
W18b unproven, for the same reasons as W13b.
Theorem w18b
x in R() and y in R() and x = y
-> ((x . y) in EXT(S('swol-sameindividualas)) ) ;
W19: <x,y> in EXT(S(swol:differentIndividualFrom)) iff x,y in R and x/=y
Theorem w19
((x . y) in EXT(S('swol-differentindividualfrom)) )
-> ([x, y] sub R() ) and x ¬= y ;
W19b unproven, for the same reasons as W13b.
Theorem w19b
([x, y] sub R() ) and x ¬= y
-> ((x . y) in EXT(S('swol-differentindividualfrom)) ) ;
W20: CEXT(S(swol:Thing)) = R
Theorem w20 CEXT(S('swol-thing)) = R() ;
W21: CEXT(S(swol:Nothing)) =
Theorem w21 null(CEXT(S('swol-nothing))) ;
Define Datatype properties.
In-Package("ACL2");
Constant *dt* = '[integerdt];
Constant *du* = '[[integerdt . http://integer]];
Constant *dl* = '[[integerdt lexone lextwo]];
Constant *dv* = '[[integerdt 1 2]];
Constant *dlv* = '[[integerdt [lexone . 1] [lextwo . 2]]];
Property extensions.
*EXT* is partial. In particular, a property with no elements does not need to be contained in this constant, since P with no elements will be indistinguishable from (P . NIL) in *EXT*.
Constant *EXT* =
'[[subclassof
[swolclass . class]
[swolobjectproperty . property]
[swoldatatypeproperty . property]
[swoluniqueproperty . property]
[swolunambiguousproperty . swolobjectproperty]
[swoltransitiveproperty . swolobjectproperty]
[class . resource]
[property . resource]
[swolObjectProperty . swolSamePropertyAs]
[constraintResource . constraintProperty]]
[p1 [p11 . 1]]
[subpropertyof
[swolsameclassas . subclassof]
[swolsamepropertyas . subpropertyof]
[swolobjectproperty . swolsamepropertyas]
[constraintresource . constraintproperty]]
[swolsameclassas
[swolobjectproperty . swolsamepropertyas]
[constraintresource . constraintproperty]]
[swolsamepropertyas]
[swoldatatypeproperty]
[swoluniqueproperty]
[swolunambiguousproperty]
[swoltransitiveproperty]
[swoldisjointwith]
[swolsameindividualas]
[swoldifferentindividualfrom]
[domain
[type . resource]
[subclassof . class]
[subpropertyof . property]
[swolsameclassas . class]
[swoldisjointwith . class]
[swolsamepropertyas . property]
[swolsameindividualas . resource]
[swoldifferentindividualfrom . resource]
[domain . property]
[range . property]]
[range
[type . class]
[subclassof . class]
[subpropertyof . property]
[swolsameclassas . class]
[swoldisjointwith . class]
[swolsamepropertyas . property]
[swolsameindividualas . resource]
[swoldifferentindividualfrom . resource]
[domain . class]
[range . class]]
[swoldatatypeproperty]
[swoluniqueproperty]
[swolunambiguousproperty]
[swoltransitiveproperty]
[type
[class . class]
[class . resource]
[constraintproperty . class]
[constraintproperty . resource]
[constraintproperty . property]
[constraintresource . class]
[constraintresource . resource]
[constraintresource . property]
[literal . class]
[literal . resource]
[property . class]
[property . resource]
[resource . class]
[resource . resource]
[resource . swolThing]
[a . resource]
[b . resource]
[c1 . class]
[c1 . resource]
[c2 . c1]
[c2 . class]
[c2 . resource]
[cinst . c1]
[cinst . c2]
[cinst . class]
[cinst . resource]
[domain . property]
[domain . resource]
[integerdt . class]
[integerdt . resource]
[integerdt . swoldatatype]
[p1 . property]
[p1 . resource]
[p11 . class]
[p11 . resource]
[range . constraintproperty]
[domain . constraintproperty]
[range . constraintresource]
[domain . constraintresource]
[range . property]
[range . resource]
[subclassof . class]
[subclassof . property]
[subclassof . resource]
[subpropertyof . class]
[subpropertyof . property]
[subpropertyof . resource]
[swolclass . class]
[swolclass . resource]
[swoldatatype . class]
[swoldatatype . resource]
[swoldatatypeproperty . class]
[swoldatatypeproperty . property]
[swoldatatypeproperty . resource]
[swoldifferentindividualfrom . class]
[swoldifferentindividualfrom . property]
[swoldifferentindividualfrom . resource]
[swoldisjointwith . class]
[swoldisjointwith . property]
[swoldisjointwith . resource]
[swolobjectproperty . class]
[swolobjectproperty . property]
[swolobjectproperty . resource]
[swolsameclassas . class]
[swolsameclassas . property]
[swolsameclassas . resource]
[swolsameindividualas . class]
[swolsameindividualas . property]
[swolsameindividualas . resource]
[swolsamepropertyas . class]
[swolsamepropertyas . property]
[swolsamepropertyas . resource]
[swoltransitiveproperty . class]
[swoltransitiveproperty . property]
[swoltransitiveproperty . resource]
[swoltransitiveproperty . swolclass]
[swoltransitiveproperty . swolobjectproperty]
[swoltransitiveproperty . swolsamepropertyas]
[swolunambiguousproperty . class]
[swolunambiguousproperty . property]
[swolunambiguousproperty . resource]
[swolunambiguousproperty . swolobjectproperty]
[swolunambiguousproperty . swolsamepropertyas]
[swoluniqueproperty . class]
[swoluniqueproperty . property]
[swoluniqueproperty . resource]
[type . class]
[type . property]
[type . resource]
[swolnothing . swolthing]
[swolthing . swolthing]
[swolthing . resource]
[swolthing . class]
[subclassof . swolthing]
[resource . swolthing]
[p1 . swolthing]
[subpropertyof . swolthing]
[swoldisjointwith . swolthing]
[swolsameindividualas . swolthing]
[swoldifferentindividualfrom . swolthing]
[domain . swolthing]
[range . swolthing]
[type . swolthing]
[c1 . swolthing]
[c2 . swolthing]
[cinst . swolthing]
[p11 . swolthing]
[resource . swolthing]
[property . swolthing]
[class . swolthing]
[literal . swolthing]
[integerdt . swolthing]
[swoldatatype . swolthing]
[constraintresource . swolthing]
[constraintproperty . swolthing]
[swolclass . swolthing]
[swolsameclassas . swolthing]
[swolsamepropertyas . swolthing]
[swolobjectproperty . swolthing]
[swoldatatypeproperty . swolthing]
[swoluniqueproperty . swolthing]
[swolunambiguousproperty . swolthing]
[swoltransitiveproperty . swolthing]
[swolnothing . class]
[swolnothing . resource]
[swolnothing . swolthing]
[p1 . swolthing]
[domain . swolthing]
[range . swolthing]
[a . swolthing]
[b . swolthing]]];
*CEXT* may be partial. But the resource, property and class elements must be complete.
Constant *CEXT* =
'[[c1 c2 cinst]
[c2 cinst]
[cinst]
[p11]
[resource
swolthing swolnothing
resource property class literal constraintresource constraintproperty type
subclassof subpropertyof range domain p1 p11 c1 c2 cinst integerdt swoldatatype
swolclass swolobjectproperty swoldatatypeproperty swoluniqueproperty
swolunambiguousproperty swoltransitiveproperty swolsameclassas swoldisjointwith
swolsamepropertyas swolsameindividualas swoldifferentindividualfrom a b
swoldifferentindividualfrom]
[property
constraintproperty constraintresource
p1 type subclassof subpropertyof range domain swolsameclassas
swolsamepropertyas swoldatatypeproperty swoluniqueproperty swolunambiguousproperty
swoltransitiveproperty swolobjectproperty swolsameclassas swoldisjointwith
swolsamepropertyas swolsameindividualas swoldifferentindividualfrom]
[class type resource literal class c1 c2 cinst property p11 constraintresource
constraintproperty integerdt swoldatatype swolclass swolobjectproperty swolsameclassas
swolsamepropertyas swoldatatypeproperty swoluniqueproperty swolunambiguousproperty
swoltransitiveproperty swolsameindividualas swoldisjointwith
swoldifferentindividualfrom subclassof subpropertyof
swolthing swolnothing ]
[literal 1 2]
[type]
[swolsameindividualas]
[swoldisjointwith]
[swoldifferentindividualfrom]
[subclassof]
[subpropertyof]
[integerdt 1 2]
[swoldatatype integerdt]
[constraintresource range domain]
[constraintproperty range domain]
[swolclass swoltransitiveproperty]
[swolsameclassas]
[swolsamepropertyas swoltransitiveproperty swolunambiguousproperty]
[swolobjectproperty swoltransitiveproperty swolunambiguousproperty]
[swoldatatypeproperty]
[swoluniqueproperty]
[swolunambiguousproperty]
[swoltransitiveproperty]
[swolnothing]
[swolthing subclassof p1 subpropertyof swoldisjointwith swolsameindividualas
swoldifferentindividualfrom domain range type c1 c2 cinst p11 resource property class
literal integerdt swoldatatype constraintresource constraintproperty swolclass
swolsameclassas swolsamepropertyas swolobjectproperty swoldatatypeproperty
swoluniqueproperty swolunambiguousproperty swoltransitiveproperty
swoldifferentindividualfrom swolnothing swolthing a b]];
*S* must be complete, since we construct N from the domain.
Constant *S* = '[[http1 . a] [http2 . b] [rdfs-resource . resource] [rdf-property . property] [rdfs-class . class] [rdfs-literal . literal] [rdfs-constraintresource . constraintresource] [rdfs-constraintproperty . constraintproperty] [rdf-type . type] [rdfs-subclassof . subclassof] [rdfs-subpropertyof . subpropertyof] [rdfs-range . range] [rdfs-domain . domain] [http://integer . integerdt] [swol-datatype . swoldatatype] [swol-class . swolclass] [swol-sameclassas . swolsameclassas] [swol-samepropertyas . swolsamepropertyas] [swol-objectproperty . swolobjectproperty] [swol-datatypeproperty . swoldatatypeproperty] [swol-uniqueproperty . swoluniqueproperty] [swol-unambiguousproperty . swolunambiguousproperty] [swol-transitiveproperty . swoltransitiveproperty] [swol-disjointwith . swoldisjointwith] [swol-sameindividualas . swolsameindividualas] [swol-differentindividualfrom . swoldifferentindividualfrom] [swol-thing . swolthing] [swol-nothing . swolnothing]];
Definitions in the theory of sets
Copyright (C) 1997 Computational Logic, Inc.
This book is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.
This book is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this book; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
Written by: Bill Bevier (bevier@cli.com)
Computational Logic, Inc.
1717 West Sixth Street, Suite 290
Austin, TX 78703-4776 U.S.A.
In-Package("ACL2");
This theory includes functions which treat lists as sets. In the theory of lists and the theory of alists, we provide three versions of each function based on three different notions of equality: EQL, EQ and EQUAL. In this theory, however, we provide only the EQUAL version. The main reason for this is mundane: Many of the function names (e.g. UNION and INTERSECTION) are not defined in ACL2, but are blocked from our use because they're in the Common Lisp package.
------------------------------------------------------------
Functions
------------------------------------------------------------
Function Name In Result (supporting function) ACL2 Type ---------------------- ---- ----- adjoin-equal N set intersection-equal N set set-difference-equal Y set union-equal Y set memberp-equal (in) N boolean subsetp-equal (sub) Y boolean set-equal (=s) N boolean setp N boolean
Function adjoin-equal(x, l)
{if x in l then l
else (x . l) }
:guard true-listp(l);
Function x in l {consp(x in l )}
:guard true-listp(l);
Function intersection-equal(x, y)
{if endp(x) then [ ]
elif first(x) in y then (first(x) . intersection-equal(rest(x), y))
else intersection-equal(rest(x), y)}
:guard true-listp(x) and true-listp(y) ;
Function a =s b {(a sub b)and (b sub a ) }
:guard true-listp(a) and true-listp(b) ;
Is l a set?
Function setp-equal(l) {true-listp(l) and no-duplicatesp-equal(l) }
:verify-guards t;
Theorems about functions in the theory of sets
Copyright (C) 1997 Computational Logic, Inc.
This book is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.
This book is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this book; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
Written by: Bill Bevier (bevier@cli.com)
Computational Logic, Inc.
1717 West Sixth Street, Suite 290
Austin, TX 78703-4776 U.S.A.
In-Package("ACL2");
Include("set-defuns");
------------------------------------------------------------
SUBSETP-EQUAL
------------------------------------------------------------
Theorem subsetp-equal-cons {(a sub b ) -> (a sub (x . b) ) };
Theorem subsetp-equal-reflexive {l sub l };
Theorem subsetp-equal-transitive
{(a sub b ) and (b sub c ) -> (a sub c ) }
:rule-classes [ ];
Theorem subsetp-equal-append-crock
{(l1 sub l2 ) -> (l1 @ [x] sub (x . l2) ) };
Theorem subsetp-equal-append2
{(l1 sub l2 ) -> (l1 sub l2 @ l3 ) };
Theorem subsetp-equal-adjoin-equal1
{ (adjoin-equal(x, a) sub b )
= (x in b and (a sub b ) )};
Theorem subsetp-equal-adjoin-equal2
{(a sub b ) -> (a sub adjoin-equal(x, b) ) };
Theorem subsetp-equal-intersection-equal
{ (a sub b ) and (a sub c )
-> (a sub intersection-equal(b, c) )};
Theorem subsetp-equal-set-difference-equal
{ (a sub b ) and intersection-equal(a, c) = [ ]
-> (a sub set-difference-equal(b, c) )};
Theorem subsetp-equal-union-equal
{(a sub b ) or (a sub c ) -> (a sub (b U c ) ) };
------------------------------------------------------------
=s SET-EQUAL is an equivalence relation.
------------------------------------------------------------
Theorem set-equal-reflexive {l =s l }
:hints [["Goal" :do-not-induct t]];
Theorem set-equal-symmetric {(a =s b ) -> (b =s a ) }
:rule-classes [ ];
Theorem set-equal-transitive {(a =s b ) and (b =s c ) -> (a =s c ) }
:rule-classes [ ]
:hints [["Goal" :do-not-induct t
:use [[:instance subsetp-equal-transitive
[a := a, b := b, c := c ]]
[:instance subsetp-equal-transitive
[a := c, b := b, c := a ]]]]];
------------------------------------------------------------
MEMBERP-EQUAL
------------------------------------------------------------
Theorem memberp-equal-subsetp-equal
{x in a and (a sub b ) -> x in b) }
:rule-classes [ ];
Theorem memberp-equal-set-equal
{(a =s b ) -> (x in a iff x in b ) }
:rule-classes [ ]
:hints [["Goal" :do-not-induct t
:use [[:instance memberp-equal-subsetp-equal
[x := x, a := a, b := b ]]
[:instance memberp-equal-subsetp-equal
[x := x, a := b, b := a ]]]]];
Theorem memberp-equal-adjoin-equal
{x in adjoin-equal(y, l) iff x = y or x in l };
Theorem memberp-equal-intersection-equal
{ x in intersection-equal(a, b)
iff x in a and x in b };
Theorem memberp-equal-set-difference-equal
{ x in set-difference-equal(a, b)
iff x in a and ¬(x in b) };
Theorem memberp-equal-union-equal
{ x in a U b
iff x in a or x in b };
------------------------------------------------------------
SETP
------------------------------------------------------------
Theorem setp-equal-cons
{setp-equal((x . l) ) = (setp-equal(l) and ¬(x in l) ) }
:hints [["Goal" :in-theory enable(setp-equal)]];
Theorem setp-equal-adjoin-equal
{setp-equal(a) -> setp-equal(adjoin-equal(x, a)) };
local Theorem member-equal-intersection-equal
{ x in intersection-equal(a, b)
iff x in a and x in b };
Theorem setp-equal-intersection-equal
{setp-equal(a) -> setp-equal(intersection-equal(a, b)) };
local Theorem member-equal-set-difference-equal
{ x in set-difference-equal(a, b)
iff x in a and x ¬ in b };
Theorem setp-equal-set-difference-equal
{setp-equal(a) -> setp-equal(set-difference-equal(a, b)) };
local Theorem member-equal-union-equal
{x in (a U b ) iff x in a or x in b };
Theorem setp-equal-union-equal
{setp-equal(a) and setp-equal(b) -> setp-equal(a U b ) };
------------------------------------------------------------
INTERSECTION-EQUAL
------------------------------------------------------------
Theorem intersection-equal-nil {intersection-equal(a, [ ]) = [ ] };
Theorem subsetp-equal-intersection-equal-instance
{true-listp(a) and (a sub b ) -> intersection-equal(a, b) = a };
Theorem intersection-equal-identity
{true-listp(a) -> intersection-equal(a, a) = a }
:hints [["Goal" :do-not-induct t]];
------------------------------------------------------------
UNION-EQUAL
------------------------------------------------------------
Theorem union-equal-nil {true-listp(a) -> (a U [ ] ) = a };
Theorem subsetp-equal-union-equal-instance
{true-listp(b) and (a sub b ) -> (a U b ) = b };
Theorem union-equal-identity {true-listp(a) -> (a U a ) = a }
:hints [["Goal" :do-not-induct t]];
------------------------------------------------------------
SET-DIFFERENCE-EQUAL
------------------------------------------------------------
Theorem set-difference-equal-nil
{true-listp(a) -> set-difference-equal(a, [ ]) = a };
Theorem subsetp-equal-set-difference-equal-instance
{true-listp(b) and (a sub b ) -> set-difference-equal(a, b) = [ ] };
Theorem set-difference-equal-identity
{true-listp(a) -> set-difference-equal(a, a) = [ ] }
:hints [["Goal" :do-not-induct t]];
Theorem set-difference-equal-cons
{x in b -> set-difference-equal(a, (x . b) ) = set-difference-equal(a, b) };
Theorem set-difference-null-intersection
{ true-listp(a) and intersection-equal(a, b) = [ ]
-> set-difference-equal(a, b) = a };
------------------------------------------------------------
Other Facts
------------------------------------------------------------
local Theorem member-equal-append
{x in a @ b iff x in a or x in b };
Theorem no-duplicatesp-equal-append
{ no-duplicatesp-equal(a @ b )
iff no-duplicatesp-equal(a)
and no-duplicatesp-equal(b)
and ¬(intersection-equal(a, b))};
local Theorem true-listp-append {true-listp(a @ b ) = true-listp(b) };
Theorem setp-equal-append
{ true-listp(a)
-> ( setp-equal(a @ b )
iff setp-equal(a)
and setp-equal(b)
and ¬(intersection-equal(a, b)))}
:hints [["Goal" :do-not-induct t]];
In-Theory(disable(set-equal, setp-equal, adjoin-equal, memberp-equal));
In-Package("ACL2");
Cartesian product helper
Function product1(x, b)
{if ¬(true-listp(b)) or null(b) then [ ]
else (((x . first(b)) ) . product1(x, rest(b))) };
Cartesian product
Function a X b
{if true-listp(a) and true-listp(b) and a and b
then product1(first(a), b) @ (rest(a) X b )
else [ ]};
Assumes a relation is a list of pairs. Note that the "a := expr" forms below are scoped within the enclosing brackets (they are LETs).
Function domain(l)
{if endp(l) then [ ]
else {rest := domain(rest(l));
if consp(first(l))
then if caar(l) in rest then rest
else (caar(l) . rest)
else rest}}
:guard alistp(l);
Function range(l)
{if endp(l) then [ ]
else {rest := range(rest(l));
if consp(first(l))
then if cdar(l) in rest then rest
else (cdar(l) . rest)
else rest}}
:guard alistp(l);
Theorem no-duplicatesdomain {alistp(l) -> no-duplicatesp-equal(domain(l)) };
Theorem no-duplicatesrange {alistp(l) -> no-duplicatesp-equal(range(l)) };
Compute the union of a list of sets.
Assumes all x in l are sets.
Function union-all(l)
{if endp(l) then [ ]
elif consp(first(l)) then first(l) U union-all(rest(l))
else union-all(rest(l))};