/* -*- Mode: Prolog -*- */ :- module(owl2_model, [ entity/1, declarationAxiom/1, builtin_class/1, is_class/1, class/1, datatype/1, property/1, objectProperty/1, dataProperty/1, annotationProperty/1, individual/1, namedIndividual/1, anonymousIndividual/1, construct/1, axiom/1, classAxiom/1, subClassOf/2, equivalentClasses/1, disjointClasses/1, disjointUnion/2, propertyAxiom/1, subPropertyOf/2, subObjectPropertyOf/2, subDataPropertyOf/2, subAnnotationPropertyOf/2, equivalentProperties/1, equivalentObjectProperties/1, equivalentDataProperties/1, disjointProperties/1, disjointObjectProperties/1, disjointDataProperties/1, inverseProperties/2, propertyDomain/2, objectPropertyDomain/2, dataPropertyDomain/2, annotationPropertyDomain/2, propertyRange/2, objectPropertyRange/2, dataPropertyRange/2, annotationPropertyRange/2, functionalProperty/1, functionalObjectProperty/1, functionalDataProperty/1, inverseFunctionalProperty/1, reflexiveProperty/1, irreflexiveProperty/1, symmetricProperty/1, asymmetricProperty/1, transitiveProperty/1, hasKey/2, fact/1, sameIndividual/1, differentIndividuals/1, classAssertion/2, propertyAssertion/3, objectPropertyAssertion/3, dataPropertyAssertion/3, negativePropertyAssertion/3, negativeObjectPropertyAssertion/3, negativeDataPropertyAssertion/3, annotationAssertion/3, annotation/1, annotation/3, ontologyAnnotation/3, axiomAnnotation/3, annotationAnnotation/3, ontology/1, ontologyDirective/2, ontologyAxiom/2, ontologyImport/2, ontologyVersionInfo/2, axiom_arguments/2, % EXPRESSIOM TYPE CHECKING classExpression/1, objectIntersectionOf/1, objectUnionOf/1, objectComplementOf/1, objectOneOf/1, objectSomeValuesFrom/1, objectAllValuesFrom/1, objectHasValue/1, objectHasSelf/1, objectMinCardinality/1, objectMaxCardinality/1, objectExactCardinality/1, dataSomeValuesFrom/1, dataAllValuesFrom/1, dataHasValue/1, dataMinCardinality/1, dataMaxCardinality/1, dataExactCardinality/1, objectPropertyExpression/1, dataRange/1, dataIntersectionOf/1, dataUnionOf/1, dataComplementOf/1, dataOneOf/1, datatypeRestriction/1, axiompred/1, anyPropertyAssertion/3, equivalent_to/2, disjoint_with/2, labelAnnotation_value/2, axiom_directly_about/2, axiom_directly_references/2, axiom_about/2, axiom_references/2, axiom_contains_expression/2, axiom_contains_expression/3, referenced_description/1, assert_axiom/1, assert_axiom/2, retract_axiom/1, retract_axiom/2, retract_all_axioms/0, owl2_model_init/0, consult_axioms/1, axiom_type/2, valid_axiom/1, is_valid_axiom/1 ]). %:- require([ is_list/1 % , current_prolog_flag/2 % , forall/2 % , debug/3 % ]). :- use_module(library(lists),[member/2]). %% axiompred(?PredSpec) % @param PredSpec Predicate/Arity % (metamodeling) true if PredSpec is a predicate that defines an axiom :- multifile axiompred/1. :- discontiguous(valid_axiom/1). :- discontiguous(axiompred/1). :- discontiguous(axiom_arguments/2). builtin_class('http://www.w3.org/2002/07/owl#Thing'). builtin_class('http://www.w3.org/2002/07/owl#Nothing'). is_class(C) :- class(C). is_class(C) :- builtin_class(C). % TODO: hasKey /**************************************** AXIOMS ****************************************/ %% entity(?IRI) % the fundamental building blocks of owl 2 ontologies, and they define the vocabulary (the named terms) of an ontology % % @see individual/1, property/1, class/1, datatype/1 entity(A) :- individual(A). entity(A) :- property(A). entity(A) :- class(A). entity(A) :- datatype(A). axiom_arguments(entity,[iri]). valid_axiom(entity(A)) :- subsumed_by([A],[iri]). %declarationAxiom(individual(A)) :- individual(A). % TODO - check this declarationAxiom(namedIndividual(A)) :- namedIndividual(A). declarationAxiom(objectProperty(A)) :- objectProperty(A). declarationAxiom(dataProperty(A)) :- dataProperty(A). declarationAxiom(annotationProperty(A)) :- annotationProperty(A). % VV added 9/3/2010 declarationAxiom(class(A)) :- class(A). declarationAxiom(datatype(A)) :- datatype(A). % TODO: check. here we treat the ontology declaration as an axiom; % this liberal definition of axiom allows us to iterate over axiom/1 % to find every piece of information in the ontology. declarationAxiom(ontology(A)) :- ontology(A). %% class(?IRI) % Classes can be understood as sets of individuals :- dynamic(class/1). :- multifile(class/1). axiompred(class/1). axiom_arguments(class,[iri]). valid_axiom(class(A)) :- subsumed_by([A],[iri]). %% datatype(?IRI) % Datatypes are entities that refer to sets of values described by a datatype map :- dynamic(datatype/1). :- multifile(datatype/1). axiompred(datatype/1). axiom_arguments(datatype,[iri]). valid_axiom(datatype(A)) :- subsumed_by([A],[iri]). %% property(?IRI) % Properties connect individuals with either other individuals or with literals % % @see dataProperty/1, objectProperty/1, annotationProperty/1 property(A) :- dataProperty(A). property(A) :- objectProperty(A). property(A) :- annotationProperty(A). axiom_arguments(property,[iri]). valid_axiom(property(A)) :- subsumed_by([A],[iri]). %% objectProperty(?IRI) % Object properties connect pairs of individuals :- dynamic(objectProperty/1). :- multifile(objectProperty/1). axiompred(objectProperty/1). axiom_arguments(objectProperty,[iri]). valid_axiom(objectProperty(A)) :- subsumed_by([A],[iri]). %% dataProperty(?IRI) % Data properties connect individuals with literals. In some knowledge representation systems, functional data properties are called attributes. :- dynamic(dataProperty/1). :- multifile(dataProperty/1). axiompred(dataProperty/1). axiom_arguments(dataProperty,[iri]). valid_axiom(dataProperty(A)) :- subsumed_by([A],[iri]). %% annotationProperty(?IRI) % Annotation properties can be used to provide an annotation for an ontology, axiom, or an IRI :- dynamic(annotationProperty/1). :- multifile(annotationProperty/1). axiompred(annotationProperty/1). axiom_arguments(annotationProperty,[iri]). valid_axiom(annotationProperty(A)) :- subsumed_by([A],[iri]). %% individual(?IRI) % Individuals represent actual objects from the domain being modeled % @see anonymousIndividual/1, namedIndividual/1 individual(A) :- anonymousIndividual(A). individual(A) :- namedIndividual(A). %individual(A) :- nonvar(A),iri(A),\+property(A),\+class(A),\+ontology(A). % TODO: check: make individuals the default axiom_arguments(individual,[iri]). valid_axiom(individual(A)) :- subsumed_by([A],[iri]). %% namedIndividual(?IRI) % Named individuals are given an explicit name that can be used in any ontology in the import closure to refer to the same individual :- dynamic(namedIndividual/1). :- multifile(namedIndividual/1). axiompred(namedIndividual/1). axiom_arguments(namedIndividual,[iri]). valid_axiom(namedIndividual(A)) :- subsumed_by([A],[iri]). %% anonymousIndividual(?IRI) % Anonymous individuals are local to the ontology they are contained in. Analagous to bnodes % @see construct/1 :- dynamic(anonymousIndividual/1). :- multifile(anonymousIndividual/1). axiompred(anonymousIndividual/1). axiom_arguments(anonymousIndividual,[iri]). valid_axiom(anonymousIndividual(A)) :- subsumed_by([A],[iri]). %% construct(?IRI) % @see axiom/1, annotation/1, ontology/1 construct(A) :- axiom(A). construct(A) :- annotation(A). construct(A) :- ontology(A). axiom_arguments(construct,[iri]). valid_axiom(construct(A)) :- subsumed_by([A],[iri]). %% axiom(?Axiom) % The main component of an OWL 2 ontology is a set of axioms - statements that say what is true in the domain being modeled. % @see classAxiom/1, propertyAxiom/1, fact/1 axiom(A) :- classAxiom(A). axiom(A) :- propertyAxiom(A). axiom(hasKey(A,B)) :- hasKey(A,B). axiom(A) :- fact(A). axiom(A) :- declarationAxiom(A). %axiom(annotation(A,B,C)) :- % annotation(A,B,C). % CJM-treat annotations as axioms axiom_arguments(axiom,[axiom]). valid_axiom(axiom(A)) :- subsumed_by([A],[axiom]). %% classAxiom(?Axiom) % OWL 2 provides axioms that allow relationships to be established between class expressions. This predicate reifies the actual axiom % @see equivalentClasses/1, disjointClasses/1, subClassOf/2, disjointUnion/2 classAxiom(equivalentClasses(A)) :- equivalentClasses(A). classAxiom(disjointClasses(A)) :- disjointClasses(A). classAxiom(subClassOf(A, B)) :- subClassOf(A, B). classAxiom(disjointUnion(A, B)) :- disjointUnion(A, B). axiom_arguments(classAxiom,[axiom]). valid_axiom(classAxiom(A)) :- subsumed_by([A],[axiom]). %% subClassOf(?SubClass:ClassExpression, ?SuperClass:ClassExpression) % A subclass axiom SubClassOf( CE1 CE2 ) states that the class expression CE1 is a subclass of the class expression CE2 % % @param SubClass a classExpression/1 representing the more specific class % @param SuperClass a classExpression/1 representing the more general class :- dynamic(subClassOf/2). :- multifile(subClassOf/2). axiompred(subClassOf/2). axiom_arguments(subClassOf,[classExpression, classExpression]). valid_axiom(subClassOf(A, B)) :- subsumed_by([A, B],[classExpression, classExpression]). %% equivalentClasses(?ClassExpressions:set(ClassExpression)) % An equivalent classes axiom EquivalentClasses( CE1 ... CEn ) states that all of the class expressions CEi, 1 <= i <= n, are semantically equivalent to each other. :- dynamic(equivalentClasses/1). :- multifile(equivalentClasses/1). axiompred(equivalentClasses/1). axiom_arguments(equivalentClasses,[set(classExpression)]). valid_axiom(equivalentClasses(A)) :- subsumed_by([A],[set(classExpression)]). %% disjointClasses(?ClassExpressions:set(ClassExpression)) % A disjoint classes axiom DisjointClasses( CE1 ... CEn ) states that all of the class expressions CEi, 1 <= i <= n, are pairwise disjoint; that is, no individual can be at the same time an instance of both CEi and CEj for i != j :- dynamic(disjointClasses/1). :- multifile(disjointClasses/1). axiompred(disjointClasses/1). axiom_arguments(disjointClasses,[set(classExpression)]). valid_axiom(disjointClasses(A)) :- subsumed_by([A],[set(classExpression)]). %% disjointUnion(?ClassExpression, ?ClassExpressions:set(ClassExpression)) % A disjoint union axiom DisjointUnion( C CE1 ... CEn ) states that a class C is a disjoint union of the class expressions CEi, 1 <= i <= n, all of which are pairwise disjoint. :- dynamic(disjointUnion/2). :- multifile(disjointUnion/2). axiompred(disjointUnion/2). axiom_arguments(disjointUnion,[classExpression,set(classExpression)]). valid_axiom(disjointUnion(A,B)) :- subsumed_by([A,B],[classExpression,set(classExpression)]). %% propertyAxiom(?Axiom) % OWL 2 provides axioms that can be used to characterize and establish relationships between object property expressions. This predicate reifies the actual axiom % % @see symmetricProperty/1, inverseFunctionalProperty/1, transitiveProperty/1, asymmetricProperty/1, subPropertyOf/2, functionalProperty/1, irreflexiveProperty/1, disjointProperties/1, propertyDomain/2, reflexiveProperty/1, propertyRange/2, equivalentProperties/1, inverseProperties/2 propertyAxiom(symmetricProperty(A)) :- symmetricProperty(A). propertyAxiom(inverseFunctionalProperty(A)) :- inverseFunctionalProperty(A). propertyAxiom(transitiveProperty(A)) :- transitiveProperty(A). propertyAxiom(asymmetricProperty(A)) :- asymmetricProperty(A). propertyAxiom(subPropertyOf(A, B)) :- subPropertyOf(A, B). propertyAxiom(functionalProperty(A)) :- functionalProperty(A). propertyAxiom(irreflexiveProperty(A)) :- irreflexiveProperty(A). propertyAxiom(disjointProperties(A)) :- disjointProperties(A). propertyAxiom(propertyDomain(A, B)) :- propertyDomain(A, B). propertyAxiom(reflexiveProperty(A)) :- reflexiveProperty(A). propertyAxiom(propertyRange(A, B)) :- propertyRange(A, B). propertyAxiom(equivalentProperties(A)) :- equivalentProperties(A). propertyAxiom(inverseProperties(A, B)) :- inverseProperties(A, B). axiom_arguments(propertyAxiom,[axiom]). valid_axiom(propertyAxiom(A)) :- subsumed_by([A],[axiom]). %% subPropertyOf(?Sub:PropertyExpression, ?Super:ObjectPropertyExpression) % subproperty axioms are analogous to subclass axioms % (extensional predicate - can be asserted) :- dynamic(subPropertyOf/2). :- multifile(subPropertyOf/2). axiompred(subPropertyOf/2). axiom_arguments(subPropertyOf,[propertyExpression, objectPropertyExpression]). valid_axiom(subPropertyOf(A, B)) :- subsumed_by([A, B],[propertyExpression, objectPropertyExpression]). %% subObjectPropertyOf(?Sub:ObjectPropertyExpressionOrChain, ?Super:ObjectPropertyExpression) % The basic form is SubPropertyOf( OPE1 OPE2 ). This axiom states that the object property expression OPE1 is a subproperty of the object property expression OPE2 - that is, if an individual x is connected by OPE1 to an individual y, then x is also connected by OPE2 to y. The more complex form is SubPropertyOf( PropertyChain( OPE1 ... OPEn ) OPE ). This axiom states that, if an individual x is connected by a sequence of object property expressions OPE1, ..., OPEn with an individual y, then x is also connected with y by the object property expression OPE subObjectPropertyOf(A, B) :- subPropertyOf(A, B),subsumed_by([A, B],[objectPropertyExpressionOrChain, objectPropertyExpression]). axiom_arguments(subObjectPropertyOf,[objectPropertyExpressionOrChain, objectPropertyExpression]). valid_axiom(subObjectPropertyOf(A, B)) :- subsumed_by([A, B],[objectPropertyExpressionOrChain, objectPropertyExpression]). %% subDataPropertyOf(?Sub:DataPropertyExpression, ?Super:DataPropertyExpression) % A data subproperty axiom SubPropertyOf( DPE1 DPE2 ) states that the data property expression DPE1 is a subproperty of the data property expression DPE2 - that is, if an individual x is connected by OPE1 to a literal y, then x is connected by OPE2 to y as well. subDataPropertyOf(A, B) :- subPropertyOf(A, B),subsumed_by([A, B],[dataPropertyExpression, dataPropertyExpression]). axiom_arguments(subDataPropertyOf,[dataPropertyExpression, dataPropertyExpression]). valid_axiom(subDataPropertyOf(A, B)) :- subsumed_by([A, B],[dataPropertyExpression, dataPropertyExpression]). %% subAnnotationPropertyOf(?Sub:AnnotationProperty, ?Super:AnnotationProperty) % An annotation subproperty axiom SubPropertyOf( AP1 AP2 ) states that the annotation property AP1 is a subproperty of the annotation property AP2 subAnnotationPropertyOf(A, B) :- subPropertyOf(A, B),subsumed_by([A, B],[annotationProperty, annotationProperty]). axiom_arguments(subAnnotationPropertyOf,[annotationProperty, annotationProperty]). valid_axiom(subAnnotationPropertyOf(A, B)) :- subsumed_by([A, B],[annotationProperty, annotationProperty]). %% equivalentProperties(?PropertyExpressions:set(PropertyExpression)) % An equivalent object properties axiom EquivalentProperties( OPE1 ... OPEn ) states that all of the object property expressions OPEi, 1 <= i <= n, are semantically equivalent to each other % (extensional predicate - can be asserted) :- dynamic(equivalentProperties/1). :- multifile(equivalentProperties/1). axiompred(equivalentProperties/1). axiom_arguments(equivalentProperties,[set(propertyExpression)]). valid_axiom(equivalentProperties(A)) :- subsumed_by([A],[set(propertyExpression)]). %% equivalentObjectProperties(?PropertyExpressions:set(ObjectPropertyExpression)) % An equivalent object properties axiom EquivalentObjectProperties( OPE1 ... OPEn ) states that all of the object property expressions OPEi, 1 <= i <= n, are semantically equivalent to each other equivalentObjectProperties(A) :- equivalentProperties(A),subsumed_by([A],[set(objectPropertyExpression)]). axiom_arguments(equivalentObjectProperties,[set(objectPropertyExpression)]). valid_axiom(equivalentObjectProperties(A)) :- subsumed_by([A],[set(objectPropertyExpression)]). %% equivalentDataProperties(?PropertyExpressions:set(DataPropertyExpression)) % An equivalent data properties axiom EquivalentProperties( DPE1 ... DPEn ) states that all the data property expressions DPEi, 1 <= i <= n, are semantically equivalent to each other. This axiom allows one to use each DPEi as a synonym for each DPEj - that is, in any expression in the ontology containing such an axiom, DPEi can be replaced with DPEj without affecting the meaning of the ontology equivalentDataProperties(A) :- equivalentProperties(A),subsumed_by([A],[set(dataPropertyExpression)]). axiom_arguments(equivalentDataProperties,[set(dataPropertyExpression)]). valid_axiom(equivalentDataProperties(A)) :- subsumed_by([A],[set(dataPropertyExpression)]). %% disjointProperties(?PropertyExpressions:set(PropertyExpression)) % A disjoint properties axiom DisjointProperties( PE1 ... PEn ) states that all of the property expressions PEi, 1 <= i <= n, are pairwise disjoint % (extensional predicate - can be asserted) :- dynamic(disjointProperties/1). :- multifile(disjointProperties/1). axiompred(disjointProperties/1). axiom_arguments(disjointProperties,[set(propertyExpression)]). valid_axiom(disjointProperties(A)) :- subsumed_by([A],[set(propertyExpression)]). %% disjointObjectProperties(?PropertyExpressions:set(ObjectPropertyExpression)) % A disjoint object properties axiom DisjointProperties( OPE1 ... OPEn ) states that all of the object property expressions OPEi, 1 <= i <= n, are pairwise disjoint; that is, no individual x can be connected to an individual y by both OPEi and OPEj for i != j. disjointObjectProperties(A) :- disjointProperties(A),subsumed_by([A],[set(objectPropertyExpression)]). axiom_arguments(disjointObjectProperties,[set(objectPropertyExpression)]). valid_axiom(disjointObjectProperties(A)) :- subsumed_by([A],[set(objectPropertyExpression)]). %% disjointDataProperties(?PropertyExpressions:set(DataPropertyExpression)) % A disjoint data properties axiom DisjointProperties( DPE1 ... DPEn ) states that all of the data property expressions DPEi, 1 <= i <= n, are pairwise disjoint; that is, no individual x can be connected to a literal y by both DPEi and DPEj for i !- j. disjointDataProperties(A) :- disjointProperties(A),subsumed_by([A],[set(dataPropertyExpression)]). axiom_arguments(disjointDataProperties,[set(dataPropertyExpression)]). valid_axiom(disjointDataProperties(A)) :- subsumed_by([A],[set(dataPropertyExpression)]). %% inverseProperties(?ObjectPropertyExpression1:ObjectPropertyExpression, ?ObjectPropertyExpression2:ObjectPropertyExpression) % An inverse object properties axiom InverseProperties( OPE1 OPE2 ) states that the object property expression OPE1 is an inverse of the object property expression OPE2 % (note there are no inverse data properties, as literals are not connected to individuals) % Example: % =|inverseProperties(partOf,hasPart)|= % (extensional predicate - can be asserted) :- dynamic(inverseProperties/2). :- multifile(inverseProperties/2). axiompred(inverseProperties/2). axiom_arguments(inverseProperties,[objectPropertyExpression, objectPropertyExpression]). valid_axiom(inverseProperties(A, B)) :- subsumed_by([A, B],[objectPropertyExpression, objectPropertyExpression]). %% propertyDomain(?PropertyExpression, ?CE) % A property domain axiom PropertyDomain( PE CE ) states that the % domain of the property expression PE is CE % (extensional predicate - can be asserted) :- dynamic(propertyDomain/2). :- multifile(propertyDomain/2). axiompred(propertyDomain/2). axiom_arguments(propertyDomain,[propertyExpression, classExpression]). valid_axiom(propertyDomain(A, B)) :- subsumed_by([A, B],[propertyExpression, classExpression]). %% objectPropertyDomain(?ObjectPropertyExpression, ?ClassExpression) % An object property domain axiom PropertyDomain( OPE CE ) states that the domain of the object property expression OPE is the class expression CE - that is, if an individual x is connected by OPE with some other individual, then x is an instance of CE objectPropertyDomain(A, B) :- propertyDomain(A, B),subsumed_by([A, B],[objectPropertyExpression, classExpression]). axiom_arguments(objectPropertyDomain,[objectPropertyExpression, classExpression]). valid_axiom(objectPropertyDomain(A, B)) :- subsumed_by([A, B],[objectPropertyExpression, classExpression]). %% dataPropertyDomain(?DataPropertyExpression, ?ClassExpression) % A data property domain axiom PropertyDomain( DPE CE ) states that the domain of the data property expression DPE is the class expression CE - that is, if an individual x is connected by DPE with some literal, then x is an instance of CE dataPropertyDomain(A, B) :- propertyDomain(A, B),subsumed_by([A, B],[dataPropertyExpression, classExpression]). axiom_arguments(dataPropertyDomain,[dataPropertyExpression, classExpression]). valid_axiom(dataPropertyDomain(A, B)) :- subsumed_by([A, B],[dataPropertyExpression, classExpression]). %% annotationPropertyDomain(?AnnotationProperty, ?IRI) % An annotation property domain axiom PropertyDomain( AP U ) states that the domain of the annotation property AP is the IRI U. Such axioms have no effect on the Direct Semantics of OWL 2 annotationPropertyDomain(A, B) :- propertyDomain(A, B),subsumed_by([A, B],[annotationProperty, iri]). axiom_arguments(annotationPropertyDomain,[annotationProperty, iri]). valid_axiom(annotationPropertyDomain(A, B)) :- subsumed_by([A, B],[annotationProperty, iri]). %% propertyRange(?PropertyExpression, ?ClassExpression) % An object property domain axiom PropertyRange( OPE CE ) states that the domain of the object property expression OPE is the class expression CE - that is, if an individual x is connected by OPE with some other individual, then x is an instance of CE % (extensional predicate - can be asserted) :- dynamic(propertyRange/2). :- multifile(propertyRange/2). axiompred(propertyRange/2). axiom_arguments(propertyRange,[propertyExpression, classExpression]). valid_axiom(propertyRange(A, B)) :- subsumed_by([A, B],[propertyExpression, classExpression]). %% objectPropertyRange(?ObjectPropertyExpression, ?ClassExpression) % An object property domain axiom PropertyRange( OPE CE ) states that the domain of the object property expression OPE is the class expression CE - that is, if an individual x is connected by OPE with some other individual, then x is an instance of CE objectPropertyRange(A, B) :- propertyRange(A, B),subsumed_by([A, B],[objectPropertyExpression, classExpression]). axiom_arguments(objectPropertyRange,[objectPropertyExpression, classExpression]). valid_axiom(objectPropertyRange(A, B)) :- subsumed_by([A, B],[objectPropertyExpression, classExpression]). %% dataPropertyRange(?ObjectPropertyExpression, ?DataRange) % A data property range axiom PropertyRange( DPE DR ) states that the range of the data property expression DPE is the data range DR - that is, if some individual is connected by DPE with a literal x, then x is in DR. The arity of DR MUST be one dataPropertyRange(A, B) :- propertyRange(A, B),subsumed_by([A, B],[dataPropertyExpression, dataRange]). axiom_arguments(dataPropertyRange,[objectPropertyExpression, dataRange]). valid_axiom(dataPropertyRange(A, B)) :- subsumed_by([A, B],[objectPropertyExpression, dataRange]). %% annotationPropertyRange(?AnnotationProperty, ?IRI) % An annotation property range axiom PropertyRange( AP U ) states that the range of the annotation property AP is the IRI U. Such axioms have no effect on the Direct Semantics of OWL 2 annotationPropertyRange(A, B) :- propertyRange(A, B),subsumed_by([A, B],[annotationProperty, iri]). axiom_arguments(annotationPropertyRange,[annotationProperty, iri]). valid_axiom(annotationPropertyRange(A, B)) :- subsumed_by([A, B],[annotationProperty, iri]). %% functionalProperty(?PropertyExpression) % An object property functionality axiom FunctionalProperty( OPE ) states that the object property expression OPE is functional - that is, for each individual x, there can be at most one distinct individual y such that x is connected by OPE to y % (extensional predicate - can be asserted) :- dynamic(functionalProperty/1). :- multifile(functionalProperty/1). axiompred(functionalProperty/1). axiom_arguments(functionalProperty,[propertyExpression]). valid_axiom(functionalProperty(A)) :- subsumed_by([A],[propertyExpression]). %% functionalObjectProperty(?ObjectPropertyExpression) % An object property functionality axiom FunctionalProperty( OPE ) states that the object property expression OPE is functional - that is, for each individual x, there can be at most one distinct individual y such that x is connected by OPE to y functionalObjectProperty(A) :- functionalProperty(A),subsumed_by([A],[objectPropertyExpression]). axiom_arguments(functionalObjectProperty,[objectPropertyExpression]). valid_axiom(functionalObjectProperty(A)) :- subsumed_by([A],[objectPropertyExpression]). %% functionalDataProperty(?DataPropertyExpression) % A data property functionality axiom FunctionalProperty( DPE ) states that the data property expression DPE is functional - that is, for each individual x, there can be at most one distinct literal y such that x is connected by DPE with y functionalDataProperty(A) :- functionalProperty(A),subsumed_by([A],[dataPropertyExpression]). axiom_arguments(functionalDataProperty,[dataPropertyExpression]). valid_axiom(functionalDataProperty(A)) :- subsumed_by([A],[dataPropertyExpression]). %% inverseFunctionalProperty(?ObjectPropertyExpression) % An object property inverse functionality axiom InverseFunctionalProperty( OPE ) states that the object property expression OPE is inverse-functional - that is, for each individual x, there can be at most one individual y such that y is connected by OPE with x. Note there are no InverseFunctional DataProperties :- dynamic(inverseFunctionalProperty/1). :- multifile(inverseFunctionalProperty/1). axiompred(inverseFunctionalProperty/1). axiom_arguments(inverseFunctionalProperty,[objectPropertyExpression]). valid_axiom(inverseFunctionalProperty(A)) :- subsumed_by([A],[objectPropertyExpression]). %% reflexiveProperty(?ObjectPropertyExpression) % An object property reflexivity axiom ReflexiveProperty( OPE ) states that the object property expression OPE is reflexive - that is, each individual is connected by OPE to itself :- dynamic(reflexiveProperty/1). :- multifile(reflexiveProperty/1). axiompred(reflexiveProperty/1). axiom_arguments(reflexiveProperty,[objectPropertyExpression]). valid_axiom(reflexiveProperty(A)) :- subsumed_by([A],[objectPropertyExpression]). %% irreflexiveProperty(?ObjectPropertyExpression) % An object property reflexivity axiom ReflexiveProperty( OPE ) states that the object property expression OPE is reflexive - that is, no individual is connected by OPE to itsel :- dynamic(irreflexiveProperty/1). :- multifile(irreflexiveProperty/1). axiompred(irreflexiveProperty/1). axiom_arguments(irreflexiveProperty,[objectPropertyExpression]). valid_axiom(irreflexiveProperty(A)) :- subsumed_by([A],[objectPropertyExpression]). %% symmetricProperty(?ObjectPropertyExpression) % An object property symmetry axiom SymmetricProperty( OPE ) states that the object property expression OPE is symmetric - that is, if an individual x is connected by OPE to an individual y, then y is also connected by OPE to x :- dynamic(symmetricProperty/1). :- multifile(symmetricProperty/1). axiompred(symmetricProperty/1). axiom_arguments(symmetricProperty,[objectPropertyExpression]). valid_axiom(symmetricProperty(A)) :- subsumed_by([A],[objectPropertyExpression]). %% asymmetricProperty(?ObjectPropertyExpression) % An object property asymmetry axiom AsymmetricProperty( OPE ) states that the object property expression OPE is asymmetric - that is, if an individual x is connected by OPE to an individual y, then y cannot be connected by OPE to x :- dynamic(asymmetricProperty/1). :- multifile(asymmetricProperty/1). axiompred(asymmetricProperty/1). axiom_arguments(asymmetricProperty,[objectPropertyExpression]). valid_axiom(asymmetricProperty(A)) :- subsumed_by([A],[objectPropertyExpression]). %% transitiveProperty(?ObjectPropertyExpression) % An object property transitivity axiom TransitiveProperty( OPE ) states that the object property expression OPE is transitive - that is, if an individual x is connected by OPE to an individual y that is connected by OPE to an individual z, then x is also connected by OPE to z :- dynamic(transitiveProperty/1). :- multifile(transitiveProperty/1). axiompred(transitiveProperty/1). axiom_arguments(transitiveProperty,[objectPropertyExpression]). valid_axiom(transitiveProperty(A)) :- subsumed_by([A],[objectPropertyExpression]). %% hasKey(?ClassExpression,?PropertyExpression) % A key axiom HasKey( CE PE1 ... PEn ) states that each (named) instance of the class expression CE is uniquely identified by the (data or object) property expressions PEi - that is, no two distinct (named) instances of CE can coincide on the values of all property expressions PEi :- dynamic(hasKey/2). :- multifile(hasKey/2). axiompred(hasKey/2). axiom_arguments(hasKey,[classExpression,propertyExpression]). valid_axiom(hasKey(CE,PE)) :- subsumed_by([CE,PE],[classExpression,propertyExpression]). %% fact(?Axiom) % OWL 2 supports a rich set of axioms for stating assertions - axioms about individuals that are often also called facts. The fact/1 predicate reifies the fact predicate % % @see annotationAssertion/3, differentIndividuals/1, negativePropertyAssertion/3, propertyAssertion/3, sameIndividual/1, classAssertion/2 fact(annotationAssertion(A, B, C)) :- annotationAssertion(A, B, C). fact(differentIndividuals(A)) :- differentIndividuals(A). fact(negativePropertyAssertion(A, B, C)) :- negativePropertyAssertion(A, B, C). fact(propertyAssertion(A, B, C)) :- propertyAssertion(A, B, C). fact(sameIndividual(A)) :- sameIndividual(A). fact(classAssertion(A, B)) :- classAssertion(A, B). axiom_arguments(fact,[axiom]). valid_axiom(fact(A)) :- subsumed_by([A],[axiom]). %% sameIndividual(?Individuals:set(Individual)) % An individual equality axiom SameIndividual( a1 ... an ) states that all of the individuals ai, 1 <= i <= n, are equal to each other. % note that despite the name of this predicate, it accepts a list of individuals as argument :- dynamic(sameIndividual/1). :- multifile(sameIndividual/1). axiompred(sameIndividual/1). axiom_arguments(sameIndividual,[set(individual)]). valid_axiom(sameIndividual(A)) :- subsumed_by([A],[set(individual)]). %% differentIndividuals(?Individuals:set(Individual)) % An individual inequality axiom DifferentIndividuals( a1 ... an ) states that all of the individuals ai, 1 <= i <= n, are different from each other :- dynamic(differentIndividuals/1). :- multifile(differentIndividuals/1). axiompred(differentIndividuals/1). axiom_arguments(differentIndividuals,[set(individual)]). valid_axiom(differentIndividuals(A)) :- subsumed_by([A],[set(individual)]). %% classAssertion(?ClassExpression, ?Individual) % A class assertion ClassAssertion( CE a ) states that the individual a is an instance of the class expression CE :- dynamic(classAssertion/2). :- multifile(classAssertion/2). axiompred(classAssertion/2). axiom_arguments(classAssertion,[classExpression, individual]). valid_axiom(classAssertion(A, B)) :- subsumed_by([A, B],[classExpression, individual]). %% propertyAssertion(?PropertyExpression, ?SourceIndividual:Individual, ?TargetIndividual:Individual) % A positive object property assertion PropertyAssertion( OPE a1 a2 ) states that the individual a1 is connected by the object property expression OPE to the individual a2 % (extensional predicate - can be asserted) :- dynamic(propertyAssertion/3). :- multifile(propertyAssertion/3). axiompred(propertyAssertion/3). axiom_arguments(propertyAssertion,[propertyExpression, individual, individual]). valid_axiom(propertyAssertion(A, B, C)) :- subsumed_by([A, B, C],[propertyExpression, individual, individual]). %% objectPropertyAssertion(?ObjectPropertyExpression, ?SourceIndividual:Individual, ?TargetIndividual:Individual) % A positive object property assertion PropertyAssertion( OPE a1 a2 ) states that the individual a1 is connected by the object property expression OPE to the individual a2 objectPropertyAssertion(A, B, C) :- propertyAssertion(A, B, C),subsumed_by([A, B, C],[objectPropertyExpression, individual, individual]). axiom_arguments(objectPropertyAssertion,[objectPropertyExpression, individual, individual]). valid_axiom(objectPropertyAssertion(A, B, C)) :- subsumed_by([A, B, C],[objectPropertyExpression, individual, individual]). %% dataPropertyAssertion(?ObjectPropertyExpression, ?SourceIndividual:Individual, ?TargetValue:Literal) % A positive data property assertion PropertyAssertion( DPE a lt ) states that the individual a is connected by the data property expression DPE to the literal lt dataPropertyAssertion(A, B, C) :- propertyAssertion(A, B, C),subsumed_by([A, B, C],[dataPropertyExpression, individual, literal]). axiom_arguments(dataPropertyAssertion,[objectPropertyExpression, individual, literal]). valid_axiom(dataPropertyAssertion(A, B, C)) :- subsumed_by([A, B, C],[dataPropertyExpression, individual, literal]). %% negativePropertyAssertion(?PropertyExpression, ?SourceIndividual:Individual, ?TargetIndividual:Individual) % A negative object property assertion NegativePropertyAssertion( OPE a1 a2 ) states that the individual a1 is not connected by the object property expression OPE to the individual a2 % (extensional predicate - can be asserted) :- dynamic(negativePropertyAssertion/3). :- multifile(negativePropertyAssertion/3). axiompred(negativePropertyAssertion/3). axiom_arguments(negativePropertyAssertion,[propertyExpression, individual, individual]). valid_axiom(negativePropertyAssertion(A, B, C)) :- subsumed_by([A, B, C],[propertyExpression, individual, individual]). %% negativeObjectPropertyAssertion(?ObjectPropertyExpression, ?SourceIndividual:Individual, ?TargetIndividual:Individual) % A negative object property assertion NegativePropertyAssertion( OPE a1 a2 ) states that the individual a1 is not connected by the object property expression OPE to the individual a2 negativeObjectPropertyAssertion(A, B, C) :- negativePropertyAssertion(A, B, C),subsumed_by([A, B, C],[objectPropertyExpression, individual, individual]). axiom_arguments(negativeObjectPropertyAssertion,[objectPropertyExpression, individual, individual]). valid_axiom(negativeObjectPropertyAssertion(A, B, C)) :- subsumed_by([A, B, C],[objectPropertyExpression, individual, individual]). %% negativeDataPropertyAssertion(?DataPropertyExpression, ?SourceIndividual:Individual, ?TargetValue:Literal) % A negative data property assertion NegativePropertyAssertion( DPE a lt ) states that the individual a is not connected by the data property expression DPE to the literal lt negativeDataPropertyAssertion(A, B, C) :- negativePropertyAssertion(A, B, C),subsumed_by([A, B, C],[dataPropertyExpression, individual, literal]). axiom_arguments(negativeDataPropertyAssertion,[dataPropertyExpression, individual, literal]). valid_axiom(negativeDataPropertyAssertion(A, B, C)) :- subsumed_by([A, B, C],[dataPropertyExpression, individual, literal]). %% annotationAssertion(?AnnotationProperty, ?AnnotationSubject, ?AnnotationValue) % An annotation assertion AnnotationAssertion( AP as av ) states that the annotation subject as - an IRI or an anonymous individual - is annotated with the annotation property AP and the annotation value av :- dynamic(annotationAssertion/3). :- multifile(annotationAssertion/3). axiompred(annotationAssertion/3). axiom_arguments(annotationAssertion,[annotationProperty, annotationSubject, annotationValue]). valid_axiom(annotationAssertion(A, B, C)) :- subsumed_by([A, B, C],[annotationProperty, annotationSubject, annotationValue]). annotationSubject(_). annotationValue(_). %% annotation(?IRI,?AnnotationProperty,?AnnotationValue) % % @see annotationAnnotation/3, ontologyAnnotation/3, axiomAnnotation/3 :- dynamic(annotation/3). :- multifile(annotation/3). axiompred(annotation/3). annotation(annotationAnnotation(A, B, C)) :- annotationAnnotation(A, B, C). annotation(axiomAnnotation(A, B, C)) :- axiomAnnotation(A, B, C). axiom_arguments(annotation,[iri,annotationProperty,annotationValue]). valid_axiom(annotation(A,B,C)) :- subsumed_by([A,B,C],[iri,annotationProperty,annotationValue]). %% ontologyAnnotation(?Ontology, ?AnnotationProperty, ?AnnotationValue) ontologyAnnotation(Ontology,AP,AV) :- annotation(Ontology,AP,AV), ontology(Ontology). axiom_arguments(ontologyAnnotation,[ontology, annotationProperty, annotationValue]). valid_axiom(ontologyAnnotation(A, B, C)) :- subsumed_by([A, B, C],[ontology, annotationProperty, annotationValue]). %% axiomAnnotation(?Axiom, ?AnnotationProperty, ?AnnotationValue) axiomAnnotation(Axiom,AP,AV) :- annotation(Axiom,AP,AV), axiom(Axiom). axiom_arguments(axiomAnnotation,[axiom, annotationProperty, annotationValue]). valid_axiom(axiomAnnotation(A, B, C)) :- subsumed_by([A, B, C],[axiom, annotationProperty, annotationValue]). %% annotationAnnotation(?Annotation, ?AnnotationProperty, ?AnnotationValue) annotationAnnotation(Annotation,AP,AV) :- annotation(Annotation,AP,AV), annotation(Annotation). axiom_arguments(annotationAnnotation,[annotation, annotationProperty, annotationValue]). valid_axiom(annotationAnnotation(A, B, C)) :- subsumed_by([A, B, C],[annotation, annotationProperty, annotationValue]). %% ontology(?IRI) % An ontology in OWL2 is a collection of OWL Axioms :- dynamic(ontology/1). :- multifile(ontology/1). axiompred(ontology/1). axiom_arguments(ontology,[iri]). valid_axiom(ontology(A)) :- subsumed_by([A],[iri]). %% ontologyDirective(?OntologyIRI,?IRI) % @see ontologyImport/2, ontologyAxiom/2 ontologyDirective(A, B) :- ontologyImport(A, B). ontologyDirective(A, B) :- ontologyAxiom(A, B). ontologyDirective(A, B) :- ontologyVersionInfo(A, B). axiom_arguments(ontologyDirective,[ontology, iri]). valid_axiom(ontologyDirective(A, B)) :- subsumed_by([A, B],[ontology, iri]). %% ontologyAxiom(?Ontology, ?Axiom) % True if Ontology contains Axiom. % Axiom is a prolog term that is typically asserted and separately and can thus can be executed as a goal. % For example, an ontology http://example.org# will contain redundant assertions: % == % subClassOf('http://example.org#a', 'http://example.org#b'). % ontologyAxiom('http://example.org#', subClassOf('http://example.org#a','http://example.org#b')). % == :- dynamic(ontologyAxiom/2). :- multifile(ontologyAxiom/2). axiompred(ontologyAxiom/2). axiom_arguments(ontologyAxiom,[ontology, axiom]). valid_axiom(ontologyAxiom(A, B)) :- subsumed_by([A, B],[ontology, axiom]). %% ontologyImport(?Ontology, ?IRI) % True of Ontology imports document IRI :- dynamic(ontologyImport/2). :- multifile(ontologyImport/2). axiompred(ontologyImport/2). axiom_arguments(ontologyImport,[ontology, iri]). valid_axiom(ontologyImport(A, B)) :- subsumed_by([A, B],[ontology, iri]). %% ontologyVersionInfo(?Ontology, ?IRI) :- dynamic(ontologyVersionInfo/2). :- multifile(ontologyVersionInfo/2). axiompred(ontologyVersionInfo/2). axiom_arguments(ontologyVersionInfo,[ontology, iri]). valid_axiom(ontologyVersionInfo(A, B)) :- subsumed_by([A, B],[ontology, iri]). /**************************************** RESTRICTIONS ON AXIOMS ****************************************/ % 11.1 % An object property expression OPE is simple in Ax if, for each object property expression OPE' such that OPE' ->* OPE holds, OPE' is not composite. % (The property hierarchy relation ->* is the reflexive-transitive closure of ->) %simpleObjectPropertyExpresion(OPE) :- % objectPropertyExpression(OPE), /**************************************** EXPRESSIONS ****************************************/ subsumed_by(X,_) :- var(X),!. subsumed_by([],[]) :- !. subsumed_by([I|IL],[T|TL]) :- !, subsumed_by(I,T), subsumed_by(IL,TL). subsumed_by(L,set(T)):- !, forall(member(I,L), subsumed_by(I,T)). subsumed_by(I,T):- !, G=..[T,I], G. %% iri(?IRI) % true if IRI is an IRI. TODO: currently underconstrained, any atomic term can be an IRI iri(IRI) :- atomic(IRI). % %% literal(?Lit) % true if Lit is an rdf literal %literal(_). % TODO literal(literal(_)). % TODO propertyExpression(E) :- objectPropertyExpression(E) ; dataPropertyExpression(E). %% objectPropertyExpression(?OPE) % true if OPE is an ObjectPropertyExpression % ObjectPropertyExpression := ObjectProperty | InverseObjectProperty objectPropertyExpression(E) :- objectProperty(E) ; inverseObjectProperty(E). % give benefit of doubt; e.g. rdfs:label % in the OWL2 spec we have DataProperty := IRI % here dataProperty/1 is an asserted fact objectPropertyExpression(E) :- nonvar(E),iri(E). objectPropertyExpressionOrChain(propertyChain(PL)) :- forall(member(P,PL),objectPropertyExpression(P)). objectPropertyExpressionOrChain(PE) :- objectPropertyExpression(PE). inverseObjectProperty(inverseOf(OP)) :- objectProperty(OP). dataPropertyExpression(E) :- dataProperty(E). dataPropertyExpression(DPEs) :- ( is_list(DPEs) -> forall(member(DPE,DPEs), dataPropertyExpression(DPE)) ; dataPropertyExpression(DPEs)). % give benefit of doubt; e.g. rdfs:label % in the OWL2 spec we have DataProperty := IRI % here dataProperty/1 is an asserted fact dataPropertyExpression(E) :- nonvar(E),iri(E). %already declared as entity %datatype(IRI) :- iri(IRI). %% dataRange(+DR) is semidet dataRange(DR) :- datatype(DR) ; dataIntersectionOf(DR ); dataUnionOf(DR) ; dataComplementOf(DR) ; dataOneOf(DR) ; datatypeRestriction(DR). %% classExpression(+CE) is semidet % % true if CE is a class expression term, as defined in OWL2 % % Example: =|classExpression(intersectionOf([car,someValuesFrom(hasColor,blue)])))|= % % Union of: % % class/1 | objectIntersectionOf/1 | objectUnionOf/1 | % objectComplementOf/1 | objectOneOf/1 | objectSomeValuesFrom/1 | % objectAllValuesFrom/1 | objectHasValue/1 | objectHasSelf/1 | % objectMinCardinality/1 | objectMaxCardinality/1 | % objectExactCardinality/1 | dataSomeValuesFrom/1 | % dataAllValuesFrom/1 | dataHasValue/1 | dataMinCardinality/1 | % dataMaxCardinality/1 | dataExactCardinality/1 classExpression(CE):- iri(CE) ; % NOTE: added to allow cases where class is not imported class(CE) ; objectIntersectionOf(CE) ; objectUnionOf(CE) ; objectComplementOf(CE) ; objectOneOf(CE) ; objectSomeValuesFrom(CE) ; objectAllValuesFrom(CE) ; objectHasValue(CE) ; objectHasSelf(CE) ; objectMinCardinality(CE) ; objectMaxCardinality(CE) ; objectExactCardinality(CE) ; dataSomeValuesFrom(CE) ; dataAllValuesFrom(CE) ; dataHasValue(CE) ; dataMinCardinality(CE) ; dataMaxCardinality(CE) ; dataExactCardinality(CE). %% objectIntersectionOf(+CE) is semidet % true if CE is a term intersectionOf(ClassExpression:list) % % An intersection class expression IntersectionOf( CE1 ... CEn ) contains all individuals that are instances of all class expressions CEi for 1 <= i <= n. objectIntersectionOf(intersectionOf(CEs)) :- forall(member(CE,CEs), classExpression(CE)). %% objectUnionOf(+CE) is semidet % A union class expression UnionOf( CE1 ... CEn ) contains all individuals that are instances of at least one class expression CEi for 1 <= i <= n objectUnionOf(unionOf(CEs)) :- forall(member(CE,CEs), classExpression(CE)). %% objectComplementOf(+CE) is semidet % objectComplementOf(complementOf(CE)) :- classExpression(CE). %% objectOneOf(+CE) is semidet % An enumeration of individuals OneOf( a1 ... an ) contains exactly the individuals ai with 1 <= i <= n. objectOneOf(oneOf(Is)) :- is_list(Is). % TODO: check if we need to strengthen this check %objectOneOf(oneOf(Is)) :- % forall(member(I,Is), % individual(I)). %% objectSomeValuesFrom(+R) is semidet % An existential class expression SomeValuesFrom( OPE CE ) consists of an object property expression OPE and a class expression CE, and it contains all those individuals that are connected by OPE to an individual that is an instance of CE objectSomeValuesFrom(someValuesFrom(OPE,CE)) :- objectPropertyExpression(OPE), classExpression(CE). %% objectAllValuesFrom(+R) is semidet % A universal class expression AllValuesFrom( OPE CE ) consists of an object property expression OPE and a class expression CE, and it contains all those individuals that are connected by OPE only to individuals that are instances of CE objectAllValuesFrom(allValuesFrom(OPE,CE)) :- objectPropertyExpression(OPE), classExpression(CE). %% objectHasValue(+R) is semidet % A has-value class expression HasValue( OPE a ) consists of an object property expression OPE and an individual a, and it contains all those individuals that are connected by OPE to a objectHasValue(hasValue(OPE,I)) :- objectPropertyExpression(OPE), individual(I). %% objectHasSelf(+R) is semidet % A self-restriction HasSelf( OPE ) consists of an object property expression OPE, and it contains all those individuals that are connected by OPE to themselves objectHasSelf(hasSelf(OPE)) :- objectPropertyExpression(OPE). %% objectMinCardinality(+CR) is semidet % A minimum cardinality expression MinCardinality( n OPE CE ) consists of a nonnegative integer n, an object property expression OPE, and a class expression CE, and it contains all those individuals that are connected by OPE to at least n different individuals that are instances of CE. If CE is missing, it is taken to be owl:Thing objectMinCardinality(minCardinality(C,OPE,CE)):- number(C), C>=0, objectPropertyExpression(OPE), classExpression(CE). objectMinCardinality(minCardinality(C,OPE)):- number(C), C>=0, objectPropertyExpression(OPE). %% objectMaxCardinality(+CR) is semidet % A maximum cardinality expression MaxCardinality( n OPE CE ) consists of a nonnegative integer n, an object property expression OPE, and a class expression CE, and it contains all those individuals that are connected by OPE to at most n different individuals that are instances of CE. If CE is missing, it is taken to be owl:Thing objectMaxCardinality(maxCardinality(C,OPE,CE)):- number(C), C>=0, objectPropertyExpression(OPE), classExpression(CE). objectMaxCardinality(maxCardinality(C,OPE)):- number(C), C>=0, objectPropertyExpression(OPE). %% objectExactCardinality(+CR) is semidet % An exact cardinality expression ExactCardinality( n OPE CE ) consists of a nonnegative integer n, an object property expression OPE, and a class expression CE, and it contains all those individuals that are connected by OPE to exactly n different individuals that are instances of CE. If CE is missing, it is taken to be owl:Thing objectExactCardinality(exactCardinality(C,OPE,CE)):- number(C), C>=0, objectPropertyExpression(OPE), classExpression(CE). objectExactCardinality(exactCardinality(C,OPE)):- number(C), C>=0, objectPropertyExpression(OPE). % NON-NORMATIVE: we accept this in order to maximize compatibility with Thea1 objectExactCardinality(cardinality(C,OPE)):- number(C), C>=0, objectPropertyExpression(OPE). %% dataIntersectionOf(+DR:dataIntersectionOf) is semidet % An intersection data range IntersectionOf( DR1 ... DRn ) contains all data values that are contained in the value space of every data range DRi for 1 <= i <= n. All data ranges DRi must be of the same arity dataIntersectionOf(intersectionOf(DRs)) :- forall(member(DR,DRs), dataRange(DR)). %% dataUnionOf(+DR:dataUnionOf) is semidet % A union data range UnionOf( DR1 ... DRn ) contains all data values that are contained in the value space of at least one data range DRi for 1 <= i <= n. All data ranges DRi must be of the same arity dataUnionOf(unionOf(DRs)) :- forall(member(DR,DRs), dataRange(DR)). %% dataComplementOf(+DR:dataComplementOf) is semidet % A complement data range ComplementOf( DR ) contains all literals that are not contained in the data range DR dataComplementOf(complementOf(DR)) :- dataRange(DR). %% dataOneOf(+DR:dataOneOf) is semidet % An enumeration of literals OneOf( lt1 ... ltn ) contains exactly the explicitly specified literals lti with 1 <= i <= n dataOneOf(oneOf(DRs)) :- forall(member(DR,DRs), dataRange(DR)). %% datatypeRestriction(+DR) is semidet % % TODO: multiple args datatypeRestriction(datatypeRestriction(DR,FacetValues)):- datatype(DR), FacetValues=[_|_]. %% dataSomeValuesFrom(+DR) is semidet dataSomeValuesFrom(someValuesFrom(DPE,DR)):- dataPropertyExpression(DPE), dataRange(DR). %% dataAllValuesFrom(+DR) is semidet dataAllValuesFrom(allValuesFrom(DPE,DR)):- dataPropertyExpression(DPE), dataRange(DR). %% dataHasValue(+DR) is semidet % A has-value class expression HasValue( DPE lt ) consists of a data property expression DPE and a literal lt, and it contains all those individuals that are connected by DPE to lt. Each such class expression can be seen as a syntactic shortcut for the class expression SomeValuesFrom( DPE OneOf( lt ) ) dataHasValue(hasValue(DPE,L)):- dataPropertyExpression(DPE), literal(L). %% dataMinCardinality(+DR) is semidet % A minimum cardinality expression MinCardinality( n DPE DR ) consists of a nonnegative integer n, a data property expression DPE, and a unary data range DR, and it contains all those individuals that are connected by DPE to at least n different literals in DR. If DR is not present, it is taken to be rdfs:Literal dataMinCardinality(minCardinality(C,DPE,DR)):- number(C), C>=0, dataPropertyExpression(DPE), dataRange(DR). dataMinCardinality(minCardinality(C,DPE)):- number(C), C>=0, dataPropertyExpression(DPE). %% dataMaxCardinality(+DR) is semidet % A maximum cardinality expression MaxCardinality( n DPE DR ) consists of a nonnegative integer n, a data property expression DPE, and a unary data range DR, and it contains all those individuals that are connected by DPE to at most n different literals in DR. If DR is not present, it is taken to be rdfs:Literal. dataMaxCardinality(maxCardinality(C,DPE,DR)):- number(C), C>=0, dataPropertyExpression(DPE), dataRange(DR). dataMaxCardinality(maxCardinality(C,DPE)):- number(C), C>=0, dataPropertyExpression(DPE). %% dataExactCardinality(+DR) is semidet % An exact cardinality expression ExactCardinality( n DPE DR ) consists of a nonnegative integer n, a data property expression DPE, and a unary data range DR, and it contains all those individuals that are connected by DPE to exactly n different literals in DR. If DR is not present, it is taken to be rdfs:Literal dataExactCardinality(exactCardinality(C,DPE,DR)):- number(C), C>=0, dataPropertyExpression(DPE), dataRange(DR). dataExactCardinality(exactCardinality(C,DPE)):- number(C), C>=0, dataPropertyExpression(DPE). % NON-NORMATIVE: we accept this in order to maximize compatibility with Thea1 dataExactCardinality(cardinality(C,OPE)):- number(C), C>=0, objectPropertyExpression(OPE). %% valid_axiom(?Axiom) is nondet % true if Axiom passes typechecking %% is_valid_axiom(?Axiom) is semidet % true if Axiom passes typechecking is_valid_axiom(Axiom) :- \+ \+ valid_axiom(Axiom). /**************************************** VIEW PREDICATES ****************************************/ %% equivalent_to(?X,?Y) % note: this is currently slow for bound values of X and Y equivalent_to(X,Y) :- equivalentClasses(L),member(X,L),member(Y,L),X\=Y. equivalent_to(X,Y) :- equivalentProperties(L),member(X,L),member(Y,L),X\=Y. disjoint_with(X,Y) :- disjointClasses(L),member(X,L),member(Y,L),X\=Y. %% anyPropertyAssertion(?Property,?Entity,?Value) % subsumes propertyAssertion/3 and annotationAssertion/3 anyPropertyAssertion(P,E,V) :- propertyAssertion(P,E,V). anyPropertyAssertion(P,E,V) :- annotationAssertion(P,E,V). %% labelAnnotation_value(?X,?Val) labelAnnotation_value(X,Val) :- anyPropertyAssertion('http://www.w3.org/2000/01/rdf-schema#label', X, literal(type(_,Val))),atom(Val). labelAnnotation_value(X,Val) :- anyPropertyAssertion('http://www.w3.org/2000/01/rdf-schema#label', X, literal(lang(_,Val))),atom(Val). labelAnnotation_value(X,Val) :- anyPropertyAssertion('http://www.w3.org/2000/01/rdf-schema#label', X, literal(Val)),atom(Val). /**************************************** META-PREDICATES ****************************************/ %% axiom_directly_about(?Ax,?About) % true if Ax is an axiom whose first argument is equal to About. % % e.g. axiom_directly_about( subClassOf(X,_), X). % % also include property assertions whose second argument is equal to About. % % e.g. axiom_directly_about( propertyAssertion(P,X,_), X). % axiom_directly_about(Ax,About) :- axiom(Ax), Ax =.. [_,Arg1|_], ( is_list(Arg1) -> member(About,Arg1) ; About=Arg1). axiom_directly_about(Ax,About) :- Ax=propertyAssertion(_,About,_), axiom(Ax). axiom_directly_about(Ax,About) :- Ax=annotationAssertion(_,About,_), axiom(Ax). axiom_directly_about(Ax,About) :- Ax=classAssertion(_,About), axiom(Ax). %% axiom_directly_references(?Ax:axiom,?Ref) % % Ref may be % - an axiom % - a named entity % - an expression axiom_directly_references(Ax,Ref) :- axiom(Ax), axiom_or_expression_references(Ax,Ref). axiom_or_expression_references(X,Ref) :- X =.. [P|Args], P\=literal, member(Arg,Args), ( is_list(Arg) -> member(Ref,Arg) ; Ref=Arg). axiom_about(Ax,About) :- axiom_directly_about(Ax,About). axiom_about(Ax,About) :- axiom_directly_about(Ax,X), axiom_about(X,About). axiom_references(Ax,Ref) :- axiom_directly_references(Ax,Ref). axiom_references(Ax,Ref) :- axiom_directly_references(Ax,X), axiom_or_expression_references(X,Ref). axiom_contains_expression(Ax,Ex) :- axiom_contains_expression(Ax,Ex,_). axiom_contains_expression(Ax,Ex,D) :- axiom(Ax), expression_has_subexpression(Ax,Ex,[],Chain), length(Chain,D). expression_has_subexpression(Ex,Ex,Accum,Accum). expression_has_subexpression(Ex,SubEx,Accum,Results) :- Ex =.. [F|Args], member(A,Args), expression_has_subexpression(A,SubEx,[F|Accum],Results). %% referenced_description(?Desc) is nondet % true if Desc is either a class or a class expression using the set of ontologies loaded. % Example: if the ontology contains % == % subClassOf(a,intersectionOf([b,someValuesFrom(p,c)])) % == % then Desc will be a member of [a, b, c, b and p some c, p some c] referenced_description(C) :- setof(C,referenced_description_1(C),Cs), member(C,Cs). referenced_description_1(C) :- class(C). referenced_description_1(C) :- subClassOf(A,B), ( referenced_description(A,C) ; referenced_description(B,C)). referenced_description_1(C) :- equivalentClasses(L), member(A,L), referenced_description(A,C). referenced_description_1(C) :- classAssertion(A,_), referenced_description(A,C). % TODO - this is incomplete referenced_description(X,X) :- ground(X). referenced_description(someValuesFrom(_,X),Y) :- referenced_description(X,Y). referenced_description(allValuesFrom(_,X),Y) :- referenced_description(X,Y). referenced_description(intersectionOf(L),Y) :- member(X,L),referenced_description(X,Y). referenced_description(unionOf(L),Y) :- member(X,L),referenced_description(X,Y). /**************************************** UTILITY ****************************************/ :- multifile assert_axiom_hook/1. :- dynamic assert_axiom_hook/1. %% assert_axiom(+Axiom:axiom) % % writes an axiom to the prolog database. % typically this will just be a matter of calling assert/1. However, in future we % will have different backing stores (rdf_db, sql), and in these cases calls to % this predicate will perform the appropriate actions. % % this also asserts ontologyAxiom/2, using nb_getval with current_ontology assert_axiom(Axiom) :- assert_axiom_hook(Axiom), !. assert_axiom(Axiom) :- assert(Axiom), ( nb_current(current_ontology,O) -> assert(ontologyAxiom(O,Axiom)) ; true), !. %% assert_axiom(+Axiom:axiom,+Ontology:ontology) is det % % as assert_axiom/1, but also asserts to ontologyAxiom/2 assert_axiom(Axiom,O) :- assert(Axiom), assert(ontologyAxiom(O,Axiom)), !. :- multifile retract_axiom_hook/1. :- dynamic retract_axiom_hook/1. %% retract_axiom(+Axiom:axiom) % % removes an axiom from the prolog database. % typically this will just be a matter of calling retract/1. However, in future we % will have different backing stores (rdf_db, sql), and in these cases calls to % this predicate will perform the appropriate actions. % % also removes ontologyAxiom/2 from ALL ontologies retract_axiom(Axiom) :- retract_axiom_hook(Axiom), !. retract_axiom(Axiom) :- retractall(Axiom), retractall(ontologyAxiom(_,Axiom)), !. %% retract_axiom(+Axiom:axiom,+Ontology) % retracts axioms from a specified ontology retract_axiom(Axiom,Ontology) :- \+ var(Ontology), retractall(ontologyAxiom(Ontology,Axiom)), ( \+ ontologyAxiom(_,Axiom) -> retractall(Axiom) ; true), % still exists in other ontology.. !. retract_all_axioms :- findall(A,axiom(A),Axioms), maplist(retract,Axioms), findall(ontologyAxiom(O,A),ontologyAxiom(O,A),OAxioms), maplist(retract,OAxioms), !. owl2_model_init :- assert(annotationProperty('http://www.w3.org/2000/01/rdf-schema#label')), assert(annotationProperty('http://www.w3.org/2000/01/rdf-schema#comment')). consult_axioms(File) :- consult(File). axiom_type(A,T) :- functor(A,T,_). /** Ontology language axioms and expressions ---+ Synopsis Example OWL2 ontology as a prolog database: == class(organism). class(animal). class(carnivore). class(herbivore). objectProperty(eats). subClassOf(animal,organism). equivalentClasses([carnivore,intersectionOf([animal,someValuesFrom(eats,animal)])]). disjointClasses([herbivore,carnivore]). == Example of use: == :- use_module(library(thea2/owl2_io)). :- use_module(library(thea2/owl2_model)). show_superclasses(OntFile,Class) :- load_axioms(OntFile), forall(subClassOf(Class,Super), writeln(Super)). == ---+ Details This module is a prolog model of the OWL2 language. It consists of predicates for both OWL2 axioms and expressions. This model is intended to closely parallel Structural Specification and Functional-Style Syntax for OWL2 (http://www.w3.org/TR/owl2-syntax). * Axioms and Declarations are modeled as prolog predicates (e.g. SubClassOf --> subClassOf/2) * Class and Property Expressions are modeled as prolog terms. These can be checked via semi-deterministic predicates (e.g. objectIntersectionOf/1) * Axiom Annotations are modeled as prolog predicates taking a reified axiom clause head as an argument (axiomAnnotation/3) * The names should correspond exactly, with the leading uppercase character substituted for a lowercase (to avoid quoting in prolog) - the one exception is Import, which maps to the prolog predicate ontologyImport/2 (to avoid confusion with prolog import/1) * Axioms with variable arguments are modeled as prolog predicates that take prolog lists as arguments (e.g. equivalentClasses/1) * For programmatic convenience we provide additional abstract predicates that do not necessarily correspond to the OWL syntax (e.g. property/1,fact/1) ---++ Axioms Extensional predicates are declared for all terminal axiom symbols in the functional syntax; i.e. subPropertyOf/2, subClassOf/2. These can be directly asserted, or compiled from a prolog file. The terms from the OWL2 structural syntax are taken as primitive, i.e. they are extensional / unit-clauses, and designed to be asserted or compiled. Some predicates such as property/1 are intensional - these generalize over the OWL2 axioms are defined by prolog rules, and should not be asserted. In this case property/1 is defined as annotationProperty/1 or dataProperty/1 or objectProperty/1. For the strong typed model, we also provide intensional predicates such as subObjectPropertyOf/2 - satisfaction of this predicate is determined at runtime based on type-checking, if subPropertyOf/2 holds. ---++ Expressions and Type checking OWL Axioms can take either entities or expressions as arguments. Entities are simply prolog atoms corresponding to the IRI. Expressions are prolog terms; e.g. =|intersectionOf(a,someValuesFrom(inverseOf(p),b))|= (Class expressions are also known as Descriptions) Optional run-time checking of predicates using valid_axiom/1. For example =|subClassOf(intersectionOf(c1,c2),unionOf(c3,c4))|= is valid if c1,c2,c3,c4 are all class expressions, but =|subClassOf(p1,c1)|= is not valid if p1 is a property We can also make checks for specific types: e.g objectIntersectionOf/1 ---++ Annotations In OWL Syntax, axiom annotations are written using an optional annotation list argument. We opt not to do this here; instead we use axiomAnnotation/3 where the first argument is the reified predicate head. E.g. == subClassOf(cat,mammal). axiomAnnotation(SubClassOf(cat,mammal),author,linnaeus). == ---++ Ontologies We use a similar scheme for annotations: == subClassOf(cat,mammal). ontologyAxiom(linnaenTaxonomy,SubClassOf(cat,mammal)). ontology(linnaenTaxonomy). == TODO: check edge cases, eg two ontologies have the same axioms but different annotations ---++ IRIs By default there is no type checking of IRIs, so =|class(polarBear)|= is allowed, even though "polarBear" is not an IRI - this makes for convenience in working with example ontologies. See prefix_IRIs/1 in owl2_util.pl for converting between short names and valid IRIs. ---+ Open Issues ---++ Enumeration of expressions We provide semi-deterministic predicates of the form ?type(+Expression). Should the mode be extended to allow enumeration of all descriptions/expressions? This would probably require forcing all expressions to be bnodes OR possibly recursively analyzing the term Axiom in a call axiom(Axiom) ---++ Type checking Is Tom Schrijvers type checking system going to be integrated into SWI and Yap? Should we use that? I am attempting to put as much typing info in the pldoc comments, but unsure of the conventions for complex terms. LATEST: see owl2_metamodel.pl ---++ Ontologies continue using ontologyAxiom/2? Alternatively use builtin prolog module mechanism..? ---+ See Also * owl2_from_rdf.pl * swrl.pl ---+ Additional Information @see README @license License */