owl2_model.pl

/* -*- 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,

	   literal/1,			% JW: Added as needed in swrl
	   builtin_class/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):-
	call(T,I).


%% 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)).

% 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 :-
	forall(axiom(A), retract(A)),
        forall(ontologyAxiom(O,A),		% JW: why not retractall/1?
	       retract(ontologyAxiom(O,A))).

owl2_model_init :-
	u_assert(annotationProperty('http://www.w3.org/2000/01/rdf-schema#label')),
	u_assert(annotationProperty('http://www.w3.org/2000/01/rdf-schema#comment')),
	u_assert(datatype('http://www.w3.org/2001/XMLSchema#integer')),
	u_assert(datatype('http://www.w3.org/2001/XMLSchema#decimal')),
	u_assert(datatype('http://www.w3.org/2001/XMLSchema#float')),
	u_assert(datatype('http://www.w3.org/2001/XMLSchema#string')).

u_assert(Clause) :-
	(   call(Clause)
	->  true
	;   assert(Clause)
	).

consult_axioms(File) :-
        consult(File).

axiom_type(A,T) :- functor(A,T,_).

/** <module> 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

*/