Skip to content
Browse files

Commit changes

  • Loading branch information...
1 parent 026a2df commit 898d4aa5b96fe4c036f63e30af72197d6475e216 Vangelis Vassiliadis committed
Showing with 292 additions and 135 deletions.
  1. +12 −20 owl2_basic_reasoner.pl
  2. +17 −10 owl2_io.pl
  3. +110 −45 owl2_model.pl
  4. +19 −5 owl2_reasoner.pl
  5. +83 −52 owl2_reasoning_rules.pl
  6. +9 −0 owl2_util.pl
  7. +22 −3 rules/basicset.pl
  8. +12 −0 testfiles/cell.owlpl
  9. +8 −0 thea.pl
View
32 owl2_basic_reasoner.pl
@@ -2,9 +2,9 @@
:- module(owl2_basic_reasoner,
[
- entailed/1,
- property_assertion_common_ancestor/5,
- property_assertion_least_common_ancestor/5
+ entailed/1
+ %property_assertion_common_ancestor/5,
+ %property_assertion_least_common_ancestor/5
]).
:- use_module(owl2_model).
@@ -21,8 +21,9 @@
%% entailed(?Axiom) is nondet
% true if Axiom is entailed
entailed(A) :-
- entailed(A,[]).
-
+ debug(reasoner,'<<testing for ~w',[A]),
+ entailed(A,[]),
+ debug(reasoner,'>>found ~w',[A]).
entailed(A,EL) :- entailed_2(A,EL).
@@ -81,21 +82,12 @@
entailed(subClassOf(X,A)),
entailed(subClassOf(X,B)).
-% TODO: move this to a utility module
-property_assertion_common_ancestor(P,XI,YI,XC,YC) :-
- propertyAssertion(P,XI,YI),
- % TESTING ONLY:
- sub_atom(XI,0,_,_,'http://ccdb.ucsd.edu/SAO/DPO/2.0/DPO.owl'),
- debug(owl2_basic_reasoner,'Testing ~w ~w ~w',[P,XI,YI]),
- entailed(classAssertion(XC,XI)),
- entailed(classAssertion(YC,YI)).
-
-property_assertion_least_common_ancestor(P,XI,YI,XC,YC) :-
- property_assertion_common_ancestor(P,XI,YI,XC,YC),
- \+ ((property_assertion_common_ancestor(P,XI,YI,XC2,YC2),
- entailed(subClassOfReflexive(XC2,XC)),
- entailed(subClassOfReflexive(YC2,YC)),
- ( XC2\=XC ; YC2\=YC))).
+%property_assertion_least_common_ancestor(P,XI,YI,XC,YC) :-
+% property_assertion_common_ancestor(P,XI,YI,XC,YC),
+% \+ ((property_assertion_common_ancestor(P,XI,YI,XC2,YC2),
+% entailed(subClassOfReflexive(XC2,XC)),
+% entailed(subClassOfReflexive(YC2,YC)),
+% ( XC2\=XC ; YC2\=YC))).
% ----------------------------------------
View
27 owl2_io.pl
@@ -41,8 +41,22 @@
; Fmt=owlpl
; Fmt=pl),
!,
+ load_prolog_axioms(File).
+load_axioms(File,Fmt,Opts) :-
+ load_handler(read,Fmt),
+ load_axioms_hook(File,Fmt,Opts),
+ !.
+load_axioms(File,Fmt,Opts) :-
+ throw(owl2_io('cannot parse fmt for',File,Fmt,Opts)).
+
+load_prolog_axioms(File) :-
+ \+ predicate_property(qcompile(_),_), % e.g. Yap
+ !,
style_check(-discontiguous),
- style_check(-atom),
+ consult_axioms(File).
+load_prolog_axioms(File) :-
+ style_check(-discontiguous),
+ style_check(-atom),
file_name_extension(Base, _Ext, File),
file_name_extension(Base, qlf, QlfFile),
debug(load,'checking for: ~w',[QlfFile]),
@@ -57,12 +71,6 @@
; debug(load,' cannot write to qlf (permission problem?), loading from: ~w',[File]),
consult_axioms(File)
).
-load_axioms(File,Fmt,Opts) :-
- load_handler(read,Fmt),
- load_axioms_hook(File,Fmt,Opts),
- !.
-load_axioms(File,Fmt,Opts) :-
- throw(owl2_io('cannot parse fmt for',File,Fmt,Opts)).
%% save_axioms(+File,+Fmt)
% saves owl2_model axioms to File.
@@ -100,11 +108,10 @@
load_axioms(FileIn,FmtIn,Opts),
save_axioms(FileOut,FmtOut,Opts).
+% TODO - check if this is the best way of doing this
load_handler(Dir,Fmt) :-
forall(format_module(Dir,Fmt,Mod),
- ( atom_concat('thea2/',Mod,TMod), % TODO: check for more elegant way to do this..
- % TMod = Mod, % assumes library_directory(<path_to_thea>) is asserted.
- ensure_loaded(library(TMod)))).
+ ensure_loaded(library(thea2/Mod))).
guess_format(File,Fmt,_Opts) :-
concat_atom(Toks,'.',File),
View
155 owl2_model.pl
@@ -122,15 +122,6 @@
% (metamodeling) true if PredSpec is a predicate that defines an axiom
:- multifile axiompred/1.
-% The ext/1 directive is used to declare a predicate extensional. Extensional predicates are dynamic, because we may
-% wish to modify the database at run time. They are multifile, as we may wish to load from multiple sources.
-% In tabled prologs such as Yap, extensional predicates are tabled, because they may be entailed as well as asserted.
-term_expansion((:- ext(Pred)),
- [( :- multifile(Pred)),(:- dynamic(Pred)), axiompred(Pred)]).
-
-%term_expansion((:- ext(Pred)),
-% [(:- table(Pred)),(:- multifile Pred),axiompred(Pred)]) :- current_prolog_flag(dialect,yap).
-
:- discontiguous(valid_axiom/1).
:- discontiguous(axiompred/1).
:- discontiguous(axiom_arguments/2).
@@ -166,13 +157,17 @@
%% class(?IRI)
% Classes can be understood as sets of individuals
-:- ext(class/1).
+:- 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
-:- ext(datatype/1).
+:- dynamic(datatype/1).
+:- multifile(datatype/1).
+axiompred(datatype/1).
axiom_arguments(datatype,[iri]).
valid_axiom(datatype(A)) :- subsumed_by([A],[iri]).
@@ -188,19 +183,25 @@
%% objectProperty(?IRI)
% Object properties connect pairs of individuals
-:- ext(objectProperty/1).
+:- 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.
-:- ext(dataProperty/1).
+:- 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
-:- ext(annotationProperty/1).
+:- dynamic(annotationProperty/1).
+:- multifile(annotationProperty/1).
+axiompred(annotationProperty/1).
axiom_arguments(annotationProperty,[iri]).
valid_axiom(annotationProperty(A)) :- subsumed_by([A],[iri]).
@@ -216,14 +217,18 @@
%% 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
-:- ext(namedIndividual/1).
+:- 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
-:- ext(anonymousIndividual/1).
+:- dynamic(anonymousIndividual/1).
+:- multifile(anonymousIndividual/1).
+axiompred(anonymousIndividual/1).
axiom_arguments(anonymousIndividual,[iri]).
valid_axiom(anonymousIndividual(A)) :- subsumed_by([A],[iri]).
@@ -261,25 +266,34 @@
%
% @param SubClass a classExpression/1 representing the more specific class
% @param SuperClass a classExpression/1 representing the more general class
-:- ext(subClassOf/2).
+:- 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.
-:- ext(equivalentClasses/1).
+:- 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
-:- ext(disjointClasses/1).
+:- 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.
-:- ext(disjointUnion/2).
+:- 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)]).
@@ -306,7 +320,9 @@
%% subPropertyOf(?Sub:PropertyExpression, ?Super:ObjectPropertyExpressions)
% subproperty axioms are analogous to subclass axioms
% (extensional predicate - can be asserted)
-:- ext(subPropertyOf/2).
+:- dynamic(subPropertyOf/2).
+:- multifile(subPropertyOf/2).
+axiompred(subPropertyOf/2).
axiom_arguments(subPropertyOf,[propertyExpression, objectPropertyExpressions]).
valid_axiom(subPropertyOf(A, B)) :- subsumed_by([A, B],[propertyExpression, objectPropertyExpressions]).
@@ -331,7 +347,9 @@
%% 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)
-:- ext(equivalentProperties/1).
+:- dynamic(equivalentProperties/1).
+:- multifile(equivalentProperties/1).
+axiompred(equivalentProperties/1).
axiom_arguments(equivalentProperties,[set(propertyExpression)]).
valid_axiom(equivalentProperties(A)) :- subsumed_by([A],[set(propertyExpression)]).
@@ -350,7 +368,9 @@
%% 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)
-:- ext(disjointProperties/1).
+:- dynamic(disjointProperties/1).
+:- multifile(disjointProperties/1).
+axiompred(disjointProperties/1).
axiom_arguments(disjointProperties,[set(propertyExpression)]).
valid_axiom(disjointProperties(A)) :- subsumed_by([A],[set(propertyExpression)]).
@@ -372,7 +392,9 @@
% Example:
% =|inverseProperties(partOf,hasPart)|=
% (extensional predicate - can be asserted)
-:- ext(inverseProperties/2).
+:- 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]).
@@ -381,7 +403,9 @@
% domain of the property expression PE is CE
% (extensional predicate - can be asserted)
-:- ext(propertyDomain/2).
+:- 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]).
@@ -406,7 +430,9 @@
%% 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)
-:- ext(propertyRange/2).
+:- 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]).
@@ -431,7 +457,9 @@
%% 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)
-:- ext(functionalProperty/1).
+:- dynamic(functionalProperty/1).
+:- multifile(functionalProperty/1).
+axiompred(functionalProperty/1).
axiom_arguments(functionalProperty,[propertyExpression]).
valid_axiom(functionalProperty(A)) :- subsumed_by([A],[propertyExpression]).
@@ -449,43 +477,57 @@
%% 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
-:- ext(inverseFunctionalProperty/1).
+:- 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
-:- ext(reflexiveProperty/1).
+:- 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
-:- ext(irreflexiveProperty/1).
+:- 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
-:- ext(symmetricProperty/1).
+:- 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
-:- ext(asymmetricProperty/1).
+:- 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
-:- ext(transitiveProperty/1).
+:- 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
-:- ext(hasKey/2).
+:- 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]).
@@ -506,26 +548,34 @@
%% 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
-:- ext(sameIndividual/1).
+:- 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
-:- ext(differentIndividuals/1).
+:- 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
-:- ext(classAssertion/2).
+:- 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)
-:- ext(propertyAssertion/3).
+:- 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]).
@@ -544,7 +594,9 @@
%% 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)
-:- ext(negativePropertyAssertion/3).
+:- 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]).
@@ -562,14 +614,18 @@
%% annotationAssertion(?AnnotationProperty, ?AnnotationSubject, ?AnnotationValue)
% An annotation assertion AnnotationAssertion( AP as at ) states that the annotation subject as - an IRI or an anonymous individual - is annotated with the annotation property AP and the annotation value av
-:- ext(annotationAssertion/3).
+:- 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]).
%% annotation(?IRI,?AnnotationProperty,?AnnotationValue)
%
% @see annotationAnnotation/3, ontologyAnnotation/3, axiomAnnotation/3
-:- ext(annotation/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).
@@ -599,7 +655,9 @@
%% ontology(?IRI)
% An ontology in OWL2 is a collection of OWL Axioms
-:- ext(ontology/1).
+:- dynamic(ontology/1).
+:- multifile(ontology/1).
+axiompred(ontology/1).
axiom_arguments(ontology,[iri]).
valid_axiom(ontology(A)) :- subsumed_by([A],[iri]).
@@ -619,18 +677,24 @@
% subClassOf('http://example.org#a', 'http://example.org#b').
% ontologyAxiom('http://example.org#', subClassOf('http://example.org#a','http://example.org#b')).
% ==
-:- ext(ontologyAxiom/2).
+:- 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
-:- ext(ontologyImport/2).
+:- 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)
-:- ext(ontologyVersionInfo/2).
+:- 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]).
@@ -931,6 +995,7 @@
****************************************/
%% 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.
View
24 owl2_reasoner.pl
@@ -3,14 +3,19 @@
:- module(owl2_reasoner,
[
initialize_reasoner/3,
- reasoner_tell/1,
reasoner_tell/2,
+ reasoner_tell_all/1,
reasoner_ask/2,
reasoner_check_consistency/1
]).
:- use_module(owl2_model).
+:- multifile owl2_reasoner:initialize_reasoner_hook/3.
+:- multifile owl2_reasoner:reasoner_tell_hook/2.
+:- multifile owl2_reasoner:reasoner_tell_all_hook/1.
+:- multifile owl2_reasoner:reasoner_ask_hook/2.
+
%% initialize_reasoner(+Type,?Reasoner)
% see initialize_reasoner/2
initialize_reasoner(Type,Reasoner) :-
@@ -30,15 +35,24 @@
reasoner_tell_hook(Reasoner,Axiom).
%% reasoner_tell_all(+Reasoner)
-reasoner_tell_all(Reasoner,Axiom) :-
- reasoner_tell_all_hook(Reasoner,Axiom).
+reasoner_tell_all(Reasoner) :-
+ reasoner_tell_all_hook(Reasoner),
+ !.
+reasoner_tell_all(Reasoner) :-
+ forall(axiom(A),
+ reasoner_tell(Reasoner,A)).
%% reasoner_ask(+Reasoner,?Axiom)
reasoner_ask(Reasoner,Axiom) :-
- reasoner_ask(Reasoner,Axiom).
+ reasoner_ask_hook(Reasoner,Axiom).
%% reasoner_consistent(+Reasoner)
+
+% --
+
+
+
/** <module> reasoner API - NOT YET IN USE
---+ Synopsis
@@ -55,7 +69,7 @@
---+ Details
-
+See Reasoning-using-Thea.txt
*/
View
135 owl2_reasoning_rules.pl
@@ -1,75 +1,106 @@
/* -*- Mode: Prolog -*- */
-:- table subClassOf/2.
-:- table subPropertyOf/2.
+:- module(owl2_reasoning_rules,[]).
+
+:- use_module(owl2_model).
+
+% yap will not allow us to table a predicate already declared dynamic..
+:- abolish(owl2_model:subClassOf/2).
+:- abolish(owl2_model:subPropertyOf/2).
+:- abolish(owl2_model:classAssertion/2).
+:- abolish(owl2_model:propertyAssertion/3).
+
+:- multifile owl2_model:subClassOf/2.
+:- multifile owl2_model:subPropertyOf/2.
+:- multifile owl2_model:classAssertion/2.
+:- multifile owl2_model:propetyAssertion/3.
+
+:- table owl2_model:subClassOf/2.
+:- table owl2_model:subPropertyOf/2.
+:- table owl2_model:classAssertion/2.
+:- table owl2_model:propertyAssertion/3.
+
+
%:- table member/2.
% ----------------------------------------
% TBox Reasoning
% ----------------------------------------
+someValuesFrom_propchain(_,[]).
+someValuesFrom_propchain(X,[P|PL]):-
+ subClassOf(X,someValuesFrom(P,Y)),
+ someValuesFrom_propchain(Y,PL).
+
+
+:- table subClassOf_all/2.
+owl2_model:subClassOf_all(_,[]).
+owl2_model:subClassOf_all(X,[D|L]):-
+ subClassOf(X,D),
+ subClassOf_all(X,L).
+
+:- table pairwise_equivalent_class/2.
+pairwise_equivalent_class(X,Y) :- equivalentClasses(L),member(X,L),member(Y,L).
+pairwise_equivalent_class(X,Y) :- subClassOf(X,Y),subClassOf(Y,X).
+
+:- table pairwise_disjoint_class/2.
+pairwise_disjoint_class(X,Y) :- disjointClasses(L),member(X,L),member(Y,L).
+pairwise_disjoint_class(X,Y) :- subClassOf(X,Y),subClassOf(Y,X).
+
% transitivity of subprop
-subPropertyOf(X,Y) :- subPropertyOf(X,Z),subPropertyOf(Z,Y).
+owl2_model:subPropertyOf(X,Y) :- subPropertyOf(X,Z),subPropertyOf(Z,Y).
% transitivity of subclass
-subClassOf(X,Y) :- subClassOf(X,Z),subClassOf(Z,Y).
+owl2_model:subClassOf(X,Y) :- subClassOf(X,Z),subClassOf(Z,Y).
-subClassOf(X,Y) :-
+owl2_model:subClassOf(X,Y) :-
pairwise_equivalent_class(X,Y).
-subClassOf(X,Y) :-
+owl2_model:subClassOf(X,Y) :-
pairwise_equivalent_class(X,intersectionOf(L)),
member(Y,L).
-subClassOf(X,Y) :-
+owl2_model:subClassOf(X,Y) :-
pairwise_equivalent_class(Y,unionOf(L)),
member(X,L).
-subClassOf(X,Y) :-
+owl2_model:subClassOf(X,Y) :-
pairwise_equivalent_class(Y,intersectionOf(L)),
subClassOf_all(X,L).
-subClassOf(X,someValuesFrom(P,D)) :-
- subClassOf(X,someValuesFrom(P,D1)),
- subClassOf(D1,D).
-subClassOf(X,someValuesFrom(P,D)) :-
- subClassOf(X,someValuesFrom(P1,D)),
- subPropertyOf(P1,P).
-subClassOf(X,someValuesFrom(P,D)) :-
- subClassOf(X,someValuesFrom(P,D1)),
- transitiveProperty(P),
- subClassOf(D1,someValuesFrom(P,D2)).
-subClassOf(X,someValuesFrom(P,D)) :-
- subClassOf(X,someValuesFrom(P1,D1)),
- subPropertyOf(propertyChain([P1,P2]),P), % TODO
- subClassOf(D1,someValuesFrom(P2,D2)).
-subClassOf(X,someValuesFrom(P,D)) :-
- subClassOf(X,someValuesFrom(P1,D1)),
- subPropertyOf(propertyChain([P1|PL]),P), % TODO
- someValuesFrom_propchain(D1,PL).
+owl2_model:subClassOf(X,someValuesFrom(P,D)) :-
+ subPropertyOf(P1,P),
+ subClassOf(X,someValuesFrom(P1,D)).
-someValuesFrom_propchain(_,[]).
-someValuesFrom_propchain(X,[P|PL]):-
- subClassOf(X,someValuesFrom(P,Y)),
- someValuesFrom_propchain(Y,PL).
+% this appears to cause a loop, even with tabling...
+%owl2_model:subClassOf(X,someValuesFrom(P,D)) :-
+% subClassOf(X,someValuesFrom(P,D1)),
+% subClassOf(D1,D).
-subClassOf(X,allValuesFrom(P,D)) :-
- subClassOf(X,allValuesFrom(P,D1)),
- subClassOf(D1,D).
+%owl2_model:subClassOf(X,someValuesFrom(P,Y)) :-
+% transitiveProperty(P),
+% subClassOf(X,someValuesFrom(P,someValuesFrom(P,Y))).
+owl2_model:subClassOf(X,someValuesFrom(P,Y)) :-
+ subClassOf(X,someValuesFrom(P,D)),
+ transitiveProperty(P),
+ subClassOf(D,someValuesFrom(P,Y)).
-:- table subClassOf_all/2.
-subClassOf_all(_,[]).
-subClassOf_all(X,[D|L]):-
- subClassOf(X,D),
- subClassOf_all(X,L).
+%
-:- table pairwise_equivalent_class/2.
-pairwise_equivalent_class(X,Y) :- equivalentClasses(L),member(X,L),member(Y,L).
-pairwise_equivalent_class(X,Y) :- subClassOf(X,Y),subClassOf(Y,X).
+/*
+owl2_model:subClassOf(X,allValuesFrom(P,D)) :-
+ subClassOf(X,allValuesFrom(P,D1)),
+ subClassOf(D1,D).
+ */
+%subClassOf(X,someValuesFrom(P,Y)) :-
+% subClassOf(X,someValuesFrom(P1,D1)),
+% subPropertyOf(propertyChain([P1,P2]),P), % TODO
+% subClassOf(D1,someValuesFrom(P2,D2)).
+%subClassOf(X,someValuesFrom(P,Y)) :-
+% subClassOf(X,someValuesFrom(P1,D1)),
+% subPropertyOf(propertyChain([P1|PL]),P), % TODO
+% someValuesFrom_propchain(D1,PL).
-:- table pairwise_disjoint_class/2.
-pairwise_disjoint_class(X,Y) :- disjointClasses(L),member(X,L),member(Y,L).
-pairwise_disjoint_class(X,Y) :- subClassOf(X,Y),subClassOf(Y,X).
% TODO: make subClassOf nothing?
:- table unsatisfiable/1.
@@ -84,18 +115,18 @@
% reified version of Grosof
-classAssertion(C,I) :- classAssertion(C2,I),subClassOf(C2,C).
+owl2_model:classAssertion(C,I) :- classAssertion(C2,I),subClassOf(C2,C).
-classAssertion(C,I) :- propertyDomain(P,C),propertyAssertion(P,I,_).
-classAssertion(C,I) :- propertyRange(P,C),propertyAssertion(P,_,I).
+owl2_model:classAssertion(C,I) :- propertyDomain(P,C),propertyAssertion(P,I,_).
+owl2_model:classAssertion(C,I) :- propertyRange(P,C),propertyAssertion(P,_,I).
-propertyAssertion(P,A,B) :- transitiveProperty(P),propertyAssertion(P,A,C),propertyAssertion(P,C,B).
-propertyAssertion(P,A,B) :- symmetricProperty(P),propertyAssertion(P,B,A).
-propertyAssertion(P,A,B) :- inverseProperties(P,Q),propertyAssertion(Q,B,A).
-propertyAssertion(Q,A,B) :- subPropertyOf(P,Q),propertyAssertion(P,A,B).
+owl2_model:propertyAssertion(P,A,B) :- transitiveProperty(P),propertyAssertion(P,A,C),propertyAssertion(P,C,B).
+owl2_model:propertyAssertion(P,A,B) :- symmetricProperty(P),propertyAssertion(P,B,A).
+owl2_model:propertyAssertion(P,A,B) :- inverseProperties(P,Q),propertyAssertion(Q,B,A).
+owl2_model:propertyAssertion(Q,A,B) :- subPropertyOf(P,Q),propertyAssertion(P,A,B).
% role chains
-propertyAssertion(P,A,B) :- subPropertyOf(propertyChain([P1|PL]),P),propertyAssertion(P,A,C),propertyAssertion_chain(PL,C,B).
+%propertyAssertion(P,A,B) :- subPropertyOf(propertyChain([P1|PL]),P),propertyAssertion(P,A,C),propertyAssertion_chain(PL,C,B).
propertyAssertion_chain([],_,_).
propertyAssertion_chain([P|PL],A,B) :- propertyAssertion(P,A,C),propertyAssertion_chain(PL,C,B).
View
9 owl2_util.pl
@@ -165,6 +165,15 @@
!.
use_label_as_IRI(X,X).
+use_property_as_IRI(Prop,IRI,NewIRI) :-
+ anyPropertyAssertion(Prop,IRI,Literal),
+ Literal=literal(type(_,Val)),
+ concat_atom([NS,Local],':',Val),
+ rdf_global_id(NS:Local,NewIRI),
+ !.
+use_property_as_IRI(X,X).
+
+
prefix_IRI(Pre,X,Y) :-
( entity(X) ; ontology(X)),
!,
View
25 rules/basicset.pl
@@ -26,10 +26,16 @@
entailed_2(classAssertion(C,I),EL) :-
+ nonvar(I),
classAssertion(C2,I),
debug(owl2_basic_reasoner,'testing ~w(~w) based on ~w(~w)',[C,I,C2,I]),
entailed(subClassOf(C2,C),EL).
+entailed_2(classAssertion(C,I),EL) :-
+ var(I),
+ entailed(subClassOf(C2,C),EL),
+ classAssertion(C2,I).
+
entailed_2(individual(I),_) :-
propertyAssertion(_,I,_).
@@ -52,14 +58,27 @@
% transitivity of subclass
% we avoid recursion by stratification - 10 cannot call a 5
% 10 is either asserted or a precalculated set of assertions based on eg equivalentClass
-entailed_5(subClassOf(X,Y),EL) :- entailed_10(subClassOf(X,Z),EL),\+member(X<Z,EL),entailed(subClassOf(Z,Y),[X<Z|EL]). % TODO: cycles
+entailed_5(subClassOf(X,Y),EL) :-
+ nonvar(X),
+ debug(reasoner,'[trans-up] testing for ~w',[subClassOf(X,Y)]),
+ entailed_10(subClassOf(X,Z),EL),\+member(X<Z,EL),entailed(subClassOf(Z,Y),[X<Z|EL]). % TODO: cycles
+entailed_5(subClassOf(X,Y),EL) :-
+ var(X),
+ debug(reasoner,'[trans-dn] testing for ~w',[subClassOf(X,Y)]),
+ entailed_10(subClassOf(Z,Y),EL),\+member(Z<Y,EL),entailed(subClassOf(X,Z),[Z<Y|EL]). % TODO: cycles
% subclass over existential restrictions
% X < P some Y :- X < P some YY, YY < Y
-entailed_5(subClassOf(X,someValuesFrom(P,Y)), EL) :-
+% TODO - fix this - cause of non-termination
+xxxxxxxxentailed_5(subClassOf(X,someValuesFrom(P,Y)), EL) :-
+ class(X),
+ debug(reasoner,'testing for ~w',[subClassOf(X,someValuesFrom(P,Y))]),
subClassOf(X,someValuesFrom(P,YY)),
- subClassOf(YY,Y),
+ debug(reasoner,' testing for ~w',[subClassOf(YY,Y)]),
+ class(YY),
+ entailed(subClassOf(YY,Y),[P-X-YY|EL]),
+ class(Y),
\+ member(X<someValuesFrom(P,Y),EL).
View
12 testfiles/cell.owlpl
@@ -16,7 +16,19 @@ equivalentClasses([n_cell,intersectionOf([cell,someValuesFrom(has_part,nuc)])]).
equivalentClasses([e_cell,intersectionOf([cell,allValuesFrom(has_part,complementOf(nuc))])]).
%equivalentClasses([cell,unionOf([e_cell,n_cell])]).
subClassOf(cell,unionOf([e_cell,n_cell])).
+
objectProperty(part_of).
objectProperty(has_part).
objectProperty(develops_from).
+transitiveProperty(has_part).
+inverseProperties(part_of,has_part).
+
+subClassOf(cell,material_anatomical_entity).
+subClassOf(neuron,cell).
+subClassOf(interneuron,neuron).
+
+subClassOf(nucleus,someValuesFrom(part_of,cell)).
+subClassOf(nucleolus,someValuesFrom(part_of,nucleus)).
+subClassOf(mt_nucleus,nucleus).
+classAssertion(interneuron,n1).
View
8 thea.pl
@@ -0,0 +1,8 @@
+
+:-use_module('owl2_model.pl').
+:-use_module('owl2_from_rdf.pl').
+:-use_module('owl2_export_rdf.pl').
+:-use_module('owl2_xml.pl').
+:-use_module('owl2_util.pl').
+:-use_module('owl2_io.pl').
+

0 comments on commit 898d4aa

Please sign in to comment.
Something went wrong with that request. Please try again.