contact:="http://www.w3.org/2000/10/swap/pim/contact#".
log:="http://www.w3.org/2000/10/swap/log#".
ont:="http://www.w3.org/2001/10/daml+oil#".
rdf:="http://www.w3.org/1999/02/22-rdf-syntax-ns#".
examples:="http://www.w3.org/2002/03owlt/".

FORALL Mdl @unambig(Mdl) {

FORALL O,P,V O[P->V] <- O[P->V]@Mdl .

FORALL O1,O2,P,V     
	O1[ont:sameIndividualAs->O2] <- 
		P[rdf:type->ont:UnambiguousProperty] and
		O1[P->V] and O2[P->V] .

	FORALL X,Y 
		X[ont:sameIndividualAs->X].
	//reflexivity

	FORALL X,Y
		X[ont:sameIndividualAs->X]<-Y[ont:sameIndividualAs->X].
	//symmetry


	FORALL X,Y,Z 
		X[ont:sameIndividualAs->Z] <- 
			X[ont:sameIndividualAs->Y] and Y[ont:sameIndividualAs->Z].
	//transitivity of ont:sameIndividualAs
}


FORALL rdfmodel @sameIndividual(rdfmodel){ 
	FORALL O,O1,P,V,V1 
		O[P->V] <-
			O[ont:sameIndividualAs->O1]@unambig(rdfmodel) and
			V[ont:sameIndividualAs->V1]@unambig(rdfmodel) and
			O1[P->V1]@rdfmodel.
}

//FORALL O,V <- 
//   O[ont:sameIndividualAs -> V]@unambig(examples:sameGuy).

//FORALL P,O1,O2, V <- P[rdf:type->ont:UnambiguousProperty]@unambig(examples:sameGuy) and
//		O1[P->V]@unambig(examples:sameGuy) and O2[P->V]@unambig(examples:sameGuy).


//FORALL P <- 
//    P[rdf:type->ont:UnambiguousProperty]@unambig(examples:sameGuy).

//FORALL O,P,V <- 
//     O[P -> V]@examples:sameGuy.




FORALL O,X,P,V <- 
     O[P->V]@sameIndividual(examples:sameGuy).