owl : THEORY

BEGIN
	IMPORTING finite_sets

	% --------------------
	% - Type Declaration -
	% --------------------

	RESOURCE: TYPE+

	INDIVIDUAL: TYPE+ = RESOURCE

	DATAVALUE: TYPE+ FROM INDIVIDUAL

	CLASS: TYPE+ FROM RESOURCE

	PROPERTY: TYPE = pred[[RESOURCE,RESOURCE]]

	O_PROPERTY: TYPE+ FROM PROPERTY

	D_PROPERTY: TYPE+ FROM PROPERTY

	% ------------------------
	% - Function Declaration -
	% ------------------------

	instances: [CLASS -> set[INDIVIDUAL]]

	% ------------------------
	% - Variable Declaration -
	% ------------------------

	thing: CLASS
	thing_ax: AXIOM FORALL (i:INDIVIDUAL): member(i,instances(thing))

	nothing: CLASS
	nothing_ax: AXIOM FORALL (i:INDIVIDUAL): NOT member(i,instances(nothing))

	% ------------------------
	% - Axiomatic Definition -
	% ------------------------

	oneOf : [set[INDIVIDUAL] -> CLASS]
	oneOf_ax : AXIOM FORALL (si:set[INDIVIDUAL]),(c:CLASS):
		(oneOf(si) = c IMPLIES instances(c) = si)

	allValuesFrom : [PROPERTY, CLASS -> CLASS]
	allValuesFrom_ax : AXIOM
		FORALL (c1,c2:CLASS),(p:PROPERTY):
			(c1 = allValuesFrom(p,c2) IMPLIES
				FORALL (i1:INDIVIDUAL):
					(member(i1,instances(c1)) IFF
						FORALL (i2:INDIVIDUAL):
							(p(i1,i2) IMPLIES member(i2,instances(c2)))
					)
			)

	someValuesFrom : [PROPERTY, CLASS -> CLASS]
	someValuesFrom_ax : AXIOM
		FORALL (c1,c2:CLASS),(p:PROPERTY):
			(c1 = someValuesFrom(p,c2) IMPLIES
				FORALL (i1:INDIVIDUAL):
					(member(i1,instances(c1)) IFF
						EXISTS (i2:INDIVIDUAL):
							(member(i2,instances(c2)) AND p(i1,i2))
					)
			)

	hasValue : [PROPERTY, INDIVIDUAL -> CLASS]
	hasValue_ax : AXIOM
		FORALL (c:CLASS),(p:PROPERTY),(i:INDIVIDUAL):
			(c = hasValue(p,i) IMPLIES
				FORALL (i1:INDIVIDUAL):
					(member(i1,instances(c)) IFF p(i1,i))
			)

	maxCardinality : [PROPERTY, nat -> CLASS]
	maxCardinality_ax : AXIOM
		FORALL (c:CLASS),(p:PROPERTY),(n:nat):
			(c = maxCardinality(p,n) IMPLIES
				FORALL (i:INDIVIDUAL):
					(member(i,instances(c)) IFF
						EXISTS (s:finite_set[RESOURCE]):
							(card(s) = n AND subset?(image(p,singleton(i)),s))
					)
			)

	minCardinality : [PROPERTY, nat -> CLASS]
	minCardinality_ax : AXIOM
		FORALL (c:CLASS),(p:PROPERTY),(n:nat):
			(c = minCardinality(p,n) IMPLIES
				FORALL (i:INDIVIDUAL):
					(member(i,instances(c)) IFF
						EXISTS (s:finite_set[RESOURCE]):
							(card(s) = n AND subset?(s,image(p,singleton(i))))
					)
			)

	cardinality : [PROPERTY, nat -> CLASS]
	cardinality_ax : AXIOM
		FORALL (c:CLASS),(p:PROPERTY),(n:nat):
			(c = cardinality(p,n) IMPLIES
				FORALL (i:INDIVIDUAL):
					(member(i,instances(c)) IFF
						EXISTS (s:finite_set[RESOURCE]):
							(card(s) = n AND s = image(p,singleton(i)))
					)
			)

	intersectionOf : [list[CLASS] -> CLASS]
	intersectionOf_ax : AXIOM
		FORALL (lc:list[CLASS]),(c:CLASS):
			(c = intersectionOf(lc) IMPLIES
				FORALL (i:INDIVIDUAL):
					(member(i,instances(c)) IFF
						FORALL (sc:CLASS):
							(member(sc,lc) IMPLIES member(i,instances(sc)))
					)
			)

	unionOf : [list[CLASS] -> CLASS]
	unionOf_ax : AXIOM
		FORALL (lc:list[CLASS]),(c:CLASS):
			(c = unionOf(lc) IMPLIES
				FORALL (i:INDIVIDUAL):
					(member(i,instances(c)) IFF
						EXISTS (sc:CLASS):
							(member(sc,lc) AND member(i,instances(sc)))
					)
			)

	complementOf : [CLASS -> CLASS]
	complementOf_ax : AXIOM
		FORALL (c1,c:CLASS):
			(c = complementOf(c1) IMPLIES complement(instances(c1)) = instances(c))

	subClassOf?(c1,c2:CLASS): bool =
	(
		subset?(instances(c1),instances(c2))
	)

	equivalentClass?(c1,c2:CLASS): bool =
	(
		instances(c1) = instances(c2)
	)

	disjointWith?(c1,c2:CLASS): bool =
	(
		disjoint?(instances(c1),instances(c2))
	)

	subPropertyOf?(p1,p2:PROPERTY): bool =
	(
		FORALL (i1,i2:INDIVIDUAL):
			(p1(i1,i2) IMPLIES p2(i1,i2))
	)

	domain?(p:PROPERTY,c:CLASS): bool =
	(
		FORALL (i1,i2:INDIVIDUAL):
			(p(i1,i2) IMPLIES member(i1,instances(c)))
	)

	range?(p:PROPERTY,c:CLASS): bool =
	(
		FORALL (i1,i2:INDIVIDUAL):
			(p(i1,i2) IMPLIES member(i2,instances(c)))
	)

	equivalentProperty?(p1,p2:PROPERTY): bool =
	(
		p1 = p2
	)

	inverseOf?(p1,p2:PROPERTY): bool =
	(
		FORALL (i1,i2:INDIVIDUAL):
			(p1(i1,i2) IFF p2(i2,i1))
	)

	sameAs?(i1,i2:RESOURCE): bool =
	(
		i1 = i2
	)

	sameAs?(p1,p2:PROPERTY): bool =
	(
		p1 = p2
	)

	differentFrom?(i1,i2:INDIVIDUAL): bool =
	(
		NOT sameAs?(i1,i2)
	)

	allDifferent?(li:list[INDIVIDUAL]): RECURSIVE bool =
		CASES li OF
			null: TRUE,
			cons(hd, tl): NOT member(hd,tl) AND allDifferent?(tl)
		ENDCASES
		MEASURE length(li)

	transitiveProperty?(p:PROPERTY): bool =
	(
		transitive?(p)
	)

	functionalProperty?(p:PROPERTY): bool =
	(
		FORALL (r1,r2,r3:RESOURCE): (p(r1,r2) AND p(r1,r3)) IMPLIES r2=r3
	)

	symmetricProperty?(p:PROPERTY): bool =
	(
		symmetric?(p)
	)

	inverseFunctionalProperty?(p:PROPERTY): bool =
	(
		FORALL (r1,r2,r3:RESOURCE): (p(r1,r3) AND p(r2,r3)) IMPLIES r1=r2
	)

END owl