%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%% %%%%%%%%%%%%%%% %%%%%%%%%%%% OWL Reasoner %%%%%%%%%%%%%%% %%%%%%%%%%%% ALCAS is an ALC Reasoner for CAS %%%%%%%%%%%%%%% %%%%%%%%%%%% %%%%%%%%%%%%%%% %%%%%%%%%%%% ALC is Attributive Language with Complements %%%%%%%%%%%%%%% %%%%%%%%%%%% CAS is the Concrete Abstract Syntax %%%%%%%%%%%%%%% %%%%%%%%%%%% see http://owl.man.ac.uk/2003/concrete/latest/ %%%%%%%%%%%%%%% %%%%%%%%%%%% %%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- set_prolog_flag(debugger_print_options, [quoted(true), portray(true), max_depth(100)]). :- set_prolog_flag(toplevel_print_options, [quoted(true), portray(true), max_depth(100)]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%% OWL Parser %%%%%%%%%%%%%%% %%%%%%%%%%%% Parser for Concrete Abstract Syntax %%%%%%%%%%%%%%% %%%%%%%%%%%% based on Definite Clause Grammars %%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ontology(O) --> namespaces(NSs), ['Ontology('], ontologyIDq(ID), directives(Directives), [')'], {O = ontology(NSs, ID, Directives)}. directive(D) --> ['Annotation('], ( ontologyPropertyID(OPID), ontologyID(OID), {D = annotation(OPID, OID)} | annotationPropertyID(APID), uriReference(URI), {D = annotation(APID, URI)} | annotationPropertyID(APID), dataLiteral(DL), {D = annotation(APID, DL)} | annotationPropertyID(APID), individual(Ind), {D = annotation(APID, Ind)} ), [')'] | fact(F), {D = F} | axiom(A), {D = A}. fact(F) --> individual(F) | ['SameIndividual('], individualID(IID), individualIDp(IIDs), [')'], {F = sameIndividual(IID, IIDs)} | ['DifferentIndividuals('], individualID(IID), individualIDp(IIDs), [')'], {F = differentIndividuals([IID | IIDs])}. individual(Ind) --> ['Individual('], individualIDq(IIDs), annotations(As), type_phrases(TPs), values(Vs), [')'], {Ind = individual(IIDs, As, TPs, Vs)}. value(V) --> ['value('], ( individualvaluedPropertyID(PID), individualID(L) | individualvaluedPropertyID(PID), individual(L) | datavaluedPropertyID(PID), dataLiteral(L) ), [')'], {V = value(PID, L)}. type(T) --> description(D), {T = type(D)}. axiom(Ax) --> ['Class('], classID(CID), deprecatedq(DQ), modality(M), annotations(Ans), descriptions(Ds), [')'], {Ax = class(CID, DQ, M, Ans, Ds)} | ['EnumeratedClass('], classID(CID), deprecatedq(Dq), annotations(Ans), individualIDs(IIDs), [')'], {Ax = enumeratedClass(CID, Dq, Ans, IIDs)} | ['DisjointClasses('], description(D), descriptionp(Dp), [')'], {Ax = disjointClasses([D | Dp])} | ['EquivalentClasses('], description(D), descriptions(Ds), [')'], {Ax = equivalentClasses([D | Ds])} | ['SubClassOf('], description(D1), description(D2), [')'], {Ax = subClassOf(D1, D2)} | ['Datatype('], datatypeID(DID), deprecatedq(Depq), annotations(Ans), [')'], {Ax = datatype(DID, Depq, Ans)} | ['DatatypeProperty('], datavaluedPropertyID(DID), deprecatedq(Depq), annotations(Ans), super_data_phrases(SDPs), functionalq(Funq), domain_phrases(DPs), range_phrases(RPs), [')'], {Ax = datatypeProperty(DID, Depq, Ans, SDPs, Funq, DPs, RPs)} | ['ObjectProperty('], individualvaluedPropertyID(IVPID), deprecatedq(Depq), annotations(Ans), super_individual_phrases(SDPs), inverse_individual_phraseq(IIPq1), inverse_individual_phraseq(IIPq2), symmetricq(Sq), functional_or_inverse_functional_or_transitiveq(FIFT), domain_phrases(DPs), range_description_phrases(RDPs), [')'], {Ax = objectProperty(IVPID, Depq, Ans, SDPs, IIPq1, IIPq2, Sq, FIFT, DPs, RDPs)} | ['AnnotationProperty('], annotationPropertyID(APID), annotations(As), [')'], {Ax = annotationProperty(APID, As)} | ['OntologyProperty('], ontologyPropertyID(OntID), annotations(As), [')'], {Ax = ontologyProperty(OntID, As)} | ['EquivalentProperties('], datavaluedPropertyID(ID1), datavaluedPropertyID(ID2), datavaluedPropertyIDs(IDs), [')'], {Ax = equivalentProperties([ID1, ID2 | IDs])} | ['EquivalentProperties('], individualvaluedPropertyID(ID1), individualvaluedPropertyID(ID2), individualvaluedPropertyIDs(IDs), [')'], {Ax = equivalentProperties([ID1, ID2 | IDs])} | ['SubPropertyOf('], datavaluedPropertyID(ID1), datavaluedPropertyID(ID2), [')'], {Ax = subPropertyOf(ID1, ID2)} | ['SubPropertyOf('], individualvaluedPropertyID(ID1), individualvaluedPropertyID(ID2), [')'], {Ax = subProperty(ID1, ID2)}. modality(V) --> ['complete'], {V = complete} | ['partial'], {V = partial}. description(D) --> classID(C), {D = C} | restriction(R), {D = R} | ['unionOf('], descriptions(Ds), [')'], {D = unionOf(Ds)} | ['intersectionOf('], descriptions(Ds), [')'], {D = intersectionOf(Ds)} | ['complementOf('], description(Dc), [')'], {D = complementOf(Dc)} | ['oneOf('], individualIDs(Is), [')'], {D = oneof(Is)}. restriction(R) --> ['restriction('], ( datavaluedPropertyID(DID), dataRestrictionComponent(DR), dataRestrictionComponents(DRs), {R = restriction(DID, [DR | DRs])} | individualvaluedPropertyID(IID), individualRestrictionComponent(IR), individualRestrictionComponents(IRs), {R = restriction(IID, [IR | IRs])} ), [')']. dataRestrictionComponent(R) --> ['allValuesFrom('], dataRange(DR), [')'], {R = allValuesFrom(DR)} | ['someValuesFrom('], dataRange(DR), [')'], {R = someValuesFrom(DR)} | ['value('], dataLiteral(DL), [')'], {R = value(DL)} | cardinality(C), {R = C}. individualRestrictionComponent(R) --> ['allValuesFrom('], description(D), [')'], {R = allValuesFrom(D)} | ['someValuesFrom('], description(D), [')'], {R = someValuesFrom(D)} | ['value('], individualID(IID), [')'], {R = value(IID)} | cardinality(C), {R = C}. cardinality(C) --> ['minCardinality('], [nnint(I)], [')'], {C = minCardinality(I)} | ['maxCardinality('], [nnint(I)], [')'], {C = maxCardinality(I)} | ['cardinality('], [nnint(I)], [')'], {C = cardinality(I)}. dataRange(DR) --> datatypeID(DR) | ['rdfs:Literal'] | ['oneOf('], dataLiterals(DLs), [')'], {DR = oneOf(DLs)}. datatypeID(URI) --> uriReference(URI). classID(URI) --> uriReference(URI). individualID(URI) --> uriReference(URI). ontologyID(URI) --> uriReference(URI). datavaluedPropertyID(URI) --> uriReference(URI). individualvaluedPropertyID(URI) --> uriReference(URI). annotationPropertyID(URI) --> uriReference(URI). ontologyPropertyID(URI) --> uriReference(URI). annotation(An) --> ['annotation(' ], ( annotationPropertyID(APID), uriReference(A) | annotationPropertyID(APID), dataLiteral(A) | annotationPropertyID(APID), individual(A) ), [')'], {An = annotation(APID, A)}. %%%%%%%%%%%%%%%%%%%% Extended Rules %%%%%%%%%%%%%%%%%%%%%%%% namespace(namespace(Prefix, URI)) --> ['Namespace(', Prefix, '=', absURI(URI), ')']. %%%%%%%%%%%%%%%%%%%% Generated productions for +, * and ? %%%%%%%%%%%%%%%%%%%%%%%% namespaces([NS | NSs]) --> namespace(NS), namespaces(NSs). namespaces([]) --> []. ontologyIDq(ontologyID(ID)) --> ontologyID(ID). ontologyIDq(anonymous) --> []. directives([D | Ds]) --> directive(D), directives(Ds). directives([]) --> []. dataLiterals([DL | DLs]) --> dataLiteral(DL), dataLiterals(DLs). dataLiterals([]) --> []. type_phrase(type(Type)) --> ['type('], type(Type), [')']. type_phrases([TP | TPs]) --> type_phrase(TP), type_phrases(TPs). type_phrases([]) --> []. individualIDq([I]) --> individualID(I). individualIDq([]) --> []. individualIDp([I | Is]) --> individualID(I), individualIDs(Is). individualIDs([I | Is]) --> individualID(I), individualIDs(Is). individualIDs([]) --> []. annotations([An | Ans]) --> annotation(An), annotations(Ans). annotations([]) --> []. deprecatedq([deprecated]) --> ['Deprecated']. deprecatedq([]) --> []. descriptionp([D | Ds]) --> description(D), descriptions(Ds). descriptions([D | Ds]) --> description(D), descriptions(Ds). descriptions([]) --> []. super_data_phrases([SP | SPS]) --> super_data_phrase(SP), super_data_phrases(SPS). super_data_phrases([]) --> []. super_data_phrase(super(DID)) --> ['super('], datavaluedPropertyID(DID), [')']. super_individual_phrases([I | Is]) --> super_individual_phrase(I), super_individual_phrases(Is). super_individual_phrases([]) --> []. super_individual_phrase(super(I)) --> ['super('], individualvaluedPropertyID(I), [')']. functionalq([functional]) --> ['Functional']. functionalq([]) --> []. domain_phrases([D | Ds]) --> domain_phrase(D), domain_phrases(Ds). domain_phrases([]) --> []. domain_phrase(domain(D)) --> ['domain('], description(D), [')']. range_phrases([R | Rs]) --> range_phrase(R), range_phrases(Rs). range_phrases([]) --> []. range_phrase(range(R)) --> ['range('], dataRange(R), [')']. range_description_phrases([P | Ps]) --> range_description_phrase(P), range_description_phrases(Ps). range_description_phrases([]) --> []. range_description_phrase(range(D)) --> ['range('], description(D), [')']. inverse_individual_phraseq([I]) --> inverse_individual_phrase(I). inverse_individual_phraseq([]) --> []. inverse_individual_phrase(inverseOf(IP)) --> ['inverseOf('], individualvaluedPropertyID(IP), [')']. symmetricq([S]) --> symmetric(S). symmetricq([]) --> []. symmetric(symmetric) --> ['Symmetric']. dataRestrictionComponents([D | Ds]) --> dataRestrictionComponent(D), dataRestrictionComponents(Ds). dataRestrictionComponents([]) --> []. individualRestrictionComponents([R | Rs]) --> individualRestrictionComponent(R), individualRestrictionComponents(Rs). individualRestrictionComponents([]) --> []. functional_or_inverse_functional_or_transitiveq([V]) --> functional_or_inverse_functional_or_transitive(V). functional_or_inverse_functional_or_transitiveq([]) --> []. functional_or_inverse_functional_or_transitive(V) --> ['Functional'], {V = functional} | ['InverseFunctional'], {V = inverseFunctional} | ['Transitive'], {V = transitive} . datavaluedPropertyIDs([DP | DPs]) --> datavaluedPropertyID(DP), datavaluedPropertyIDs(DPs). datavaluedPropertyIDs([]) --> []. individualvaluedPropertyIDs([IP | IPs]) --> individualvaluedPropertyID(IP), individualvaluedPropertyIDs(IPs). individualvaluedPropertyIDs([]) --> []. values([]) --> []. values([V | Vs]) --> value(V), values(Vs). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%% Tokenizer %%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%% URI %%%%%%%%%%%%%%%%%%%%%%%%%% uriReference(uri(URI)) --> [absURI(URI)] ; qname(URI). qname(Prefix : LocalName) --> [Prefix], [':'], {!}, [LocalName]. prefix(Letters) --> letters(Letters). %%%%%%%%%%%%%%%%%%%%%%%%% dataLiteral %%%%%%%%%%%%%%%%%%%%%% dataLiteral(DL) --> langString(DL) | datatypeString(DL). langString(langString(S,'@',Lang)) --> [string(S), '@', Lang]. datatypeString(datatypeString(S, '^^', URI)) --> [string(S), '^^'], uriReference(URI). %%%%%%%%%%%%%%%%%%%%%%%%% Integers %%%%%%%%%%%%%%%%%%%%%% non_negative_integer(nnint(I)) --> digit(D0), digits(D), { number_chars(I, [D0|D]) }. digits([D|T]) --> digit(D), !, digits(T). digits([]) --> []. digit(D) --> [D], { code_type(D, digit) }. %%%%%%%%%%%%%%%%%%%%%%%%% Localname %%%%%%%%%%%%%%%%%%%%%% localname(localname(Id)) --> letter(L0), alphanumerics_or_underscores(L), { name(Id, [L0|L]) }. alphanumeric_or_underscore(A) --> [A], { code_type(A, alnum) }. alphanumeric_or_underscore('_') --> ['_']. alphanumerics_or_underscores([A|As]) --> alphanumeric_or_underscore(A), !, alphanumerics_or_underscores(As). alphanumerics_or_underscores([]) --> []. %%%%%%%%%%%%%%%%%%%%% Tokensize and remove comments %%%%%%%%%%%%%%%%%%%%%%%%%%% tokenize([]) --> []. tokenize(Tokens) --> [Code], {code_type(Code, space), !}, tokenize(Tokens). tokenize(Tokens) --> "//", {!}, slash_slash_comment, tokenize(Tokens). tokenize(Tokens) --> "/*", {!}, slash_star_comment, tokenize(Tokens). tokenize([Token | Tokens]) --> token(Token),!, tokenize(Tokens). slash_slash_comment --> [10], {!}. slash_slash_comment --> [_], %any char slash_slash_comment. slash_star_comment --> "*/", {!}. slash_star_comment --> [_], %any char slash_star_comment. token('=') --> "=", !. token(')') --> ")", !. token(':') --> ":", !. token(URI) --> "<", !, absoluteURI(URI), ">". %languageTags not implemented yet % token(langString(LangString)) --> % "\"",!, % non_double_quote_codes(Codes), % "@", % {name(LangString, Codes)}. token(string(Str)) --> "\"", !, non_double_quote_codes(Codes), {name(Str, Codes)}. token('@') --> "@". token('^^') --> "^^". token(I) --> non_negative_integer(I). token(T) --> letter(C), idEndsWithLfParenOrNonAlnum(Codes), {name(T, [C|Codes])}. non_double_quote_codes([]) --> "\"",!. non_double_quote_codes([R|Cs]) --> "\\", [C], {([C] = "\\" -> R = C; [C] = "\"" -> R = C)}, non_double_quote_codes(Cs). non_double_quote_codes([C|Cs]) --> [C], non_double_quote_codes(Cs). idEndsWithLfParenOrNonAlnum("(") --> "(", !. idEndsWithLfParenOrNonAlnum([C|Cs]) --> [C], {code_type(C, alnum) ; [C]=="_"}, !, idEndsWithLfParenOrNonAlnum(Cs). idEndsWithLfParenOrNonAlnum([]) --> []. letter(A) --> [A],{code_type(A, alpha)}. absoluteURI(absURI(URI)) --> non_right_angle_characters(Cs), {name(URI, Cs)}. non_right_angle_characters([C | Cs]) --> [C], {[C] \= ">"}, !, non_right_angle_characters(Cs). non_right_angle_characters([]) --> []. %%%%%%%%%%%%%%% Queries in the file %%%%%%%%%%%%%%%%%%%%%%%%%%%% querySet(Qs) --> ['Query('], queries(Qs), [')']. queries([]) --> []. queries([Q | Qs]) --> query(Q), queries(Qs). query(Q) --> ( ['ClassSubsumes('], description(D1), description(D2), [')'], {E = classSubsumes(D1, D2)} | ['ClassEquivalent('], description(D1), description(D2), [')'], {E = classEquivalent(D1, D2)} ), {Q = query(E)}. %%%%%%%%%%%%%%%%%%%%%%%%%% Top Level Parser Call %%%%%%%%%%%%%%%%%%%%%%%%%% readCAS(File, Ont, Qs) :- read_file_to_codes(File, Codes, []), !, write('File Read'), nl, phrase(tokenize(T), Codes, []), !, write('Tokenized'), nl, phrase(ontology(Ont), T, T2), !, write('Parsed Ontology'), nl, %pretty_print(Ont), phrase(querySet(Qs), T2, []), !, write('Parsed Queries'), nl. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%% %%%%%%%%%%%%%%% %%%%%%%%%%% OWL Reasoner %%%%%%%%%%%%%%% %%%%%%%%%%%% %%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% run(File) :- statistics(runtime, _), readCAS(File, Ontology, Queries), write('File parsed: '), statistics(runtime, [_, Elapsed1]), write(Elapsed1), write(' msec'), nl, !, ontologyToBoxes(Ontology, TBox, _ABox), %pretty_print(TBox), unfold(TBox, Base, T), !, write('Unfolded: '), statistics(runtime, [_, Elapsed2]), write(Elapsed2), write(' msec'), nl, runQueries(Base, T, 1, Queries). ontologyToBoxes(ontology(_NameSpaces, _Name, Directives), TBox, ABox) :- directivesToBoxes(Directives, [], TBox, [], ABox). directivesToBoxes([], T, T, A, A). directivesToBoxes([D | Ds], T0, T, A0, A) :- directiveToBoxes(D, T0, T1, A0, A1), directivesToBoxes(Ds, T1, T, A1, A). directiveToBoxes(D, T, [Ax|T], A, A):- D = class(ClassID, _Depq, Mode, _Annotations, Descriptions), descriptionsToIntersectExpr(Descriptions, IntersectExpr), ( Mode = complete -> Ax = eq(ClassID, IntersectExpr); Mode = partial -> Ax = sub(ClassID, IntersectExpr) ). % %directiveToBoxes(D, T, T, A, [Ax | A]):- % D = individual(IIDs, Annotations, TypePhrases, Values), /* Here we need to process the individual declarations so that all type phrases and values are translated into the format for the tableau reasoner Individual(pp:Rex type(pp:dog) value(pp:is_pet_of pp:Mick)) on input becomes Individual(pp:Rex type(pp:dog) value(pp:is_pet_of pp:Mick)) */ descriptionsToIntersectExpr([Desc], Expr) :- descriptionToExpr(Desc, Expr). descriptionsToIntersectExpr([D | Ds], intersect(E1, E2)) :- Ds \= [], descriptionToExpr(D, E1), descriptionsToIntersectExpr(Ds, E2). descriptionsToUnionExpr([Desc], Expr) :- descriptionToExpr(Desc, Expr). descriptionsToUnionExpr([D | Ds], union(E1, E2)) :- Ds \= [], descriptionToExpr(D, E1), descriptionsToUnionExpr(Ds, E2). descriptionToExpr(unionOf(Ds), E) :- descriptionsToUnionExpr(Ds, E). descriptionToExpr(intersectionOf(Ds), E) :- descriptionsToIntersectExpr(Ds, E). descriptionToExpr(complementOf(D), not(E)) :- descriptionToExpr(D, E). descriptionToExpr(restriction(PropID, RestrictionComponents), Expr):- restrictionsToIntersectionExpr(RestrictionComponents, PropID, Expr). %more directives to do, but the reasoning engine does not support anything else yet. descriptionToExpr(uri(X), uri(X)). % restriction(prop someValuesFrom(intersect(c d))) --> some(prop, intersect(c, d)) restrictionsToIntersectionExpr([R], PropID, Expr) :- restrictionToExpr(R, PropID, Expr). restrictionsToIntersectionExpr([R | Rs], PropID, intersect(E, Es)):- Rs \= [], restrictionToExpr(R, PropID, E), restrictionsToIntersectionExpr(Rs, PropID, Es). %restriction(r [allValuesFrom(a)]) --> all(r, a) restrictionToExpr(allValuesFrom(Desc), PropID, all(PropID, Expr)) :- descriptionToExpr(Desc, Expr). %restriction(r [someValuesFrom(b)]) --> some(r, b) restrictionToExpr(someValuesFrom(Desc), PropID, some(PropID, Expr)) :- descriptionToExpr(Desc, Expr). runQueries(_Base, _T, _, []). runQueries(Base, T, N, [Q | Qs]) :- runQuery(Base, T, N, Q), N1 is N + 1, runQueries(Base, T, N1, Qs). runQuery(Base, T, N, query(classSubsumes(C1, C2))) :- traceMessage(1, ['Query ', N, ') ', classSubsumes(C1, C2)]), descriptionToExpr(C1, E1), descriptionToExpr(C2, E2), expandConcept(E1, T, Base, E1E), expandConcept(E2, T, Base, E2E), traceMessage(1, ['Query ', N, ' after expanding ', classSubsumes(E1E, E2E)]), runAndReport(N, conceptSubsumedBy(E2E, E1E)). runQuery(Base, T, N, query(classEquivalent(C1, C2))) :- traceMessage(1, ['Query (#', N, ') ', classEquivalent(C1, C2)]), descriptionToExpr(C1, E1), descriptionToExpr(C2, E2), expandConcept(E1, T, Base, E1E), expandConcept(E2, T, Base, E2E), traceMessage(1, ['Query ', N, ' after expanding ', classEquivalent(C1, C2)]), runAndReport(N, conceptEquivalent(E2E, E1E)). runAndReport(N, Q) :- write('Query (#'), write(N), write(')'), nl, write(' '), %write(Q), nl, Q,!, write(' yes '), statistics(runtime, [_, Elapsed]), write(Elapsed), write(' msec'), nl. runAndReport(_, _) :- write(' no '), statistics(runtime, [_, Elapsed]), write(Elapsed), write(' msec'), nl. % Description Logic Engine in Prolog, Tableau algorithm % based on slides from Volker Haarslev, Concordia U, Montreal, Canada % % Concept Construction Syntax % top % bottom % not(A) % union(C, D) % intersect(C, D) % all(R, C) % some(R, C) % atleast(n, R) % atleast(n, R, C) % atmost(n, R) % atmost(n, R, C) % % Syntax of Terminologies % equivalent % implies (means is subsumed by) % % Syntax of Questions about Concepts % sat(C), unsat(C) means (resp.) is C satisfiable, unsatisfiable? % disjoint(C, D) means are C and D disjoint % conceptSubsumedBy(C, D) means does C imply D, or is C subsumed by D? % conceptEquivalent(C, D) means are C and D equivalent concepts? conceptSubsumedBy(C, D) :- unsat(intersect(C, not(D))). conceptEquivalent(C, D) :- conceptSubsumedBy(C, D), conceptSubsumedBy(D, C). unsat(C) :- \+ sat(C). sat(C) :- freshIndividual(I), nnfAll([I:C], NewNNF), traceMessage(1, ['Testing sat of ', NewNNF]), tt_new(NewNNF, [], []). tt_new(New, L, LD) :- (clashL(New, L, LD, Clash) -> traceMessage(1, ['Clash found ', Clash]), fail ; insertNew(New, L, L1), tt(L1, LD) ). clashL(New, L, LD, Clash) :- clash(L, New, Clash); clash(LD, New, Clash). clashL(New, _, _, A:E1):- orderedPair(New, A:E1, A:E2), comp(E1, E2). tt([], LD) :- %nothing left to try. LD is a model. traceMessage(1, ['Model is ', LD]). tt(L, LD) :- select(L, Act, L1), %select is don't care non-deterministic, assuming calculus is confluent !, traceMessage(1, ['Selecting ', Act]), traceMessage(1, ['Leaving tableau ', L, ' and ', LD]), tt(Act, L1, LD). %Conjunction rule tt(Act, L, LD):- Act = A:intersect(C, D), !, traceMessage(1, ['Apply conjunction rule. ']), (inL(A:C, L, LD) -> (inL(A:D, L, LD) -> % both already in, so inactivate Act traceMessage(1, ['Both conjuncts already in. ']), tt(L, [Act | LD]) ; %A:C is in, so add A:D and inactivate Act traceMessage(1, ['Adding ', A:D]), tt_new([A:D], L, [Act | LD]) ); (inL(A:D, L, LD) -> %A:D is is, so add A:C and inactivate Act traceMessage(1, ['Adding ', A:C]), tt_new([A:C], L, [Act | LD]) ; %neither is in, so add both and inactivate traceMessage(1, ['Adding ', A:C, ' and ', A:D]), tt_new([A:C, A:D], L, [Act | LD]) ) ). %Disjunction rule tt(Act, L, LD) :- Act = A:union(C, D), !, traceMessage(1, ['Apply disjunction rule.']), ((inL(A:C, L, LD);inL(A:D, L, LD)) -> % One or both are in traceMessage(1, ['One or both disjuncts already in. ']), tt(L, [Act | LD]) ; %neither is in, so apply disjunction rule traceMessage(1, ['Splitting. ']), (tt_new([A:C], L, [Act| LD]); tt_new([A:D], L, [Act | LD])) ). %Role exists restriction rule tt(Act, L, LD) :- Act = A:some(R, C), !, traceMessage(1, ['Applying role-exists rule. ']), (subsetL([[A,B]:R, B:C], L, LD) -> traceMessage(1, ['Witness ', B, ' already exists in that role. ']), tt(L, [Act | LD]) ; freshIndividual(B), traceMessage(1, ['Fresh individual ', B, ' for witness ', B:C, ' and ', [A,B]:R]), tt_new([[A,B]:R, B:C], L, LD) ). %Role value restriction rule tt(Act, L, LD) :- Act = A:all(R, C), traceMessage(1, ['Applying role-value restriction rule']), inL([A,B]:R, L, LD), \+ inL(B:C, L, LD), traceMessage(1, ['Role-value ', B:C, ' added for ', [A,B]:R]), !, tt_new([B:C], L, [Act | LD]). tt(Act, L, LD) :- Act = _A:all(_R, C), traceMessage(1, ['No new role-value ', C, ' to add.']), !, tt(L, [Act | LD]). tt(Act, L, LD) :- Act = [A, B] : R, member(A:all(R, C), LD), \+ inL(B:C, L, LD), traceMessage(1, ['Role value. Adding ', B:C, ' since ', A:all(R, C)]), !, tt_new([B:C, A:all(R, C)], [Act | L], LD). %Move a-box assertions into LD tt(Act, L, LD) :- Act = [_A, _B] : _R, traceMessage(1, ['Moved a-box assertion to LD']), !, tt(L, [Act | LD]). tt(Act, L, LD) :- Act = _A : _R, traceMessage(1, ['Moved a-box assertion to LD']), %leafLevelConcept(R), !, tt(L, [Act | LD]). tt(Act, L, LD) :- traceMessage(1, ['No tableau expansion was found for ', Act, ' with L ', L, LD]). clash(L1, L2, A:C) :- member(A:C, L1), comp(C, NotC), member(A:NotC, L2). comp(not(X), X):-!. comp(X, not(X)). % Negation Normal Form nnf(not(A:C), A:NCNNF) :- nnfConcept(not(C), NCNNF). nnf(A : C, A : CNNF) :- nnfConcept(C, CNNF). %nnf(not([A, B]:R), [A,B]: NRNNF) :- % nnfRole(not(R), NRNNF). %Not sure if one can state that A does not have B for its role R. % probably not. nnfConcept(not(not(C)), NNFC) :- !, nnfConcept(C, NNFC). nnfConcept(not(intersect(B, C)), union(NBNNF, NCNNF)) :- !, nnfConcept(not(B), NBNNF), nnfConcept(not(C), NCNNF). nnfConcept(not(union(B, C)), intersect(NBNNF, NCNNF)) :- !, nnfConcept(not(B), NBNNF), nnfConcept(not(C), NCNNF). nnfConcept(not(some(R, C)), all(R, NCNNF)) :- !, nnfConcept(not(C), NCNNF). nnfConcept(not(all(R, C)), some(R, NCNNF)) :- !, nnfConcept(not(C), NCNNF). nnfConcept(intersect(B, C), intersect(NNFB, NNFC)) :- !, nnfConcept(B, NNFB), nnfConcept(C, NNFC). nnfConcept(union(B, C), union(NNFB, NNFC)) :- !, nnfConcept(B, NNFB), nnfConcept(C, NNFC). nnfConcept(all(R, C), all(R, CNNF)) :- !, nnfConcept(C, CNNF). nnfConcept(some(R, C), some(R, CNNF)) :- !, nnfConcept(C, CNNF). nnfConcept(not(C), not(C)) :- !. nnfConcept(C, C) :- !. nnfAll([], []). nnfAll([E1 | L1], [E2 | L2]) :- nnf(E1, E2), nnfAll(L1, L2). % Expand the T-Box %expandTBox([], % Handling insertion insertNew(L1, L2, L) :- append(L1, L2, L). select(L1, Act, L2) :- memberFrom(Act, L1, L2). %utility functions memberFrom(E, [E|L], L). memberFrom(E, [E1|L], [E1|L2]):- memberFrom(E, L, L2). replaceMember(E1, E2, [E1 | L], [E2 | L]). replaceMember(E1, E2, [E | L1], [E | L2]) :- replaceMember(E1, E2, L1, L2). inL(A, L, _LD) :- member(A, L). inL(A, _L, LD) :- member(A, LD). subsetL([], _L, _LD). subsetL([E | Rest], L, LD):- inL(E, L, LD), subsetL(Rest, L, LD). orderedPair(L, E1, E2) :- append(_, [E1 | L1], L), append(_, [E2 | _], L1). bump(N) :- (retract(myCounter(N1)) -> N is N1 + 1, assert(myCounter(N)) ; assert(myCounter(1)), N = 1). :- dynamic(myCounter). freshIndividual(X) :- bump(N), name(N, Codes), name(X, [36 | Codes]). %36 is ascii for $ freshConcept(X) :- bump(N), name(N, Codes), name(X, [37 | Codes]). %37 is ascii for % %%%%%%%%%%%%%%%%%%%% traceMessage(N, M) :- verbose(V), V >= N, !, writeAll(M), nl. traceMessage(_, _). writeAll([]). writeAll([E | L]):- write(E), writeAll(L). :- dynamic(verbose/1). % verbose 0 means verbose is turned off % verbose 1 means show what expressions are selected, trace sort % verbose 2 means also show what expansion steps are done verbose(2). % ************************************** %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %expand T-Box unfold(TBox0, Base, TBox) :- tbox2graph(TBox0, G), baseConcepts(G, [], Base), expandTBox(G, Base, TBox0, TBox). displayTBox([]). displayTBox([eq(A, B) | TBox]) :- write(eq(A, B)), nl, displayTBox(TBox). tbox2graph(TBox, V):- tbox2graph(TBox, [], V). tbox2graph([], G, G). tbox2graph([eq(Concept, Expression) | TBox], G0, G) :- findAndInsertEdge(Concept, Expression, G0, G1), tbox2graph(TBox, G1, G). tbox2graph([sub(Concept, Expression) | TBox], G0, G) :- freshConcept(C), tbox2graph([eq(Concept, intersect(Expression, C)) | TBox], G0, G). findAndInsertEdge(C, not(Expression), G0, G) :- !, findAndInsertEdge(C, Expression, G0, G). findAndInsertEdge(C, intersect(E1, E2), G0, G) :- !, findAndInsertEdge(C, E1, G0, G1), findAndInsertEdge(C, E2, G1, G). findAndInsertEdge(C, union(E1, E2), G0, G) :- !, findAndInsertEdge(C, E1, G0, G1), findAndInsertEdge(C, E2, G1, G). findAndInsertEdge(C, all(_R, E), G0, G) :- !, findAndInsertEdge(C, E, G0, G). findAndInsertEdge(C, some(_R, E), G0, G) :- !, findAndInsertEdge(C, E, G0, G). findAndInsertEdge(_C, atleast(_N, _R), G, G) :- !. findAndInsertEdge(_C, atmost(_N, _R), G, G) :- !. findAndInsertEdge(C, atleast(_N, _R, E), G0, G) :- !, findAndInsertEdge(C, E, G0, G). findAndInsertEdge(C, atmost(_N, _R, E), G0, G) :- !, findAndInsertEdge(C, E, G0, G). findAndInsertEdge(C, E, G0, G) :- insertEdge(C, E, G0, G). insertEdge(To, From, G0, G):- FromNode = node(From, AdjFrom, InDegFrom), ensureExists(FromNode, NewFromNode, G0, G1), ToNode = node(To, AdjTo, InDegTo), ensureExists(ToNode, NewToNode, G1, G), %add To to the adjacency list of From NewFromNode = node(From, [To | AdjFrom], InDegFrom), %add one to In Degree of To node InDegTo1 is InDegTo+1, NewToNode = node(To, AdjTo, InDegTo1). ensureExists(Node1, Node2, [], [Node2]) :- Node1 = node(_N, [], 0). ensureExists(Node1, Node2, [Node1 | G], [Node2 | G]). ensureExists(Node1, Node2, [Node | G1], [Node | G2]) :- ensureExists(Node1, Node2, G1, G2). baseConcepts([], B, B). baseConcepts([node(C, _, 0) | G], B0, [C | B]) :- baseConcepts(G, B0, B). baseConcepts([node(_C, _, N) | G], B0, B) :- N >= 1, baseConcepts(G, B0, B). expandTBox([], _Base, TBox, TBox) :- !. expandTBox(G0, Base, TBox0, TBox) :- memberFrom(node(C, AdjList, 0), G0, G1), !, traceMessage(1, ['Topological sorted concept ', C]), reduceInDegOfAdj(AdjList, C, Base, G1, G, TBox0, TBox1), expandTBox(G, Base, TBox1, TBox). expandTBox(_, _, TBox, _) :- write('**** TBox is cyclic ****'), nl, write(TBox), nl, abort. reduceInDegOfAdj([], _, _, G, G, TBox, TBox). reduceInDegOfAdj([Adj | List], C, Base, G0, G, TBox0, TBox) :- replaceMember(node(Adj, AA, InDeg), node(Adj, AA, InDeg1), G0, G1), InDeg1 is InDeg-1, %now expand the definition if it is not base (member(C, Base) -> TBox0 = TBox1 ; member(eq(C, E), TBox0), replaceMember(eq(Adj, AdjDef), eq(Adj, NewAdjDef), TBox0, TBox1), replaceInConcept(C, E, AdjDef, NewAdjDef) ), reduceInDegOfAdj(List, C, Base, G1, G, TBox1, TBox). replaceInConcept(C, E, not(R), not(S)) :- !, replaceInConcept(C, E, R, S). replaceInConcept(C, E, intersect(R0, R1), intersect(S0, S1)) :- !, replaceInConcept(C, E, R0, S0), replaceInConcept(C, E, R1, S1). replaceInConcept(C, E, union(R0, R1), union(S0, S1)) :- !, replaceInConcept(C, E, R0, S0), replaceInConcept(C, E, R1, S1). replaceInConcept(C, E, all(R, S0), all(R, S1)) :- !, replaceInConcept(C, E, S0, S1). replaceInConcept(C, E, some(R, S0), some(R, S1)) :- !, replaceInConcept(C, E, S0, S1). replaceInConcept(_C, _E, atmost(N, R), atmost(N, R)) :- !. replaceInConcept(_C, _E, atleast(N, R), atleast(N, R)) :- !. replaceInConcept(C, E, atmost(N, R, S0), atmost(N, R, S1)):- !, replaceInConcept(C, E, S0, S1). replaceInConcept(C, E, atleast(N, R, S0), atleast(N, R, S1)) :- !, replaceInConcept(C, E, S0, S1). replaceInConcept(C, E, R, S) :- !, (C = R -> S = E; S = R). expandConcept(intersect(C1, C2), TBox, Base, intersect(E1, E2)) :- !, expandConcept(C1, TBox, Base, E1), expandConcept(C2, TBox, Base, E2). expandConcept(union(C1, C2), TBox, Base, union(E1, E2)) :- !, expandConcept(C1, TBox, Base, E1), expandConcept(C2, TBox, Base, E2). expandConcept(all(R, C), TBox, Base, all(R, E)) :- !, expandConcept(C, TBox, Base, E). expandConcept(some(R, C), TBox, Base, some(R, E)) :- !, expandConcept(C, TBox, Base, E). expandConcept(atmost(N, R, C), TBox, Base, atmost(N, R, E)) :- !, expandConcept(C, TBox, Base, E). expandConcept(atleast(N, R, C), TBox, Base, atleast(N, R, E)) :- !, expandConcept(C, TBox, Base, E). expandConcept(C, _TBox, Base, E) :- member(C, Base), !, C = E. expandConcept(C, TBox, _Base, E) :- member(eq(C, E), TBox), !. %Otherwise it is a new concept, which we will just pass through expandConcept(C, _TBox, _Base, C). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% compileTBox(Axioms, tbox(T, Base)) :- unfold(Axioms, Base, T), !. subsumedBy(C1, C2, tbox(T, Base)) :- abolish(myCounter/1), expandConcept(C1, T, Base, C1e), expandConcept(C2, T, Base, C2e), unsat(intersect(C1e, not(C2e))). eqConcept(C1, C2, TBox) :- subsumedBy(C1, C2, TBox), subsumedBy(C2, C1, TBox). concept(C, tbox(T, Base)) :- member(eq(C, _), T); member(C, Base). %%%%%%%%%%%%%%%%% Pretty Print %%%%%%%%%%%%%%%%%%%%% /* $Id: pretty_print.pl,v 1.1 2000/04/27 13:59:18 jan Exp $ Part of SWI-Prolog SGML/XML parser Author: Jan Wielemaker E-mail: jan@swi.psy.uva.nl WWW: http://www.swi.psy.uva.nl/projects/SWI-Prolog/ Copying: LGPL-2. See the file COPYING or http://www.gnu.org Copyright (C) 1990-2000 SWI, University of Amsterdam. All rights reserved. */ % :- module(dia_pretty_print, % [ pretty_print/1 % ]). :- require([ atom_length/2 , between/3 , forall/2 , is_list/1 , member/2 , memberchk/2 ]). pretty_print(Term) :- numbervars(Term, 0, _), pp(Term, 0), write('.'), nl, fail. pretty_print(_). pp(Term, _Indent) :- atomic(Term), !, writeq(Term). pp(Var, _Indent) :- var(Var), !, write(Var). pp(Var, _Indent) :- Var = '$VAR'(_), !, print(Var). pp('$aref'(Name), _Indent) :- !, write(Name). pp(Module:Term, Indent) :- atomic(Module), !, writeq(Module), write(':'), pp(Term, Indent). :-op(300, xfy, (:=)). pp([A1 := V1|ArgList], Indent) :- % [] is done by `atomic'! is_list(ArgList), forall(member(A, ArgList), A = (_ := _)), !, longest_attribute([A1 := V1|ArgList], 0, L), NewIndent is Indent + 2, ( L > 9, Indent < 25, length(ArgList, Args), Args > 1 -> ArgIndent is Indent + 4, ValGoal = (nl, indent(ArgIndent)) ; ArgIndent is Indent + 6 + L, ValGoal = write(' ') ), write('[ '), pp(A1, Indent), term_length(A1, L1), tab(L-L1), write(' :='), ValGoal, pp(V1, ArgIndent), forall(member(A := V, ArgList), (write(','), nl, indent(NewIndent), pp(A, Indent), term_length(A, LA), tab(L-LA), write(' :='), ValGoal, pp(V, ArgIndent))), nl, indent(Indent), write(']'). pp([H|T], Indent) :- is_list(T), !, write('[ '), NewIndent is Indent + 2, pp(H, NewIndent), forall(member(E, T), (write(','), nl, indent(NewIndent), pp(E, NewIndent))), nl, indent(Indent), write(']'). pp(Term, Indent) :- functor(Term, Name, 2), current_op(_, Type, Name), memberchk(Type, [xfx, yfx]), !, arg(1, Term, A1), arg(2, Term, A2), pp(A1, Indent), format(' ~q ', [Name]), pp(A2, Indent). pp(Term, Indent) :- functor(Term, Name, _Arity), atom_length(Name, L), NewIndent is Indent + L + 1, format('~q(', Name), ( term_argument_length(Term, AL), NewIndent + AL < 72 -> Wrap = nowrap ; Wrap = wrap ), forall(generate_arg(I, Term, Arg), pparg(I, Arg, Wrap, NewIndent)), write(')'). generate_arg(ArgN, Term, Arg) :- functor(Term, _, Arity), between(1, Arity, ArgN), arg(ArgN, Term, Arg). pparg(1, Term, _, Indent) :- !, pp(Term, Indent). pparg(_, Term, wrap, Indent) :- !, write(','), nl, indent(Indent), pp(Term, Indent). pparg(_, Term, _, Indent) :- write(', '), pp(Term, Indent). longest_attribute([], L, L). longest_attribute([A := _|T], L0, L) :- term_length(A, AL), max(L0, AL, L1), longest_attribute(T, L1, L). term_length(A, AL) :- atomic(A), !, atom_length(A, AL). term_length(Var, AL) :- var(Var), !, AL = 1. term_length('$VAR'(N), AL) :- varname(N, L), length(L, AL). term_length('$aref'(N), AL) :- atom_length(N, AL). term_argument_length(Term, L) :- term_argument_length(Term, 1, 0, L). term_argument_length(Term, A, L0, L) :- arg(A, Term, Arg), !, term_length(Arg, AL), L1 is AL + L0, NA is A + 1, term_argument_length(Term, NA, L1, L). term_argument_length(_, _, L, L). max(A, B, M) :- ( A >= B -> M = A ; M = B ). varname(N, [C]) :- N < 26, !, C is N + 0'A. varname(N, [C1, C2]) :- C1 is N // 26 + 0'A, C2 is N mod 26 + 0'A. indent(I) :- Tabs is I // 8, forall(between(1, Tabs, _), put(9)), Spaces is I mod 8, tab(Spaces). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%