1/*  
    2% ===================================================================
    3% File 'mpred_type_constraints.pl'
    4% Purpose: For Emulation of OpenCyc for SWI-Prolog
    5% Maintainer: Douglas Miles
    6% Contact: $Author: dmiles $@users.sourceforge.net ;
    7% Version: 'interface' 1.0.0
    8% Revision:  $Revision: 1.9 $
    9% Revised At:   $Date: 2002/06/27 14:13:20 $
   10% ===================================================================
   11% File used as storage place for all predicates which change as
   12% the world is run.
   13%
   14%
   15% Dec 13, 2035
   16% Douglas Miles
   17*/
   18
   19
   20%:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).
   21:- module(mpred_motel,[ getLibraries/0]).   22%:- endif.
   23:- style_check(-singleton).   24
   25assert_logged(A):-assert(A).
   26asserta_logged(A):-asserta(A).
   27assertz_logged(A):-assertz(A).
   28:- op(700,fy,skipped).   29skipped(G):- nop(G).
   30/*
   31:- discontiguous testAllMotelExamples/1. 
   32:- discontiguous testMotel/1. 
   33:- discontiguous tryGoal/1.
   34*/
   35:- system:op(1199,fx,('==>')).   36:- system:op(1190,xfx,('::::')).   37:- system:op(1180,xfx,('==>')).   38:- system:op(1170,xfx,('<==>')).   39:- system:op(1160,xfx,('<-')).   40
   41:- system:op(1150,xfx,('=>')).   42:- system:op(1140,xfx,('<=')).   43:- system:op(1130,xfx,('<=>')).   44:-  system:((
   45 op(1199,fx,('==>')), 
   46 op(1190,xfx,('::::')),
   47 op(1180,xfx,('==>')),
   48 op(1170,xfx,'<==>'),  
   49 op(1160,xfx,('<-')),
   50 op(1150,xfx,'=>'),
   51 op(1140,xfx,'<='),
   52 op(1130,xfx,'<=>'), 
   53 op(600,yfx,'&'), 
   54 op(600,yfx,'v'),
   55 op(350,xfx,'xor'),
   56 op(300,fx,'~'),
   57 op(300,fx,'-'))).   58
   59
   60:- meta_predicate prolog_statistics_time(0).   61:- meta_predicate setupTest(*,0).   62
   63:-  system:op(200,yfx,('`')).   64:-  system:op(600,yfx,('&')).   65:-  system:op(600,yfx,('v')).   66:-  system:op(350,xfx,('xor')).   67:-  system:op(300,fx,('~')).   68:-  system:op(300,fx,('-')).   69:- user:use_module(library(logicmoo_common)).   70:- user:use_module(library(logicmoo_utils)).   71
   72/*	
   73
   74
   75                         INSTALLING MOTEL
   76			================
   77
   78The MOTEL distribution contains one compressed tar file, which
   79includes the MOTEL system. To install the sytem execute the following 
   80steps:
   81
   821. Uncompress the compressed tar file
   83
   84prompt(1)% uncompress motel.tar.Z
   85
   862. Extract the source file and documentation file from the tar file
   87
   88prompt(2)% tar xvf motel.tar
   89
   90This results in the files 	
   91README      ---	brief description how the system can be used
   92int.c       --- Part of the interface between Lucid Common Lisp and Sicstus Prolog
   93int.o       --- Part of the interface between Lucid Common Lisp and Sicstus Prolog
   94int.pl	    --- Prolog code of the interface between Lucid Common Lisp and Sicstus Prolog
   95motel.lisp  ---	Lisp   code of the interface between Lucid Common Lisp and Sicstus Prolog
   96motel.pl    ---	MOTEL source code	
   97motel.dvi   --- MOTEL user manual 
   98nh.dvi      --- Introduction to modal terminological logics
   99
  100After starting your PROLOG system you have to consult the source file.
  101
  102prompt(3)% sicstus
  103SICStus 2.1 #5: Tue Jul 21 16:16:49 MET DST 1992
  104| ?- consult(motel).
  105consulting motel.pl...
  106motel.pl consulted, 5600 msec 329168 bytes
  107
  108yes
  109| ?-
  110
  111Now you can work with the MOTEL system as described in the user manual.
  112
  113To use the interface between Lucid Common Lisp and SICStus Prolog, you 
  114have to modify the file motel.lisp. At the beginning it contains two
  115setq-commands:
  116
  117(setq *consult-motel-string* "['/usr/local/motel/motel.pl'].")
  118(setq *prolog-executable* "/usr/local/sicstus2.1/sicstus")
  119(setq *int_dot_pl* "/HG/hiwis/timm/lucid/int.pl")
  120
  121You should replace `/usr/local/motel/motel.pl` with the filename
  122of your installation of the motel.pl file. Furthermore you should
  123replace `/usr/local/sicstus2.1/sicstus` with the filename of you
  124PROLOG system. The variable `*int_dot_pl*` contains the location 
  125of the file `int.pl` included in the distribution
  126
  127Now you can load this file after you have started Lucid Common Lisp:
  128
  129prompt(4)% lucid
  130;;; Lucid Common Lisp/SPARC
  131;;; Application Environment Version 4.0.0, 6 July 1990
  132;;; Copyright (C) 1985, 1986, 1987, 1988, 1989, 1990, 1991 by Lucid, Inc.
  133;;; All Rights Reserved
  134;;;
  135;;; This software product contains confidential and trade secret information
  136;;; belonging to Lucid, Inc.  It may not be copied for any reason other than
  137;;; for archival and backup purposes.
  138;;;
  139;;; Lucid and Lucid Common Lisp are trademarks of Lucid, Inc.  Other brand
  140;;; or product names are trademarks or registered trademarks of their
  141;;; respective holders.
  142
  143> (load "motel.lisp")
  144;;; Loading source file "motel.lisp"
  145;;; Warning: File "motel.lisp" does not begin with IN-PACKAGE.
  146    Loading into package "USER"
  147#P"/usr/local/motel/src/motel/motel.lisp"
  148> 
  149
  150Then you are able to work with the interface between Lucid Lisp and
  151SICSTUS Prolog as described the appendix of the MOTEL user manual.
  152
  153*/
  154/**********************************************************************
  155 *
  156 * @(#) dynamicDef.pl 1.16@(#)
  157 *
  158 */
  159
  160:- multifile(call_u_lm/1).  161:- dynamic(call_u_lm/1).  162
  163% !! Remember: Any changes to the following list should be carefully
  164%              reflected in     clearEnvironment
  165%                       and     saveEnvironment.
  166
  167% The following predicates belong to the translated terminologial 
  168% axioms.
  169:- multifile(in/9).  170:- dynamic(in/9).  171:- multifile(kb_in/10).  172:- dynamic(kb_in/10).  173:- multifile(eq/9).  174:- dynamic(eq/9).  175:- multifile(constraint/8).  176:- dynamic(constraint/8).  177:- multifile(rel/5).  178:- dynamic(rel/5).  179% The following predicates are used for additional informations about
  180% the terminology and the world description.
  181:- multifile((attribute)/5).  182:- dynamic((attribute)/5).  183
  184:- multifile(axiom/3).  185:- dynamic(axiom/3).  186:- multifile(closed/5).  187:- dynamic(closed/5).  188:- multifile(compiledPredicate/2).  189:- dynamic(compiledPredicate/2).  190:- multifile(conceptElement/7).  191:- dynamic(conceptElement/7).  192:- multifile(conceptEqualSets/6).  193:- dynamic(conceptEqualSets/6).  194:- multifile(conceptHierarchy/3).  195:- dynamic(conceptHierarchy/3).  196:- multifile(conceptName/4).  197:- dynamic(conceptName/4).  198
  199
  200:- multifile(conceptName1/4).  201:- dynamic(conceptName1/4).  202
  203
  204:- multifile(conceptSubsets/6).  205:- dynamic(conceptSubsets/6).  206:- multifile(environment/3).  207:- dynamic(environment/3).  208:- multifile(given_change/4).  209:- dynamic(given_change/4).  210:- multifile(given_inflLink/4).  211:- dynamic(given_inflLink/4).  212:- multifile(modalAxioms/6).  213:- dynamic(modalAxioms/6).  214:- multifile(roleAttributes/5).  215:- dynamic(roleAttributes/5).  216:- multifile(roleDefault/4).  217:- dynamic(roleDefault/4).  218:- multifile(roleDefNr/4).  219:- dynamic(roleDefNr/4).  220:- multifile(roleDomain/4).  221:- dynamic(roleDomain/4).  222:- multifile(roleElement/8).  223:- dynamic(roleElement/8).  224:- multifile(roleEqualSets/6).  225:- dynamic(roleEqualSets/6).  226:- multifile(roleHierarchy/3).  227:- dynamic(roleHierarchy/3).  228:- multifile(roleName/4).  229:- dynamic(roleName/4).  230:- multifile(roleName1/4).  231:- dynamic(roleName1/4).  232:- multifile(roleNr/5).  233:- dynamic(roleNr/5).  234:- multifile(roleRange/4).  235:- dynamic(roleRange/4).  236:- multifile(roleSubsets/6).  237:- dynamic(roleSubsets/6).  238
  239:- multifile(sub/5).  240:- dynamic(sub/5).  241:- multifile(succ/5).  242:- dynamic(succ/5).  243:- multifile(nsub/5).  244:- dynamic(nsub/5).  245
  246% The following predicates are used during computations only.
  247:- multifile(abductiveDerivation/3).  248:- dynamic(abductiveDerivation/3).  249:- multifile(consistencyDerivation/3).  250:- dynamic(consistencyDerivation/3).  251:- multifile(hypothesis/1).  252:- dynamic(hypothesis/1).  253:- multifile(inconsistencyCheck/3).  254:- dynamic(inconsistencyCheck/3).  255:- multifile(motel_option/2).  256:- dynamic(motel_option/2).  257:- multifile(nsub3/2).  258:- dynamic(nsub3/2).  259:- multifile(sub3/2).  260:- dynamic(sub3/2).  261:- multifile(succ3/2).  262:- dynamic(succ3/2).  263%:- multifile(value/2).
  264%:- dynamic(value/2).
  265% Predicates which are no longer needed
  266%:- multifile(falsum/2).
  267%:- dynamic(falsum/2).
  268%:- multifile(numb/1).
  269%:- dynamic(numb/1).
  270:- op(1200,xfx,<==).  271
  272 :- meta_predicate doFileGoal(0).  273 :- meta_predicate performQuery(*,0,0).  274 :- meta_predicate setofOrNil(?,^,-).  275 :- meta_predicate bagofOrNil(?,^,-).  276 :- meta_predicate tryGoal(0).  277 :- meta_predicate doClashTest(0).  278 :- meta_predicate runTest(*,0).  279 :- meta_predicate mapGoal(0,*,*).  280 :- meta_predicate doboth(0,0).  281 :- meta_predicate assert2(0).  282 :- meta_predicate callList(0).  283 :- meta_predicate assert1(0).  284 :- meta_predicate try(0).  285 :- meta_predicate unexpand_role(*,*,0,*).  286
  287
  288:- multifile( clause/1).  289:- multifile( conceptElement/6).  290:- multifile( conceptEqualSets/5).  291:- multifile( conceptSubsets/5).  292:- multifile( constructEqHead/20).  293:- multifile( constructMLHead/20).  294:- multifile( cont1a/5).  295:- multifile( convertInConsequence/10).  296:- multifile( default_change/3).  297:- multifile( eq/19).  298:- multifile( noDouble/2).  299:- multifile( prolog_flag/3).  300:- multifile( roleAll/9).  301:- multifile( roleEqualSets/5).  302:- multifile( roleName1/4).  303:- multifile( roleSubsets/5).  304:- multifile( roleTripel/6).  305
  306:- dynamic( clause/1).  307:- dynamic( conceptElement/6).  308:- dynamic( conceptSubsets/5).  309
  310:- dynamic( conceptEqualSets/5).  311:- dynamic( conceptSubsets/4).  312
  313
  314:- dynamic( constructEqHead/20).  315:- dynamic( constructMLHead/20).  316:- dynamic( cont1a/5).  317:- dynamic( convertInConsequence/10).  318:- dynamic( default_change/3).  319:- dynamic( eq/19).  320:- dynamic( noDouble/2).  321
  322:- dynamic( roleAll/9).  323:- dynamic( roleEqualSets/5).  324:- dynamic( roleName1/4).  325:- dynamic( roleSubsets/5).  326:- dynamic( roleTripel/6).  327
  328/**********************************************************************
  329 *
  330 * @(#) sets.pl 1.1@(#)
  331 *
  332 */
  333
  334%   member(?Element, ?Set)
  335%   is true when Set is a list, and Element occurs in it.  It may be used
  336%   to test for an element or to enumerate all the elements by backtracking.
  337%   Indeed, it may be used to generate the Set!
  338/*
  339member(X, [X|_]    ).
  340member(X, [_,X|_]  ).
  341member(X, [_,_,X|_]).
  342member(X, [_,_,_|L]) :-
  343        member(X, L).
  344*/
  345%   reverseList(+List1,-List2
  346%   reverses the list List1 to get List2
  347
  348reverseList([],[]) :- !.
  349reverseList([H|T],L2) :-
  350	reverseList(T,L1),
  351	append(L1,[H],L2),
  352	!.
  353
  354%   memberchk(+Element, +Set)
  355%   means the same thing, but may only be used to test whether a known
  356%   Element occurs in a known Set.  In return for this limited use, it
  357%   is more efficient than member/2 when it is applicable.
  358/*
  359memberchk(X, L) :- 
  360	nonvar(X), 
  361	nonvar(L),
  362	memberchk1(X,L).
  363
  364memberchk1(X, [X|_]    ) :- !.
  365memberchk1(X, [_,X|_]  ) :- !.
  366memberchk1(X, [_,_,X|_]) :- !.
  367memberchk1(X, [_,_,_|L]) :-
  368	memberchk1(X, L).
  369*/
  370%   nonmember(+Element, +Set)
  371%   means that Element does not occur in Set.  It does not make sense
  372%   to instantiate Element in any way, as there are infinitely many
  373%   terms which do not occur in any given set.  Nor can we generate
  374%   Set; there are infinitely many sets not containing a given Element.
  375%   Read it as "the given Element does not occur in the given list Set".
  376%   This code was suggested by Bruce Hakami; seven versions of this
  377%   operation were benchmarked and this found to be the fastest.
  378%   The old code was for DEC-10 Prolog, which did not compile (\+)/1.
  379
  380nonmember(Element, Set) :-
  381	nonvar(Element),
  382	nonvar(Set),
  383	\+ (member(Element, Set)).
  384
  385%   intersection_motel(+Set1, +Set2, ?Intersection)
  386%   is true when all three arguments are lists representing sets,
  387%   and Intersection contains every element of Set1 which is also
  388%   an element of Set2, the order of elements in Intersection
  389%   being the same as in Set1.  That is, Intersection represents
  390%   the intersection_motel of the sets represented by Set1 and Set2.
  391%   If Set2 is a partial list, Intersection will be empty, which
  392%   is not, of course, correct.  If Set1 is a partial list, this
  393%   predicate will run away on backtracking.  Set1 and Set2 should
  394%   both be proper lists, but this is not checked.  Duplicates in
  395%   Set1 may survive in Intersection.  It is worthy of note that
  396%   if Set1 is an ordset, Intersection is an ordset, despite Set2.
  397
  398intersection_motel([], _, []).
  399intersection_motel([Element|Elements], Set, Intersection) :-
  400	memberchk(Element, Set),
  401	!,
  402	Intersection = [Element|Rest],
  403	intersection_motel(Elements, Set, Rest).
  404intersection_motel([_|Elements], Set, Intersection) :-
  405	intersection_motel(Elements, Set, Intersection).
  406
  407
  408
  409%   intersection_motel(+ListOfSets, ?Intersection)
  410%   is true when Intersection is the intersection_motel of all the sets in
  411%   ListOfSets.  The order of elements in Intersection is taken from
  412%   the first set in ListOfSets.  This has been turned inside out to
  413%   minimise the storage turnover.
  414
  415intersection_motel([Set|Sets], Intersection) :-
  416	intersection1(Set, Sets, Intersection).
  417
  418intersection1([], _, []).
  419intersection1([Element|Elements], Sets, Intersection) :-
  420	memberchk_all(Sets, Element),
  421	!,
  422	Intersection = [Element|Rest],
  423	intersection1(Elements, Sets, Rest).
  424intersection1([_|Elements], Sets, Intersection) :-
  425	intersection1(Elements, Sets, Intersection).
  426
  427memberchk_all([], _).
  428memberchk_all([Set|Sets], Element) :-
  429	memberchk(Element, Set),
  430	memberchk_all(Sets, Element).
  431
  432%   motel_subtract(+Set1, +Set2, ?Difference)
  433%   is like intersect, but this time it is the elements of Set1 which
  434%   *are* in Set2 that are deleted.  Note that duplicated Elements of
  435%   Set1 which are not in Set2 are retained in Difference.
  436
  437motel_subtract([], _, []).
  438motel_subtract([Element|Elements], Set, Difference) :-
  439	memberchk(Element, Set),
  440	!,
  441	motel_subtract(Elements, Set, Difference).
  442motel_subtract([Element|Elements], Set, [Element|Difference]) :-
  443	motel_subtract(Elements, Set, Difference).
  444
  445%   motel_union(+Set1, +Set2, ?Union)
  446%   is true when motel_subtract(Set1,Set2,Diff) and append(Diff,Set2,Union),
  447%   that is, when Union is the elements of Set1 that do not occur in
  448%   Set2, followed by all the elements of Set2.
  449
  450motel_union([], Union, Union).
  451motel_union([Element|Elements], Set, Union) :-
  452	memberchk(Element, Set),
  453	!,
  454	motel_union(Elements, Set, Union).
  455motel_union([Element|Elements], Set, [Element|Union]) :-
  456	motel_union(Elements, Set, Union).
  457
  458%   motel_union(+ListOfSets, ?Union)
  459%   is true when Union is the motel_union of all sets in ListOfSets.
  460
  461motel_union([],[]).
  462motel_union([Set1],Set1).
  463motel_union([Set1,Set2|Sets],Union) :-
  464	motel_union(Set1,Set2,Set),
  465	motel_union([Set|Sets],Union).
  466
  467
  468%   list_to_set(+List, ?Set)
  469%   is true when List and Set are lists, and Set has the same elements
  470%   as List in the same order, except that it contains no duplicates.
  471%   The two are thus equal considered as sets.  If you really want to
  472%   convert a list to a set, list_to_ord_set is faster, but this way
  473%   preserves as much of the original ordering as possible.
  474%   If List contains several copies of an element X, only the LAST
  475%   copy of X is retained.  If you want to convert a List to a Set,
  476%   retaining the FIRST copy of repeated elements, call
  477%	symdiff([], List, Set)
  478/*
  479list_to_set([], []).
  480list_to_set([Head|Tail], Set) :-
  481	memberchk(Head, Tail),
  482	!,
  483	list_to_set(Tail, Set).
  484list_to_set([Head|Tail], [Head|Set]) :-
  485	list_to_set(Tail, Set).
  486*/
  487
  488%   deleteInList(+List, +Kill, ?Residue)
  489%   is true when List is a list, in which Kill may or may not occur, and
  490%   Residue is a copy of List with all elements equal to Kill deleted.
  491%   To extract a single copy of Kill, use select(Kill, List, Residue).
  492%   If List is not proper, deleteInList/3 will FAIL.  Kill and the elements of
  493%   List should be sufficiently instantiated for \= to be sound.
  494
  495deleteInList(-, _, _) :- !, fail.		% reject partial lists
  496deleteInList([], _, []).
  497deleteInList([Kill|Tail], Kill, Residue) :- !,
  498	deleteInList(Tail, Kill, Residue).
  499deleteInList([Head|Tail], Kill, [Head|Residue]) :-
  500    %	Head \= Kill,
  501	deleteInList(Tail, Kill, Residue).
  502
  503
  504
  505motel_subset([],_S2) :- !.
  506motel_subset([E1|S1],S2) :-
  507	\+(\+(member(E1,S2))),
  508	motel_subset(S1,S2),
  509	!.
  510
  511equalset(S1,S2) :-
  512	motel_subset(S1,S2),
  513	motel_subset(S2,S1),
  514	!.
  515
  516
  517%----------------------------------------------------------------------	
  518%   Module : lists
  519%   Authors: Bob Welham, Lawrence Byrd, and Richard A. O'Keefe
  520%   Updated: 10/25/90
  521%   Defines: list processing utilities
  522%   SeeAlso: library(motel_flatten)
  523
  524%   Adapted from shared code written by the same authors; all changes
  525%   Copyright (C) 1987, Quintus Computer Systems, Inc.  All rights reserved.
  526
  527%   perm(+List, ?Perm)
  528%   is true when List and Perm are permutations of each other.  The main
  529%   use of perm/2 is to generate permutations.  You should not use this
  530%   predicate in new programs; use permutation_motel/2 instead.  List must be
  531%   a proper list.  Perm may be partly instantiated.
  532
  533perm([], []).
  534perm([X|Xs], Ys1) :-
  535	perm(Xs, Ys),
  536	motel_insert(Ys, X, Ys1).
  537
  538
  539motel_insert(L, X, [X|L]).
  540motel_insert([H|T], X, [H|L]) :-
  541	motel_insert(T, X, L).
  542
  543%   permutation_motel(?List, ?Perm)
  544%   is true when List and Perm are permuations of each other.
  545%   Unlike perm/2, it will work even when List is not a proper list.
  546%   It even acts in a marginally sensible way when Perm isn't proper
  547%   either, but it will still backtrack forever.
  548%   Be careful: this is quite efficient, but the number of permutations of an
  549%   N-element list is N!, and even for a 7-element list that is 5040.
  550
  551permutation_motel(List, Perm) :-
  552	permutation_motel(List, Perm, Perm).
  553
  554permutation_motel([], [], []).
  555permutation_motel([X|Xs], Ys1, [_|Zs]) :-
  556	permutation_motel(Xs, Ys, Zs),
  557	motel_insert(Ys, X, Ys1).
  558
  559
  560
  561/**********************************************************************
  562 *
  563 * @(#) lib.pl 1.7@(#)
  564 *
  565 */
  566
  567/* POPLOG PROLOG LIBRARIES
  568 */
  569
  570/* Library gensym
  571 * import:  gensym(_,_)
  572 */
  573
  574/* QUINTUS PROLOG LIBRARIES
  575 */
  576
  577/* Library strings
  578 * import:  gensym(_,_)
  579 */
  580
  581
  582/**********************************************************************
  583 *
  584 * COUNTER
  585 *
  586 */
  587
  588/**********************************************************************
  589 *
  590 * setCounter(+Counter,+Value)
  591 * creates a new counter Counter with value Value.
  592 *
  593 */
  594
  595setCounter(Counter,N) :- flag(Counter,_,N).
  596
  597/**********************************************************************
  598 *
  599 * addCounter(+Counter,+Value)
  600 * adds Value to the current value of counter Counter.
  601 *
  602 */
  603 
  604addCounter(Counter,N) :-  flag(Counter,M,M+N).
  605
  606/**********************************************************************
  607 *
  608 * getCounter(+Counter,-Value)
  609 * retrieves the current value Value of counter Counter.
  610 *
  611 */
  612
  613getCounter(Counter,N) :- flag(Counter,N,N).
  614      
  615
  616/**********************************************************************
  617 *
  618 * writes(+List)
  619 * put each character in List.
  620 *
  621 */
  622
  623writes([]) :- !.
  624writes([H|T]) :- put(H), writes(T).
  625
  626/***********************************************************************
  627 *
  628 * printTime(+G)
  629 * execute goal G and report the runtime the execution needed.
  630 * Only available for SICStus Prolog and Quintus Prolog.
  631 *
  632 */
  633
  634:- meta_predicate printTime(0).  635:- meta_predicate printTime(0,*).  636
  637printTime(G) :-
  638	(currentProlog(poplog) ; currentProlog(macprolog)),
  639	!,
  640	call(G),
  641	!.
  642printTime(G) :-
  643	!,
  644	getRuntime(T0),
  645	printTime(G,T0).
  646
  647printTime(G,T0) :-
  648	call(G),
  649	getRuntime(T1),
  650	T is T1 - T0,
  651	format('Total runtime ~3d sec.~n', [T]).
  652printTime(_,T0) :-
  653	getRuntime(T1),
  654	T is T1 - T0,
  655	format('Total runtime ~3d sec.~n', [T]),
  656	!,
  657	fail.
  658
  659/**********************************************************************
  660 *
  661 * simple_term(X) 
  662 * it contrast to the usage in the Quintus Prolog user manual we
  663 * call a term `simple` if it is either an atom or a variable.
  664 * This predicate succeeds iff X is a simple term in this sense.
  665 *
  666 */
  667
  668simple_term(X) :-
  669	var(X),
  670	!.
  671simple_term(X) :-
  672	atomic(X),
  673	!.
  674
  675/**********************************************************************
  676 *
  677 * LIBRARY HANDLING
  678 *
  679 */
  680
  681loadLibraries(sicstus) :-
  682	assertz_logged((gensym(Prefix, V) :-
  683	var(V),
  684	atomic(Prefix),
  685	(   retract(gensym_counter(Prefix, M))
  686	;   M = 0
  687	),
  688	N is M+1,
  689	asserta_logged(gensym_counter(Prefix, N)),
  690	name(Prefix,P1),
  691	name(N,N1),
  692	append(P1,N1,V1),
  693	name(V,V1),
  694	!)),
  695	assertz_logged((getTwoRandomNumbers(RT,CT) :-
  696	statistics(runtime,[RT,CT]))),
  697	assertz_logged((getRuntime(RT) :-
  698	statistics(runtime,[RT|_]))),
  699	assertz_logged((append([],L2,L2))),
  700	assertz_logged((append([A1|L1],L2,[A1|L3]) :-
  701	append(L1,L2,L3))),
  702	assertz_logged((not(Goal) :- call(\+ Goal))),
  703	assertz_logged((once(Goal) :- Goal, !)),
  704	assertz_logged((ask(A1) :- deduce(A1))),
  705	assertz_logged((ask(A1,A2) :- deduce(A1,A2))),
  706	assertz_logged((ask(A1,A2,A3) :- deduce(A1,A2,A3))),
  707	assertz_logged((ask(A1,A2,A3,A4) :- deduce(A1,A2,A3,A4))),
  708	assertz_logged((map(A1,A2,A3) :- hop_map(A1,A2,A3))),
  709	assertz_logged((map(A1,A2,A3,A4) :- hop_map(A1,A2,A3,A4))),
  710	!.
  711loadLibraries(eclipse) :-
  712	assertz_logged((gensym(Prefix, V) :-
  713	var(V),
  714	atomic(Prefix),
  715	(   retract(gensym_counter(Prefix, M))
  716	;   M = 0
  717	),
  718	N is M+1,
  719	asserta_logged(gensym_counter(Prefix, N)),
  720	name(Prefix,P1),
  721	name(N,N1),
  722	append(P1,N1,V1),
  723	name(V,V1),
  724	!)),
  725	assertz_logged((getTwoRandomNumbers(RT,CT) :-
  726	statistics(runtime,[RT,CT]))),
  727	assertz_logged((getRuntime(RT) :-
  728	statistics(runtime,[RT|_]))),
  729	assertz_logged((append([],L2,L2))),
  730	assertz_logged((append([A1|L1],L2,[A1|L3]) :-
  731	append(L1,L2,L3))),
  732	assertz_logged((ask(A1) :- deduce(A1))),
  733	assertz_logged((ask(A1,A2) :- deduce(A1,A2))),
  734	assertz_logged((ask(A1,A2,A3) :- deduce(A1,A2,A3))),
  735	assertz_logged((ask(A1,A2,A3,A4) :- deduce(A1,A2,A3,A4))),
  736	assertz_logged((map(A1,A2,A3) :- hop_map(A1,A2,A3))),
  737	assertz_logged((map(A1,A2,A3,A4) :- hop_map(A1,A2,A3,A4))),
  738	!.
  739loadLibraries(swiprolog) :-
  740	assertz_logged((ask(A1) :- deduce(A1))),
  741	assertz_logged((ask(A1,A2) :- deduce(A1,A2))),
  742	assertz_logged((ask(A1,A2,A3) :- deduce(A1,A2,A3))),
  743	assertz_logged((ask(A1,A2,A3,A4) :- deduce(A1,A2,A3,A4))),
  744	assertz_logged((map(A1,A2,A3) :- hop_map(A1,A2,A3))),
  745	assertz_logged((map(A1,A2,A3,A4) :- hop_map(A1,A2,A3,A4))),
  746	assertz_logged((portray(not(F)) :- display(not(F)))),
  747	assertz_logged((getTwoRandomNumbers(RT,CT) :-
  748	statistics(cputime,RT1), RT is (ceil(RT1 * 100000)) mod 100000, statistics(atoms,CT))),
  749	assertz_logged((getRuntime(RT) :-
  750	statistics(cputime,RT1), RT is ceil(RT1 * 1000))),
  751	%index(kb_in(1,0,0,0,1,1,0,0,0,0)),
  752	%index(eq(1,0,0,1,1,0,0,0,0)),
  753	%index(constraint(1,0,0,1,0,0,0,0)),
  754	assertz_logged((retractall_head(Head) :- retract(Head), fail)),
  755	assertz_logged((retractall_head(Head) :- retract((Head :- _Body)), fail)),
  756	assertz_logged((retractall_head(_))),
  757	!.
  758loadLibraries(poplog) :-
  759	op(600,xfy,':'),
  760	assertz_logged((gensym(Prefix, V) :-
  761	var(V),
  762	atomic(Prefix),
  763	(   retract(gensym_counter(Prefix, M))
  764	;   M = 0
  765	),
  766	N is M+1,
  767	asserta_logged(gensym_counter(Prefix, N)),
  768	name(Prefix,P1),
  769	name(N,N1),
  770	append(P1,N1,V1),
  771	name(V,V1),
  772	!)),
  773	assertz_logged((append([],L2,L2))),
  774	assertz_logged((append([A1|L1],L2,[A1|L3]) :-
  775	append(L1,L2,L3))),
  776	assertz_logged((ask(A1) :- deduce(A1))),
  777	assertz_logged((ask(A1,A2) :- deduce(A1,A2))),
  778	assertz_logged((ask(A1,A2,A3) :- deduce(A1,A2,A3))),
  779	assertz_logged((ask(A1,A2,A3,A4) :- deduce(A1,A2,A3,A4))),
  780	assertz_logged((map(A1,A2,A3) :- hop_map(A1,A2,A3))),
  781	assertz_logged((map(A1,A2,A3,A4) :- hop_map(A1,A2,A3,A4))),
  782	assertz_logged((once(Goal) :- Goal, !)),
  783	assertz_logged((saveMOTEL(F) :- save_program(F))),
  784	!.
  785loadLibraries(quintus) :-
  786	assertz_logged((gensym(Prefix, V) :-
  787	var(V),
  788	atomic(Prefix),
  789	(   retract(gensym_counter(Prefix, M))
  790	;   M = 0
  791	),
  792	N is M+1,
  793	asserta_logged(gensym_counter(Prefix, N)),
  794	name(Prefix,P1),
  795	name(N,N1),
  796	append(P1,N1,V1),
  797	name(V,V1),
  798	!)),
  799	assertz_logged((getTwoRandomNumbers(RT,CT) :-
  800	statistics(runtime,[RT,CT]))),
  801	assertz_logged((getRuntime(RT) :-
  802	statistics(runtime,[RT|_]))),
  803	assertz_logged((not(Goal) :- call(\+ Goal))),
  804	assertz_logged((once(Goal) :- Goal, !)),
  805	assertz_logged((ask(A1) :- deduce(A1))),
  806	assertz_logged((ask(A1,A2,A3,A4) :- deduce(A1,A2,A3,A4))),
  807	assertz_logged((ask(A1,A2) :- deduce(A1,A2))),
  808	assertz_logged((ask(A1,A2,A3) :- deduce(A1,A2,A3))),
  809	assertz_logged((map(A1,A2,A3) :- hop_map(A1,A2,A3))),
  810	assertz_logged((map(A1,A2,A3,A4) :- hop_map(A1,A2,A3,A4))),
  811	assertz_logged((saveMOTEL(F) :- save_program(F))),
  812	!.
  813loadLibraries(macprolog) :-
  814	op(600,xfy,':'),
  815	!.
  816
  817testForMacprolog(others) :-
  818	current_op(_X,_Y,':'),
  819	!,
  820	fail.
  821testForMacprolog(macprolog) :-
  822	unknown(_X,fail),
  823	!.
  824
  825getLibraries :-
  826	testForMacprolog(_),
  827	!,
  828	asserta_logged(currentProlog(macprolog)),
  829	version('MOTEL-0.4 Tue Aug 04 15:00:00 MET 1992'),
  830	loadLibraries(macprolog).
  831:- if(false).  832getLibraries :-
  833	current_op(1190,fx,delay),
  834	!,
  835	sicstus,
  836	asserta_logged(currentProlog(eclipse)),
  837	set_flag(variable_names,off),
  838	loadLibraries(eclipse).
  839:- endif.  840getLibraries :-
  841	current_op(_X,_Y,?),
  842	style_check(-singleton),
  843	!,
  844	asserta_logged(currentProlog(swiprolog)),
  845	style_check(-discontiguous),
  846	loadLibraries(swiprolog).
  847getLibraries :-
  848	setof((X,Y),prolog_flag(X,Y),L),
  849	member((single_var,_Z),L),
  850	!,
  851	asserta_logged(currentProlog(quintus)),
  852	version('MOTEL-0.4 Tue Aug 04 15:00:00 MET 1992'),
  853	prolog_flag(single_var,_,off),
  854	loadLibraries(quintus).
  855getLibraries :-
  856	prolog_flag(_X,_Y),
  857	!,
  858	asserta_logged(currentProlog(sicstus)),
  859	version('MOTEL-0.4 Tue Aug 04 15:00:00 MET 1992'),
  860	prolog_flag(single_var_warnings,_,off),
  861	prolog_flag(compiling,_,fastcode),
  862	prolog_flag(unknown,_,fail),
  863%	asserta_logged(foreign_file('int.o',[int_init])),
  864%	asserta_logged(foreign(int_init,int_init)),
  865%	load_foreign_files(['int.o'],[]),
  866%	int_init,
  867	loadLibraries(sicstus).
  868getLibraries :-
  869	tell('/tmp/v1'), version, told,
  870	!,
  871	asserta_logged(currentProlog(poplog)),
  872	version('MOTEL-0.4 Tue Aug 04 15:00:00 MET 1992'),
  873	loadLibraries(poplog).
  874
  875/**********************************************************************
  876 *
  877 * OPTIONS
  878 *
  879 */
  880
  881/***********************************************************************
  882 *
  883 * setOption(+Option,+Set)
  884 * set motel_option Option to value Set.
  885 *
  886 */
  887
  888setOption(Option,Set) :-
  889	retractall_head(motel_option(Option,_)),
  890	asserta_logged(motel_option(Option,Set)),
  891	!.
  892
  893/**********************************************************************
  894 *
  895 * ifOption(+Option,+Set,+Goal)
  896 * executes Goal if the current value of Option is Set otherwise
  897 * the predicate suceeds.
  898 *
  899 */
  900
  901:- meta_predicate ifOption(*,*,0).  902ifOption(Option,Set,Goal) :-
  903	motel_option(Option,Set),
  904	call(Goal),
  905	!.
  906ifOption(_,_,_) :-
  907	!.
  908
  909retractallEnv(Env,Pred/Arity) :-
  910	constructHead(Env,Pred/Arity,Head),
  911	retractall_head(Head), 
  912	!.
  913
  914% :- ensure_loaded('/opt/PrologMUD/pack/logicmoo_base/prolog/logicmoo_utils').
  915
  916:- getLibraries.  917
  918
  919
  920
  921% Copyright (C) 1993 Patrick Brandmeier
  922%                    Ullrich Hustadt
  923%                    Renate  Schmidt
  924%                    Jan     Timm
  925
  926% This file is part of the MOTEL distribution.
  927
  928% MOTEL is free software; you can redistribute it and/or modify
  929% it under the terms of the GNU General Public License as published by
  930% the Free Software Foundation; either version 1, or (at your motel_option)
  931% any later version.
  932
  933% MOTEL is distributed in the hope that it will be useful,
  934% but WITHOUT ANY WARRANTY; without even the implied warranty of
  935% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  936% GNU General Public License for more details.
  937/**********************************************************************
  938 *
  939 * @(#) abduction.pl 1.2@(#)
  940 *
  941 */
  942
  943getAbductionHyps(L,[]) :-
  944	var(L),
  945	!.
  946getAbductionHyps([],[]) :-
  947	!.
  948getAbductionHyps([in(Env,RN,modal(MS),C,X,A1,A2,A3,A4)|L1],
  949	[in(Env,RN,modal(MS),C,X,A1,A2,A3,A4)|L2]) :-
  950	!,
  951	getAbductionHyps(L1,L2).
  952
  953doMinimalityCheck(GL1,[in(Env,RN,modal(MS),C,X,_A1,_A2,_A3,_A4)|GL2]) :-
  954	append(GL1,GL2,GL),
  955	HYPS = [or(GL),rl([]),fl(H3)],
  956	constructMLCall(Env,rn(_AX3,_RN3,_S3,_O3),bodyMC(MS),headMC(MS),
  957	                C,X,HYPS,[],CALLS,_PT35,Goal),
  958	not(Goal),
  959	doMinimalityCheck([in(Env,RN,modal(MS),C,X,_A1,_A2,_A3,_A4)|GL1],
  960	                   GL2),
  961	!.
  962doMinimalityCheck(_GL1,[]) :-
  963	!.
  964	
  965
  966doConsistencyCheck(GL1,[in(Env,RN,modal(MS),C,X,_A1,_A2,_A3,_A4)|GL2]) :-
  967	append(GL1,GL2,GL),
  968	HYPS = [or(GL),rl([]),fl(H3)],
  969	normalizeNot(not(C),C1),
  970	constructMLCall(Env,rn(_AX3,_RN3,_S3,_O3),bodyMC(MS),headMC(MS),
  971	                C1,X,HYPS,[],CALLS,_PT35,Goal),
  972	not(Goal),
  973	doConsistencyCheck([in(Env,RN,modal(MS),C,X,_A1,_A2,_A3,_A4)|GL1],
  974	                   GL2),
  975	!.
  976doConsistencyCheck(_GL1,[]) :-
  977	!.
  978	
  979
  980	
  981/**********************************************************************
  982 *
  983 * @(#) callStack.pl 1.4@(#)
  984 *
  985 */
  986
  987/**********************************************************************
  988 *
  989 * THE CALL STACK 
  990 * is a list of elements of the following form:
  991 * - true 
  992 * - in(rn(AX,RN,_,_),modal(MS),C,X,hyp(HYPS))
  993 * - eq(rn(AX,RN,_,_),modal(MS),X,Y,hyp(HYPS))
  994 * - constraint(rn(AX,RN,_,_),MS,(card,app(_F:R,X),Rel,N),hyp(HYPS))
  995 *
  996 */
  997
  998/***********************************************************************
  999 * 
 1000 * cCS(+CallStack,Call)
 1001 * succeeds if the 'top' call on CallStack is not already contained
 1002 * elsewhere in CallStack and Call is not already contained in CallStack.
 1003 * This predicate is used to prevent nontermination.
 1004 *
 1005 */
 1006
 1007cCS([],_) :- !.
 1008cCS(IL,A1) :-
 1009%	print('trying '), print(A1), nl,
 1010	noAxiom(A1,IL),
 1011%	IL = [I1|IL1],
 1012	noDouble(IL),
 1013%	printAxiom(A1), nl,
 1014%	print('------------------------------------------------------------'),
 1015%	nl,
 1016	not(clashCS([A1|IL])),
 1017	!.
 1018
 1019testEqualAbductiveHypotheses(D1,D2) :-
 1020	currentEnvironment(Env),
 1021	abductiveDerivation(Env,D1,HL1),
 1022	abductiveDerivation(Env,D2,HL2),
 1023	!,
 1024	equalset(HL1,HL2),
 1025	!.
 1026testEqualAbductiveHypotheses(_D1,_D2) :-
 1027	!.
 1028
 1029testEqualHypotheses(H1,H2) :-
 1030%	equalset(H1,H2),
 1031	!.
 1032
 1033% To prove in(C,X) it is not allowed to use another in-clause generated 
 1034% from the same axiom
 1035sameAxiom(AX,_RN1,MS1,in(C1,X1),HYPS1,D1,
 1036          in(rn(AX,_RN2,_,_),modal(MS2),C2,X2,hyp(HYPS2),ab(D2))) :- 
 1037	not(not(X1 = X2)),
 1038	not(not(C1 = C2)),
 1039	testEqualAbductiveHypotheses(D1,D2),
 1040	testEqualHypotheses(HYPS1,HYPS2),
 1041	equalWorlds(MS1,MS2), !.
 1042sameAxiom(AX,_RN1,MS1,in(_C,X1),HYPS1,_D1,
 1043          eq(rn(AX,_RN2,_,_),modal(MS2),X2,_,hyp(HYPS2))) :- 
 1044	nonvar(X1),
 1045	nonvar(X2),
 1046	not(not(X1 = X2)),
 1047	testEqualHypotheses(HYPS1,HYPS2),
 1048	equalWorlds(MS1,MS2), !.
 1049sameAxiom(AX,_RN1,MS1,in(_C,X1),HYPS1,_D1,
 1050          eq(rn(AX,_RN2,_,_),modal(MS2),_,X2,hyp(HYPS2))) :- 
 1051	not(not(X1 = X2)),
 1052	testEqualHypotheses(HYPS1,HYPS2),
 1053	equalWorlds(MS1,MS2), !.
 1054% To prove in(C,X) it is not allowed to use a constraint-clause generated 
 1055% from the same axiom
 1056sameAxiom(AX,_RN1,MS1,in(_C,X1),HYPS1,_D1,
 1057          constraint(rn(AX,_RN2,_,_),MS2,(card,app(_,X2),_Rel,_N),hyp(HYPS2))) :- 
 1058	not(not(X1 = X2)),
 1059	testEqualHypotheses(HYPS1,HYPS2),
 1060	equalWorlds(MS1,MS2), !.
 1061sameAxiom(AX,_RN1,MS1,in(_C,X1),HYPS1,_D1,
 1062          solveConstraint(rn(AX,_RN2,_,_),MS2,(card,app(_,X2),_Rel,_N),hyp(HYPS2))) :- 
 1063	not(not(X1 = X2)),
 1064	testEqualHypotheses(HYPS1,HYPS2),
 1065	equalWorlds(MS1,MS2), !.
 1066sameAxiom(AX,_RN1,MS1,eq(X1,_Y),HYPS1,_D1,
 1067          in(rn(AX,_RN2,_,_),modal(MS2),_C,X2,hyp(HYPS2),ab(_D2))) :- 
 1068	nonvar(X1),
 1069	nonvar(X2),
 1070	not(not(X1 = X2)),
 1071	testEqualHypotheses(HYPS1,HYPS2),
 1072	equalWorlds(MS1,MS2), !.
 1073sameAxiom(AX,_RN1,MS1,eq(_X,Y1),HYPS1,_D1,
 1074          in(rn(AX,_RN2,_,_),modal(MS2),_C,Y2,hyp(HYPS2),ab(_D2))) :- 
 1075	not(not(Y1 = Y2)),
 1076	testEqualHypotheses(HYPS1,HYPS2),
 1077	equalWorlds(MS1,MS2), !.
 1078sameAxiom(AX,_RN1,MS1,eq(X1,Y1),HYPS1,_D1,
 1079          eq(rn(AX,_RN2,_,_),modal(MS2),X2,Y2,hyp(HYPS2))) :- 
 1080	not(not(X1 = X2)),
 1081	not(not(Y1 = Y2)),
 1082	testEqualHypotheses(HYPS1,HYPS2),
 1083	equalWorlds(MS1,MS2), !.
 1084sameAxiom(AX,_RN1,MS1,eq(X1,app(_Y1)),HYPS1,_D1,
 1085          constraint(rn(AX,_RN2,_,_),MS2,(card,app(_,X2),_Rel,_N),hyp(HYPS2))) :-   
 1086	not(not(X1 = X2)),
 1087	testEqualHypotheses(HYPS1,HYPS2),
 1088	equalWorlds(MS1,MS2), 
 1089	!.
 1090sameAxiom(AX,_RN1,MS1,eq(_X,app(_F1:R1,Y1)),HYPS1,_D1,
 1091          constraint(rn(AX,_RN2,_,_),MS2,(card,app(_F2:R2,Y2),_Rel,_N),hyp(HYPS2))) :-
 1092	not(not(R1 = R2)),
 1093	not(not(Y1 = Y2)),
 1094	testEqualHypotheses(HYPS1,HYPS2),
 1095	equalWorlds(MS1,MS2), !.
 1096sameAxiom(AX,_RN1,MS1,eq(X1,app(_Y1)),HYPS1,_D1,
 1097          solveConstraint(rn(AX,_RN2,_,_),MS2,(card,app(_,X2),_Rel,_N),hyp(HYPS2))) :-   
 1098	not(not(X1 = X2)),
 1099	testEqualHypotheses(HYPS1,HYPS2),
 1100	equalWorlds(MS1,MS2), 
 1101	!.
 1102sameAxiom(AX,_RN1,MS1,eq(_X,app(_F1:R1,Y1)),HYPS1,_D1,
 1103          solveConstraint(rn(AX,_RN2,_,_),MS2,(card,app(_F2:R2,Y2),_Rel,_N),hyp(HYPS2))) :-
 1104	not(not(R1 = R2)),
 1105	not(not(Y1 = Y2)),
 1106	testEqualHypotheses(HYPS1,HYPS2),
 1107	equalWorlds(MS1,MS2), !.
 1108sameAxiom(AX,_RN1,MS1,eq(_X,Y1),HYPS1,_D1,
 1109          solveConstraint(rn(AX,_RN2,_,_),MS2,(card,app(_,Y2),_Rel,_N),hyp(HYPS2))) :-
 1110	not(not(Y1 = Y2)),
 1111	testEqualHypotheses(HYPS1,HYPS2),
 1112	equalWorlds(MS1,MS2), !.
 1113sameAxiom(AX,_RN1,MS1,c(X1,_,_),HYPS1,_D1,
 1114          in(rn(AX,_RN2,_,_),modal(MS2),_,X2,hyp(HYPS2),ab(_D2))) :- 
 1115	not(not(X1 = X2)),
 1116	testEqualHypotheses(HYPS1,HYPS2),
 1117	equalWorlds(MS1,MS2), !.
 1118sameAxiom(AX,_RN1,MS1,c(X1,_,_),HYPS1,_D1,
 1119          eq(rn(AX,_RN2,_,_),modal(MS2),X2,_,hyp(HYPS2))) :- 
 1120	not(not(X1 = X2)),
 1121	testEqualHypotheses(HYPS1,HYPS2),
 1122	equalWorlds(MS1,MS2), !.
 1123sameAxiom(AX,_RN1,MS1,c(X1,_,_),HYPS1,_D1,
 1124          eq(rn(AX,_RN2,_,_),modal(MS2),X2,_,hyp(HYPS2))) :- 
 1125	not(not(X1 = X2)),
 1126	testEqualHypotheses(HYPS1,HYPS2),
 1127	equalWorlds(MS1,MS2), !.
 1128sameAxiom(AX,_RN1,MS1,c(X1,_,_),HYPS1,_D1,
 1129          eq(rn(AX,_RN2,_,_),modal(MS2),_,app(_,X2),hyp(HYPS2))) :- 
 1130	not(not(X1 = X2)),
 1131	testEqualHypotheses(HYPS1,HYPS2),
 1132	equalWorlds(MS1,MS2), !.
 1133sameAxiom(AX,_RN1,MS1,c(X1,R1,Rel1),HYPS1,_D1,
 1134          constraint(rn(AX,_RN2,_,_),MS2,(card,app(_F:R2,X2),Rel2,_N),hyp(HYPS2))) :- 
 1135	not(not(X1 = X2)),
 1136	not(not(R1 = R2)),
 1137	not(not(Rel1 = Rel2)),
 1138	testEqualHypotheses(HYPS1,HYPS2),
 1139	equalWorlds(MS1,MS2), !.
 1140sameAxiom(AX,_RN1,MS1,c(X1,R1,Rel1),HYPS1,_D1,
 1141          solveConstraint(rn(AX,_RN2,_,_),MS2,(card,app(_F:R2,X2),Rel2,_N),hyp(HYPS2))) :- 
 1142	not(not(X1 = X2)),
 1143	not(not(R1 = R2)),
 1144	not(not(Rel1 = Rel2)),
 1145	testEqualHypotheses(HYPS1,HYPS2),
 1146	equalWorlds(MS1,MS2), !.
 1147sameAxiom(AX,_RN1,MS1,sc(X1,_,_),HYPS1,_D1,
 1148          in(rn(AX,_RN2,_,_),modal(MS2),_,X2,hyp(HYPS2),ab(_D2))) :- 
 1149	not(not(X1 = X2)),
 1150	testEqualHypotheses(HYPS1,HYPS2),
 1151	equalWorlds(MS1,MS2), !.
 1152sameAxiom(AX,_RN1,MS1,sc(X1,_,_),HYPS1,_D1,
 1153          eq(rn(AX,_RN2,_,_),modal(MS2),X2,_,hyp(HYPS2))) :- 
 1154	not(not(X1 = X2)),
 1155	testEqualHypotheses(HYPS1,HYPS2),
 1156	equalWorlds(MS1,MS2), !.
 1157sameAxiom(AX,_RN1,MS1,sc(X1,_,_),HYPS1,_D1,
 1158          eq(rn(AX,_RN2,_,_),modal(MS2),X2,_,hyp(HYPS2))) :- 
 1159	not(not(X1 = X2)),
 1160	testEqualHypotheses(HYPS1,HYPS2),
 1161	equalWorlds(MS1,MS2), !.
 1162sameAxiom(AX,_RN1,MS1,sc(X1,_,_),HYPS1,_D1,
 1163          eq(rn(AX,_RN2,_,_),modal(MS2),_,app(_,X2),hyp(HYPS2))) :- 
 1164	not(not(X1 = X2)),
 1165	testEqualHypotheses(HYPS1,HYPS2),
 1166	equalWorlds(MS1,MS2), !.
 1167sameAxiom(AX,_RN1,MS1,sc(X1,R1,Rel1),HYPS1,_D1,
 1168          constraint(rn(AX,_RN2,_,_),MS2,(card,app(_F:R2,X2),Rel2,_N),hyp(HYPS2))) :- 
 1169	not(not(X1 = X2)),
 1170	not(not(R1 = R2)),
 1171	not(not(Rel1 = Rel2)),
 1172	testEqualHypotheses(HYPS1,HYPS2),
 1173	equalWorlds(MS1,MS2), !.
 1174sameAxiom(AX,_RN1,MS1,sc(X1,R1,Rel1),HYPS1,_D1,
 1175          solveConstraint(rn(AX,_RN2,_,_),MS2,(card,app(_F:R2,X2),Rel2,_N),hyp(HYPS2))) :- 
 1176	not(not(X1 = X2)),
 1177	not(not(R1 = R2)),
 1178	not(not(Rel1 = Rel2)),
 1179	testEqualHypotheses(HYPS1,HYPS2),
 1180	equalWorlds(MS1,MS2), !.
 1181sameAxiom(_AX,_,_,_,_,_,_) :- !, fail.
 1182
 1183equalWorlds(W1,W2) :-
 1184	var(W1),
 1185	var(W2),
 1186	!.
 1187equalWorlds(W1,W2) :-
 1188	var(W1),
 1189	nonvar(W2),
 1190	!,
 1191	fail.
 1192equalWorlds(W1,W2) :-
 1193	var(W2),
 1194	nonvar(W1),
 1195	!,
 1196	fail.
 1197equalWorlds([],[]) :-
 1198	!.
 1199equalWorlds(app(_F:m(_MOp,_A),_W1),[]) :-
 1200	!,
 1201	fail.
 1202equalWorlds([],app(_F:m(_MOp,_A),_W2)) :-
 1203	!,
 1204	fail.
 1205equalWorlds(app(F1:m(MOp,A1),W1),app(F2:m(MOp,A2),W2)) :-
 1206	A1 == A2,
 1207%	var(F1),
 1208%	var(F2),
 1209%       not(not(F1 = F2)),
 1210	!,
 1211	equalWorlds(W1,W2).
 1212equalWorlds(app(F1:m(MOp,A1),_W1),app(F2:m(MOp,A2),_W2)) :-
 1213	A1 == A2,
 1214	nonvar(F1),
 1215	nonvar(F2),
 1216	not(not(F1 = F2)),
 1217	!.
 1218equalWorlds(_W1,_W2) :-
 1219	!,
 1220	fail.
 1221	
 1222
 1223noAxiom(true,_) :- !.
 1224noAxiom(_,[]) :- !.
 1225noAxiom(in(rn(AX,RN,_,_),modal(MS),C,X,hyp(HYPS),ab(D)),[C1|CL]) :-
 1226	not(sameAxiom(AX,RN,MS,in(C,X),HYPS,D,C1)),
 1227	noAxiom(in(rn(AX,RN,_,_),modal(MS),C,X,hyp(HYPS),ab(D)),CL).
 1228noAxiom(eq(rn(AX,RN,_,_),modal(MS),X,Y,hyp(HYPS)),[C1|CL]) :-
 1229	not(sameAxiom(AX,RN,MS,eq(X,Y),HYPS,_D,C1)),
 1230	noAxiom(eq(rn(AX,RN,_,_),modal(MS),X,Y,hyp(HYPS)),CL).
 1231noAxiom(constraint(rn(AX,RN,_,_),MS,(card,app(_F:R,X),Rel,N),hyp(HYPS)),[C1|CL]) :-
 1232	not(sameAxiom(AX,RN,MS,c(X,R,Rel),HYPS,_D,C1)),
 1233	noAxiom(constraint(rn(AX,RN,_,_),MS,(card,app(_,X),Rel,N),hyp(HYPS)),CL).
 1234noAxiom(solveConstraint(rn(AX,RN,_,_),MS,(card,app(_F:R,X),Rel,N),hyp(HYPS)),[C1|CL]) :-
 1235	not(sameAxiom(AX,RN,MS,sc(X,R,Rel),HYPS,_D,C1)),
 1236	noAxiom(solveConstraint(rn(AX,RN,_,_),MS,(card,app(_,X),Rel,N),hyp(HYPS)),CL).
 1237
 1238noDouble([in(rn(AX,RN,_,_),modal(MS),not(C),X,hyp(_HYPS1),ab(D))|IL]) :-
 1239	!,
 1240	not(member(in(rn(AX1,RN1,_,_),modal(MS),not(C),X,hyp(_HYPS2),ab(D)),IL)),
 1241	not(member(in(rn(AX2,RN2,_,_),modal(MS),C,X,hyps(_HYPS3),ab(noAb)),IL)),
 1242	!,
 1243	noDouble(IL).
 1244noDouble([in(rn(AX,RN,_,_),modal(MS),C,X,hyp(_HYPS1),ab(D))|IL]) :-
 1245	!,
 1246	not(member(in(rn(AX1,RN1,_,_),modal(MS),C,X,hyp(_HYPS2),ab(D)),IL)),
 1247	not(member(in(rn(AX2,RN2,_,_),modal(MS),not(C),X,hyps(_HYPS3),ab(noAb)),IL)),
 1248	!,
 1249	noDouble(IL).
 1250noDouble([eq(rn(AX,RN,_,_),modal(MS),X,Y,hyp(_HYPS1))|IL]) :-
 1251	!,
 1252	not(member(eq(rn(AX1,RN1,_,_),modal(MS),X,Y,hyp(_HYPS2)),IL)),
 1253	!,
 1254	noDouble(IL).
 1255noDouble([constraint(rn(AX,RN,_,_),MS,(card,app(_F:R,X),Rel,N),hyp(_HYPS1))|IL]) :-
 1256	!,
 1257	not(member(constraint(rn(AX1,RN1,_,_),MS,(card,app(_F:R,X),Rel,N),hyp(_HYPS2)),IL)),
 1258	!,
 1259	noDouble(IL).
 1260noDouble([solveConstraint(rn(AX,RN,_,_),MS,(card,app(_F:R,X),Rel,N),hyp(_HYPS1))|IL]) :-
 1261	!,
 1262	not(member(solveConstraint(rn(AX1,RN1,_,_),MS,(card,app(_F:R,X),Rel,N),hyp(_HYPS2)),IL)),
 1263	!,
 1264	noDouble(IL).
 1265noDouble([I1|IL]) :-
 1266	not(member(I1,IL)),
 1267	!,
 1268	noDouble(I1,IL).
 1269noDouble([]) :-
 1270	!.
 1271
 1272printAxiom(solveConstraint(MS,(card,app((_FF:R),X),Rel,N),hyp(HYPS))) :-
 1273	print('axiom???'),
 1274	print('   '),
 1275	print(solveConstraint(MS,(app(R,X),Rel,N),hyp(HYPS))),
 1276	!.
 1277printAxiom(eq(rn(AX,RN,_,_),modal(MS),Y,app((_FF:R),X),hyp(HYPS))) :-
 1278	print(rn(AX,RN)),
 1279	print('   '),
 1280	print(eq(MS,Y,app(R,X),hyp(HYPS))),
 1281	!.
 1282printAxiom(in(rn(AX,RN,_,_),modal(_MS),CN,CON,hyp(HYP))) :-
 1283	print(rn(AX,RN)),
 1284	print('   '),
 1285	print(in(CN,CON,hyp(HYP))),
 1286	!.
 1287printAxiom(constraint(rn(AX,RN,_,_),MS,(card,app((_FF:R),X),Rel,N),hyp(HYPS))) :-
 1288	print(rn(AX,RN)),
 1289	print('   '),
 1290	print(constraint(MS,(app(R,X),Rel,N),hyp(HYPS))),
 1291	!.
 1292printAxiom(true) :-
 1293	!.
 1294
 1295/**********************************************************************
 1296 *
 1297 * clashCS(+CL)
 1298 * succeeds if CL is a clash, i.e. it obeys one of the following 
 1299 * conditions:
 1300 * - it contains in('bot',X) for some X.
 1301 * - it contains both in(A,X) and in(not(A),X) for some A and some X.
 1302 *
 1303 */
 1304
 1305last([],[],_) :-
 1306	!,
 1307	fail.
 1308last([L1],[],L1) :-
 1309	!.
 1310last([L1|LL1],[L1|LL2],Last) :-
 1311	last(LL1,LL2,Last),
 1312	!.
 1313
 1314generateClashGoal(CS1,Goal) :-
 1315	last(CS1,CS2,in(rn(AX,RN,S,O),modal(W1),C,X,hyp(HYPS))),
 1316	getCurrentEnvironment(EnvName),
 1317	environment(EnvName,Env,_),
 1318	constructMLHead(Env,rn(_AX1,_RN1,user,_O1),W1,C1,X,CS1,noAb,[],_,Goal),
 1319	!.
 1320
 1321		
 1322clashCS(CL) :-
 1323	retract(clashTest(possible)),
 1324	assertz_logged(clashTest(impossible)),
 1325	generateClashGoal(CL,Goal),
 1326	!,
 1327	doClashTest(Goal).
 1328clashCS(_CL) :-
 1329	!,
 1330	fail.
 1331	
 1332doClashTest(InHead1) :-
 1333	call(InHead1),
 1334	InHead1 = in(Env,_,modal(W1),C1,X,hyp(HYP),ab(_),call(_CALL),_),
 1335	atomic(X),
 1336	normalizeNot(not(C1),C2),
 1337	constructMLHead(Env,rn(_AX2,_RN2,_S2,_O2),W1,C2,X,HYP,noAb,[],_,InHead2),
 1338	call(InHead2),
 1339	print('Clash test succeeded for'), nl,
 1340	print(HYP), nl,
 1341	print('and'), nl,
 1342	print(InHead1), nl,
 1343	nl,
 1344	retract(clashTest(impossible)),
 1345	assertz_logged(clashTest(possible)),
 1346	!.
 1347doClashTest(Goal) :-
 1348	% the clash goal has failed, so there is no clash
 1349	print('Clash test succeeded for'), nl,
 1350	print(HYP), nl,
 1351	nl,
 1352	retract(clashTest(impossible)),
 1353	assertz_logged(clashTest(possible)),
 1354	!,
 1355	fail.
 1356
 1357
 1358
 1359
 1360% clashCS(CL) :-
 1361% 	clashTest(possible),
 1362% 	member(in(rn(_,_,_,_),modal(_MS),'bot',_X,hyp(_HYPS1)),CL),
 1363% 	!.
 1364% clashCS(CL) :-
 1365% 	clashTest(possible),
 1366% 	member(in(rn(_,_,_,_),modal(MS),not(A),X,hyp(_HYPS1)),CL),
 1367% 	member(in(rn(_,_,_,_),modal(MS),A,X,hyp(_HYPS2)),CL),
 1368% 	!.
 1369% clashCS(CL) :-
 1370% 	clashTest(possible),
 1371% 	member(constraint(rn(_,_,_,_),MS,
 1372% 			  (card,app(_F1:R,X),'>=',N1),hyp(_HYPS1)),CL),
 1373% 	member(constraint(rn(_,_,_,_),MS,
 1374% 			  (card,app(_F2:R,X),'=<',N2),hyp(_HYPS2)),CL),
 1375% 	number(N1),
 1376% 	number(N2),
 1377% 	N1 > N2,
 1378% 	!.
 1379% clashCS(CL) :-
 1380% 	member(constraint(rn(_,_,_,_),MS,
 1381% 			  (card,app(_F1:R,X),'=<',N1),hyp(_HYPS1)),CL),
 1382% 	number(N1),
 1383% 	countAllRoleFillersInCS(MS,R,X,CL,N2),
 1384% 	N2 > N1,
 1385% 	!.
 1386% 		
 1387% 		 
 1388% countAllRoleFillersInCS(MS,R,X,CL,N) :-
 1389% 	getAllRoleFillersInCS(MS,R,X,CL,[],RF),
 1390% 	length(RF,N).
 1391% 
 1392% getAllRoleFillersInCS(_MS,_R,_X,[],RF,RF) :-
 1393% 	!.
 1394% getAllRoleFillersInCS(MS,R,X,
 1395%    [eq(rn(_,_,_,_),modal(MS),Y,app(_F:R,X),hyp(_HYPS))|CL],RF1,RF2) :-
 1396% 	nonvar(Y),
 1397% 	nonvar(X),
 1398% 	atomic(Y),
 1399% 	not(member((X,Y),RF1)),
 1400% 	!,
 1401% 	getAllRoleFillersInCS(MS,R,CL,[(X,Y)|RF1],RF2).
 1402% getAllRoleFillersInCS(MS,R,X,[_|CL],RF1,RF2) :-
 1403% 	getAllRoleFillersInCS(MS,R,X,CL,RF1,RF2),
 1404% 	!.
 1405
 1406/**********************************************************************
 1407 *
 1408 * @(#) clash.pl 1.2@(#)
 1409 *
 1410 */
 1411
 1412clashInHyp(CL) :-
 1413	member(in(_,modal(_MS),'bot',_X,hyp(_HYPS1),ab(_)),CL),
 1414	!.
 1415clashInHyp(CL) :-
 1416	member(in(_N2,modal(MS2),A,X,hyp(_HYPS2),ab(_D2)),CL),
 1417	atomic(A),
 1418	member(in(_N1,modal(MS1),not(A),X,hyp(_HYPS1),ab(_D1)),CL),
 1419	not(not(MS1 = MS2)),
 1420	!.
 1421% clashInHyp(CL) :-
 1422% 	member(constraint(rn(_,_,_,_),MS,
 1423% 			  (card,app(_F1:R,X),'>=',N1),hyp(_HYPS1)),CL),
 1424% 	member(constraint(rn(_,_,_,_),MS,
 1425% 			  (card,app(_F2:R,X),'=<',N2),hyp(_HYPS2)),CL),
 1426% 	number(N1),
 1427% 	number(N2),
 1428% 	N1 > N2,
 1429% 	!.
 1430% clashInHyp(CL) :-
 1431% 	member(constraint(rn(_,_,_,_),MS,
 1432% 			  (card,app(_F1:R,X),'=<',N1),hyp(_HYPS1)),CL),
 1433% 	number(N1),
 1434% 	countAllRoleFillersInCS(MS,R,X,CL,N2),
 1435% 	N2 > N1,
 1436% 	!.
 1437% 		
 1438% 		 
 1439% countAllRoleFillersInCS(MS,R,X,CL,N) :-
 1440% 	getAllRoleFillersInCS(MS,R,X,CL,[],RF),
 1441% 	length(RF,N).
 1442% 
 1443% getAllRoleFillersInCS(_MS,_R,_X,[],RF,RF) :-
 1444% 	!.
 1445% getAllRoleFillersInCS(MS,R,X,
 1446%    [eq(rn(_,_,_,_),modal(MS),Y,app(_F:R,X),hyp(_HYPS))|CL],RF1,RF2) :-
 1447% 	nonvar(Y),
 1448% 	nonvar(X),
 1449% 	atomic(Y),
 1450% 	not(member((X,Y),RF1)),
 1451% 	!,
 1452% 	getAllRoleFillersInCS(MS,R,CL,[(X,Y)|RF1],RF2).
 1453% getAllRoleFillersInCS(MS,R,X,[_|CL],RF1,RF2) :-
 1454% 	getAllRoleFillersInCS(MS,R,X,CL,RF1,RF2),
 1455% 	!.
 1456% 
 1457/**********************************************************************
 1458 *
 1459 * @(#) classifier.pl 1.12@(#)
 1460 *
 1461 */
 1462
 1463/***********************************************************************
 1464 *
 1465 * subsumes(+Name1,+Name2)
 1466 * Parameter: Name1     concept or role name
 1467 *            Name2     concept or role name
 1468 * true iff Name1 subsumes Name2 in modal context []
 1469 * (so Name1 and Name2 must both be concept names or role names).
 1470 *
 1471 */
 1472
 1473subsumes(N1,N2) :-
 1474	getCurrentEnvironment(EnvName),
 1475	subsumes(EnvName,[],N1,N2).
 1476
 1477/***********************************************************************
 1478 *
 1479 * subsumes(+MS,+Name1,+Name2)
 1480 * Parameter: MS        modal context
 1481 *            Name1     concept or role name
 1482 *            Name2     concept or role name
 1483 * true iff Name1 subsumes Name2 (so Name1 and Name2 must both be
 1484 * concept names or role names).
 1485 *
 1486 */
 1487
 1488subsumes(MS,N1,N2) :-
 1489	nonvar(MS),
 1490	(MS = [] ; MS = [_|_]),
 1491	currentEnvironment(Env),
 1492	clause(conceptName(Env,_MS1,_W1,N1),_),
 1493	clause(conceptName(Env,_MS2,_W2,N2),_),
 1494	!,
 1495	subsumes(concepts,Env,MS,N1,N2).
 1496subsumes(MS,N1,N2) :-
 1497	nonvar(MS),
 1498	(MS = [] ; MS = [_|_]),
 1499	currentEnvironment(Env),
 1500	clause(roleName(Env,_MS1,_W1,N1),_),
 1501	clause(roleName(Env,_MS2,_W2,N2),_),
 1502	subsumes(roles,Env,MS,N1,N2).
 1503
 1504subsumes(EnvName,MS,N1,N2) :-
 1505	environment(EnvName,Env,_),
 1506	nonvar(MS),
 1507	(MS = [] ; MS = [_|_]),
 1508	clause(conceptName(Env,_MS1,_W1,N1),_),
 1509	clause(conceptName(Env,_MS2,_W2,N2),_),
 1510	!,
 1511	subsumes(concepts,Env,MS,N1,N2).
 1512subsumes(EnvName,MS,N1,N2) :-
 1513	environment(EnvName,Env,_),
 1514	nonvar(MS),
 1515	(MS = [] ; MS = [_|_]),
 1516	currentEnvironment(Env),
 1517	clause(roleName(Env,_MS1,_W1,N1),_),
 1518	clause(roleName(Env,_MS2,_W2,N2),_),
 1519	subsumes(roles,Env,MS,N1,N2).
 1520
 1521subsumes(concepts,Env,MS,C,D) :-
 1522	convertMS(positive,Env,[[],true],MS,[],[W1,G1],_),
 1523	constructMLHead(Env,_RN1,W1,D,aaa,_HYPS,noAb,_CALLS,abox,InHeadD),
 1524	asserta_logged((InHeadD :- call(G1))),
 1525 	getQuery(Env,W1,C,aaa,Exp,InHeadC),
 1526%	convertToGoal(Env,_RN2,MS,C,aaa,[or([]),rl([]),fl(_DML1)],noAb,[],
 1527%		      _PT2,InHeadC),
 1528	call((call(G1), InHeadC)),
 1529	retract((InHeadD :- _Body)).
 1530subsumes(concepts,Env,MS,_C,D) :-
 1531	convertMS(positive,Env,[[],true],MS,[],[W1,_G1],_),
 1532	constructMLHead(Env,_RN1,W1,D,aaa,_HYPS,noAb,_CALLS,abox,InHeadD),
 1533	retract((InHeadD :- _Body)),
 1534	!,
 1535	fail.
 1536subsumes(roles,Env,MS,R,S) :-
 1537	convertMS(positive,Env,[[],true],MS,[],[W1,G1],_),
 1538	gensym(mskolem,SF),
 1539	constructEqHead(Env,_RN1,W1,bbb,SF,S,aaa,_HYPS,noAb,_CALLS,abox,InHeadS),
 1540	asserta_logged((InHeadS :- call(G1))),
 1541	constructEqHead(Env,_RN2,W1,bbb,_FF,R,aaa,[or([]),rl([]),fl(_DML1)],
 1542			noAb,[],_PT2,InHeadR),
 1543	call((G1, InHeadR)),
 1544	retract((InHeadS :- _Body)).
 1545subsumes(roles,Env,MS,_R,S) :-
 1546	convertMS(positive,Env,[[],true],MS,[],[W1,_G1],_),
 1547	constructEqHead(Env,_RN2,W1,bbb,_FF,S,aaa,_HYPS,noAb,_CALLS,_,InHeadS),
 1548	retract((InHeadS :- _Body)),
 1549	!,
 1550	fail.
 1551
 1552/***********************************************************************
 1553 *
 1554 * classified(+MS,+Name)
 1555 * succeeds iff Name is already in the appropriate subsumption hierarchy 
 1556 * in modal context MS.
 1557 *
 1558 */
 1559
 1560classified(Env,MS,Concept) :-
 1561	clause(conceptName(Env,_MS1,_W1,Concept),_),
 1562	!,
 1563	conceptHierarchy(Env,MS,Tree),
 1564	search(Concept,Tree).
 1565classified(Env,MS,Role) :-
 1566	clause(roleName(Env,_MS1,_W1,Role),_),
 1567	roleHierarchy(Env,MS,Tree),
 1568	search(Role,Tree).
 1569
 1570
 1571search(Concept,node(CL,_NL)) :-
 1572	member(Concept,CL),
 1573	!.
 1574search(Concept,node(_CL,NL)) :-
 1575	searchSubtrees(Concept,NL),
 1576	!.
 1577
 1578searchSubtrees(_Concept,[]) :-
 1579	!,
 1580	fail.
 1581searchSubtrees(Concept,[N1|_]) :-
 1582	search(Concept,N1),
 1583	!.
 1584searchSubtrees(Concept,[_|NL]) :-
 1585	searchSubtrees(Concept,NL).
 1586
 1587
 1588search(Concept,node(CL,NL),[node(CL,NL)]) :-
 1589	member(Concept,CL),
 1590	!.
 1591search(Concept,node(_CL,NL),T1) :-
 1592	searchSubtrees(Concept,NL,T1),
 1593	!.
 1594
 1595searchSubtrees(_Concept,[],[]) :-
 1596	!.
 1597searchSubtrees(Concept,[N1|NL],T2) :-
 1598	search(Concept,N1,T1),
 1599	searchSubtrees(Concept,NL,TL),
 1600	append(T1,TL,T2),
 1601	!.
 1602
 1603/***********************************************************************
 1604 *
 1605 * classify
 1606 * compute the subsumption hierarchy 
 1607 * side effects: 
 1608 * asserts a clause
 1609 *               conceptHierarchy(MS,Tree)
 1610 * where Tree is a tree representation of the subsumption hierarchy.
 1611 * This is now done using the new classification algorithm written
 1612 * by Patrick Brandmeier.
 1613 *
 1614 */
 1615
 1616classify :-
 1617	newClassify.
 1618classify(Arg1) :-
 1619	newClassify(Arg1).
 1620classify(EnvName,MS) :-
 1621	newClassify(EnvName,MS).
 1622
 1623/***********************************************************************
 1624 *
 1625 * classify(+NewConcept)
 1626 * adds concept NewConcept to the subsumption hierarchy in the modal
 1627 * context [].
 1628 * side effects: 
 1629 * asserts a clause
 1630 *               conceptHierarchy([],Tree)
 1631 * or            roleHierachy([],Tree)
 1632 * where Tree is a tree representation of the subsumption hierarchy.
 1633 *
 1634 */
 1635
 1636classify(EnvName,NewConcept) :-
 1637	environment(EnvName,Env,_),
 1638	atomic(NewConcept),
 1639	clause(conceptName(Env,_MS1,_W2,NewConcept),_), % _MS1 might be [] ?
 1640	classify(concepts,[],NewConcept).
 1641classify(EnvName,NewRole) :-
 1642	environment(EnvName,Env,_),
 1643	atomic(NewRole),
 1644	clause(roleName(Env,_MS1,_W1,NewRole),_), % _MS1 might be [] ?
 1645	classify(roles,[],NewRole).
 1646
 1647
 1648/***********************************************************************
 1649 *
 1650 * oldClassify
 1651 * compute the subsumption hierarchy in the modal context MS
 1652 * side effects: 
 1653 * asserts a clause
 1654 *               conceptHierarchy(MS,Tree)
 1655 * where Tree is a tree representation of the subsumption hierarchy.
 1656 * This is the original classification algorithm written by 
 1657 * Ullrich Hustadt.
 1658 *
 1659 */
 1660
 1661oldClassify :-
 1662	getCurrentEnvironment(EnvName),
 1663	oldClassify(EnvName,[]).
 1664
 1665oldClassify(EnvName) :-
 1666	environment(EnvName,_Env,_),
 1667	!,
 1668	oldClassify(EnvName,[]).
 1669oldClassify(MS) :-
 1670	(MS = [] ; MS = [_|_]),
 1671	getCurrentEnvironment(EnvName),
 1672	oldClassify(EnvName,MS).
 1673
 1674oldClassify(EnvName,MS) :-
 1675	environment(EnvName,Env,_),
 1676	clause(conceptName(Env,MS,_,Concept),_),
 1677	once(classify(concepts,Env,MS,Concept)),
 1678	fail.
 1679oldClassify(EnvName,MS) :-
 1680	environment(EnvName,Env,_),
 1681	clause(roleName(Env,MS,_,Role),_),
 1682	once(classify(roles,Env,MS,Role)),
 1683	fail.
 1684oldClassify(_,_) :-
 1685	!.
 1686	
 1687
 1688/***********************************************************************
 1689 *
 1690 * classify(+MS,+NewConcept)
 1691 * adds concept NewConcept to the subsumption hierarchy in the modal
 1692 * context MS.
 1693 * side effects: 
 1694 * asserts a clause
 1695 *               conceptHierarchy(MS,Tree)
 1696 * or            roleHierarchy(MS,Tree)
 1697 * where Tree is a tree representation of the subsumption hierarchy.
 1698 *
 1699 */
 1700 
 1701classify(EnvName,MS,NewConcept) :-
 1702	environment(EnvName,Env,_),
 1703	clause(conceptName(Env,_MS1,_W1,NewConcept),_), % _MS1 might be MS ?
 1704	!,
 1705	classify(concepts,Env,MS,NewConcept).
 1706classify(EnvName,MS,NewRole) :-
 1707	environment(EnvName,Env,_),
 1708	clause(roleName(Env,_MS1,_W1,NewRole),_), % _MS1 might be MS ?
 1709	!,
 1710	classify(roles,Env,MS,NewRole).
 1711
 1712classify(concepts,Env,MS,NewConcept) :-
 1713	classified(Env,MS,NewConcept),
 1714	!.
 1715classify(roles,Env,MS,NewRole) :-
 1716	classified(Env,MS,NewRole),
 1717	!.
 1718classify(concepts,Env,MS,NewConcept) :-
 1719	retract(conceptHierarchy(Env,MS,OldTree)),
 1720	classify(concepts,Env,MS,NewConcept,OldTree,NewTree),
 1721	assertz_logged(conceptHierarchy(Env,MS,NewTree)).
 1722classify(roles,Env,MS,NewRole) :-
 1723	retract(roleHierarchy(Env,MS,OldTree)),
 1724	classify(roles,Env,MS,NewRole,OldTree,NewTree),
 1725	assertz_logged(roleHierarchy(Env,MS,NewTree)).
 1726
 1727classify(Type,Env,MS,NewConcept,OldTree,NewTree) :-
 1728	testForSubsumption(Type,Env,MS,NewConcept,OldTree,NewTree,_Judgement),
 1729	!.
 1730
 1731
 1732/***********************************************************************
 1733 *
 1734 * testForSubsumption(+Type,+MS,+NewConcept,+OldTree
 1735 *                    -NewTree,-Judgement)
 1736 * builds a tree representation NewTree of the subsumption hierarchy 
 1737 * Judgement has the following meaning:
 1738 * below  : NewConcept is below  the 'top' concept of OldTree
 1739 *          in this case NewTree is instantiated with the tree which
 1740 *          has NewConcept inserted in OldTree
 1741 * beside : NewConcept is beside the 'top' concept of OldTree
 1742 *          in this case NewTree is instantiated with the tree which
 1743 *          has NewConcept as 'top' concept and all concepts of OldTree
 1744 *          which are subsumed by NewConcept below it
 1745 * above  : NewConcept is above  the 'top' concept of OldTree
 1746 *          in this case NewTree is not instantiated
 1747 * in     : NewConcept is equivalent to the 'top' concept of OldTree
 1748 *          in this case NewTree is instantiated with the tree which
 1749 *          has NewConcept inserted in OldTree
 1750 *
 1751 */
 1752
 1753testForSubsumption(Type,Env,MS,NewConcept,node([ClassifiedConcept|CL],AL),NewTree,Judgement) :-
 1754	once(subsume2(Type,Env,MS,NewConcept,ClassifiedConcept)), 
 1755	testForEquivalence(Type,Env,MS,NewConcept,node([ClassifiedConcept|CL],AL),NewTree,Judgement),
 1756	!.
 1757testForSubsumption(Type,Env,MS,NewConcept,node([ClassifiedConcept|CL],AL),NewTree,below) :-
 1758	% to get here the subsumption test in the first clause
 1759        % must have failed
 1760	once(subsume2(Type,Env,MS,ClassifiedConcept,NewConcept)),
 1761	% so only x \in NewConcept        => x \in ClassifiedConcept
 1762	% but not x \in ClassifiedConcept => x \in NewConcept
 1763	tfsList1(Type,Env,MS,NewConcept,[ClassifiedConcept|CL],[],AL,
 1764                below([]),beside([]),above([]),NewTree),
 1765	!.
 1766testForSubsumption(Type,Env,MS,NewConcept,node([ClassifiedConcept|CL],AL),NewTree,beside) :-
 1767	% neither x \in NewConcept        => x \in ClassifiedConcept
 1768	% nor     x \in ClassifiedConcept => x \in NewConcept
 1769	tfsList2(Type,Env,MS,NewConcept,[ClassifiedConcept|CL],[],AL,
 1770                below([]),beside([]),above([]),NewTree),
 1771	!.
 1772
 1773tfsList1(_Type,_,_MS,NewConcept,N,_NL1,[],
 1774        below(NL3),beside(NL4),above(NL5),Tree) :-
 1775	buildTree1(NewConcept,N,below(NL3),beside(NL4),above(NL5),Tree),
 1776	!.
 1777tfsList1(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1778        below(NL3),beside(NL4),above(NL5),NewTree) :-
 1779	testForSubsumption(Type,Env,MS,NewConcept,Node1,Tree,Judgement),
 1780	continue1(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1781	         below(NL3),beside(NL4),above(NL5),Tree,Judgement,NewTree).
 1782
 1783buildTree1(NewConcept,N,below([]),beside(NL2),above(NL3),
 1784	node(N,[node([NewConcept],NL3)|NL2])) :- 
 1785	!.
 1786buildTree1(_NewConcept,N,below(NL1),beside(NL2),above(_),
 1787	node(N,NL)) :-
 1788	motel_union(NL1,NL2,NL),
 1789	!.
 1790buildTree1(_NewConcept,_N,_,_,_,_) :-
 1791	!,
 1792	fail.
 1793
 1794	
 1795continue1(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1796         below(NL3),beside(NL4),above(NL5),Tree,below,NewTree) :-
 1797	% NL4 can be non-empty
 1798	% NL5 should be the empty list !
 1799	tfsList1(Type,Env,MS,NewConcept,N,[Node1|NL1],NL2,
 1800                below([Tree|NL3]),beside(NL4),above(NL5),NewTree),
 1801	!.
 1802continue1(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1803         below(NL3),beside(NL4),above(NL5),
 1804         node([NewConcept],[]),beside,NewTree) :-
 1805	tfsList1(Type,Env,MS,NewConcept,N,[Node1|NL1],NL2,
 1806                below(NL3),beside([Node1|NL4]),above(NL5),NewTree),
 1807	!.
 1808continue1(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1809         below(NL3),beside(NL4),above(NL5),
 1810         node([NewConcept],[N1|NL]),beside,NewTree) :-
 1811	motel_union(NL5,[N1|NL],NL6),
 1812	tfsList1(Type,Env,MS,NewConcept,N,[Node1|NL1],NL2,
 1813                below(NL3),beside([Node1|NL4]),above(NL6),NewTree),
 1814	!.
 1815continue1(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1816         below(NL3),beside(NL4),above(NL5),_Tree,above,NewTree) :-
 1817	tfsList1(Type,Env,MS,NewConcept,N,[Node1|NL1],NL2,
 1818	        below(NL3),beside(NL4),above([Node1|NL5]),NewTree),
 1819	!.
 1820continue1(_Type,_,_MS,_NewConcept,N,NL1,[_Node1|NL2],
 1821         below(_NL3),beside(_NL4),above(_NL5),
 1822         Tree,in,node(N,NL)) :-
 1823        % NL3, NL4 and NL5 can be non-empty
 1824	reverseList(NL1,NL6),
 1825	motel_union(NL6,[Tree|NL2],NL),
 1826	!.
 1827
 1828tfsList2(_Type,_,_MS,NewConcept,N,_NL1,[],
 1829        below(NL3),beside(NL4),above(NL5),Tree) :-
 1830	buildTree2(NewConcept,N,below(NL3),beside(NL4),above(NL5),Tree),
 1831	!.
 1832tfsList2(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1833        below(NL3),beside(NL4),above(NL5),NewTree) :-
 1834	testForSubsumption(Type,Env,MS,NewConcept,Node1,Tree,Judgement),
 1835	continue2(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1836	         below(NL3),beside(NL4),above(NL5),Tree,Judgement,NewTree).
 1837
 1838buildTree2(NewConcept,_N,below([]),beside(_NL2),above([]),
 1839	node([NewConcept],[])) :-
 1840	!.
 1841buildTree2(NewConcept,_N,below([]),beside(_NL2),above(NL3),
 1842	node([NewConcept],NL3)) :- 
 1843	!.
 1844buildTree2(_NewConcept,_N,_,_,_,_) :-
 1845	!,
 1846	fail.
 1847
 1848	
 1849continue2(_Type,_,_MS,_NewConcept,_N,_NL1,[_Node1|_NL2],
 1850         below(_NL3),beside(_NL4),above(_NL5),_Tree,below,_NewTree) :-
 1851	!,
 1852	fail.
 1853continue2(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1854         below(NL3),beside(NL4),above(NL5),_Tree,beside,NewTree) :-
 1855	tfsList2(Type,Env,MS,NewConcept,N,[Node1|NL1],NL2,
 1856                below(NL3),beside([Node1|NL4]),above(NL5),NewTree),
 1857	!.
 1858continue2(Type,Env,MS,NewConcept,N,NL1,[Node1|NL2],
 1859         below(NL3),beside(NL4),above(NL5),_Tree,above,NewTree) :-
 1860	tfsList2(Type,Env,MS,NewConcept,N,[Node1|NL1],NL2,
 1861	        below(NL3),beside(NL4),above([Node1|NL5]),NewTree),
 1862	!.
 1863continue2(_Type,_,_MS,_NewConcept,_N,_NL1,[_Node1|_NL2],
 1864         below(_NL3),beside(_NL4),above(_NL5),
 1865         _Tree,in,node(_N,_NL)) :-
 1866	!,
 1867	fail.
 1868
 1869testForEquivalence(Type,Env,MS,NewConcept,node([ClassifiedConcept|CL],AL),
 1870	           node([NewConcept,ClassifiedConcept|CL],AL),in) :-
 1871	once(subsume2(Type,Env,MS,ClassifiedConcept,NewConcept)),
 1872	% so NewConcept = ClassifiedConcept
 1873	!.
 1874testForEquivalence(_Type,_,_MS,_NewConcept,node([_ClassifiedConcept|_CL],_AL),
 1875	           _,above) :-
 1876	% so only x \in ClassifiedConcept => x \in NewConcept
 1877        % but not x \in NewConcept        => x \in ClassifiedConcept
 1878	!.
 1879
 1880subsume2(Type,Env,MS,X,Y) :- var(X),!,fail.
 1881subsume2(Type,Env,MS,X,Y) :- var(Y),!,fail.
 1882subsume2(Type,Env,MS,X,'top') :- !,fail.
 1883subsume2(Type,Env,MS,'bot',X) :- !,fail.
 1884subsume2(Type,Env,MS,X,'bot') :- !.
 1885subsume2(Type,Env,MS,'top',X) :- !.
 1886subsume2(Type,Env,MS,X,Y) :- 
 1887	sub3(X,Y),
 1888	!.
 1889subsume2(Type,Env,MS,X,Y) :- 
 1890	nsub3(X,Y),
 1891	!,fail. 
 1892subsume2(Type,Env,MS,X,Y) :- 
 1893	X \== Y,
 1894	subsumes(Type,Env,MS,X,Y), 
 1895  	cont4(X,Y),
 1896	!.
 1897subsume2(Type,Env,MS,X,Y) :- 
 1898	X \== Y,
 1899	cont5a(X,Y),
 1900	!,
 1901	fail.
 1902cont4('top',Y).
 1903cont4(X,Y) :- 
 1904	assert1(sub3(X,Y)),
 1905	succ3(Z,X),
 1906	cont4(Z,Y),!.
 1907cont4(X,Y). 
 1908cont5a('bot',X) :- !.
 1909cont5a(X,'bot') :- !,fail.
 1910cont5a(X,Y) :-
 1911	assert1(nsub3(X,Y)),
 1912	succ3(Y,Z),
 1913	cont5a(X,Z),!.
 1914
 1915assert2(G) :- not(G),assert_logged(G),!.
 1916assert2(_G) :-!.
 1917
 1918retract2(G) :- retract(G),!.
 1919retract2(_G) :- !.
 1920
 1921succ2(X,Y) :- succ3(X,Y),!.
 1922succ2(_X,'bot') :- !.
 1923
 1924
 1925/***********************************************************************
 1926 *
 1927 * showHierarchy(+Type)
 1928 * Parameter: Type     'concepts' or 'roles'
 1929 * display subsumption hierarchy in the modal context [].
 1930 *
 1931 */
 1932showHierarchy:- ignore(((member(Type,['concepts', 'roles']),showHierarchy(Type),fail))).
 1933showHierarchy(Type) :-
 1934	getCurrentEnvironment(EnvName),
 1935	showHierarchy(EnvName,[],Type).
 1936
 1937/***********************************************************************
 1938 *
 1939 * showHierarchy(+EnvName,+MS,+Type)
 1940 * Parameter: EnvName   environment name
 1941 *            MS        modal context
 1942 *            Type      'concepts' or 'roles'
 1943 * display subsumption hierarchy in the modal context MS.
 1944 *
 1945 */
 1946
 1947showHierarchy(EnvName,MS,concepts) :-
 1948	environment(EnvName,Env,_),
 1949	conceptHierarchy(Env,MS,Tree),
 1950	showDag([],Tree).
 1951showHierarchy(EnvName,MS,roles) :-
 1952	environment(EnvName,Env,_),
 1953	roleHierarchy(Env,MS,Tree),
 1954	showDag([],Tree).
 1955
 1956showHierarchy(EnvName,Type) :-
 1957	environment(EnvName,_,_),
 1958	!,
 1959	showHierarchy(EnvName,[],Type).
 1960showHierarchy(MS,Type) :-
 1961	(MS = [] ; MS = [_|_]),
 1962	!,
 1963	getCurrentEnvironment(EnvName),
 1964	showHierarchy(EnvName,MS,Type).
 1965
 1966/***********************************************************************
 1967 *
 1968 * getHierarchy(+Type,-H)
 1969 * Parameter: Type     'concepts' or 'roles'
 1970 * instantiates H with the internal representation of the subsumption 
 1971 * hierarchy of Type in the current environment and modal context [].
 1972 *
 1973 */
 1974
 1975getHierarchy(Type,H) :-
 1976	getCurrentEnvironment(EnvName),
 1977	getHierarchy(EnvName,[],Type,H).
 1978
 1979/***********************************************************************
 1980 *
 1981 * getHierarchy(+EnvName,+MS,+Type,-H)
 1982 * Parameter: EnvName   environment name
 1983 *            MS        modal context
 1984 *            Type      'concepts' or 'roles'
 1985 * instantiates H with the internal representation of the subsumption 
 1986 * hierarchy of Type in environment EnvName and modal context MS.
 1987 *
 1988 */
 1989
 1990getHierarchy(EnvName,MS,concepts,Tree) :-
 1991	environment(EnvName,Env,_),
 1992	conceptHierarchy(Env,MS,Tree).
 1993getHierarchy(EnvName,MS,roles,Tree) :-
 1994	environment(EnvName,Env,_),
 1995	roleHierarchy(Env,MS,Tree).
 1996
 1997getHierarchy(EnvName,Type,Tree) :-
 1998	environment(EnvName,_,_),
 1999	!,
 2000	getHierarchy(EnvName,[],Type,Tree).
 2001getHierarchy(MS,Type,Tree) :-
 2002	(MS = [] ; MS = [_|_]),
 2003	!,
 2004	getCurrentEnvironment(EnvName),
 2005	getHierarchy(EnvName,MS,Type,Tree).
 2006
 2007/***********************************************************************
 2008 *
 2009 * showDag(+Depth,+Tree)
 2010 * display subtree of the tree representation of the subsumption 
 2011 * hierarchy which is located at depth D, where D is the lenght of
 2012 * the list Depth of minus signs, in the hierarchy.
 2013 *
 2014 */
 2015
 2016showDag(Depth,node(CL,AL)) :-
 2017	writes(Depth),
 2018	writes(" "),
 2019	printClass(CL),
 2020	printArgs([45|Depth],AL).
 2021
 2022printClass([C1]) :-
 2023	print(C1),
 2024	nl,
 2025	!.
 2026printClass([C1,C2|CL]) :-
 2027	print(C1),
 2028	writes(" ("),
 2029	printRest([C2|CL]),
 2030	writes(")"),
 2031	nl.
 2032printRest([]) :- !.
 2033printRest([C1]) :-
 2034	print(C1).
 2035printRest([C1,C2|CL]) :-
 2036	print(C1),
 2037	print(", "),
 2038	printRest([C2|CL]).
 2039
 2040printArgs(_Depth,[]) :- !.
 2041printArgs(Depth,[N1|NL]) :-
 2042	showDag(Depth,N1),
 2043	printArgs(Depth,NL).
 2044
 2045
 2046
 2047
 2048
 2049
 2050/**********************************************************************
 2051 *
 2052 * @(#) classifier2.pl 1.35@(#)
 2053 *
 2054 */
 2055
 2056init_new_daten :- 
 2057	currentEnvironment(Env),
 2058	init_new_daten(Env).
 2059
 2060init_new_daten(Env) :-
 2061        init_succ(_),
 2062	init_sub(_),
 2063	init_nsub(_),
 2064	assert_logged(conceptName1(Env,_,'top')),
 2065	assert_logged(roleName1(Env,_,'top')),
 2066       	assertz_logged(succ(concepts,Env,_,'top','bot')),
 2067	assertz_logged(sub(concepts,Env,_,'top',_)),
 2068	assertz_logged(nsub(concepts,Env,_,X,X)),	
 2069	assertz_logged(succ(roles,Env,_,'top','bot')),
 2070	assertz_logged(sub(roles,Env,_,'top',_)),
 2071	assertz_logged(nsub(roles,Env,_,X,X)),
 2072	assertz_logged(sub(roles,Env,_,_,'bot')),
 2073	assertz_logged(sub(concepts,Env,_,_,'bot')).
 2074
 2075init_new_daten1 :-
 2076	currentEnvironment(Env),
 2077	!,
 2078	init_new_daten1(Env).	
 2079init_new_daten1(Env) :-
 2080	conceptName(Env,MS,W1,NewConcept),
 2081	not(name(NewConcept,[99,111,110,99,101,112,116|_])),
 2082	assert1(conceptName1(Env,MS,W1,NewConcept)),
 2083	fail.
 2084init_new_daten1(Env) :-
 2085	roleName(Env,MS,W1,NewRole),
 2086	not(name(NewRole,[114,111,108,101|_])),
 2087	assert1(roleName1(Env,MS,W1,NewRole)),
 2088	fail.
 2089init_new_daten1(Env).
 2090
 2091init_succ(MS) :- 
 2092 	currentEnvironment(Env),
 2093        init_succ(Env,MS),
 2094	!.
 2095init_succ(MS).
 2096init_succ(Env,MS) :- 
 2097	retractall_head(succ(_,Env,MS,_,_)),
 2098	!.
 2099init_sub(MS) :-
 2100	currentEnvironment(Env),
 2101	init_sub(Env,MS).
 2102init_sub(MS).
 2103init_sub(Env,MS) :- 
 2104	retractall_head(sub(_,Env,MS,_,_)),
 2105	!.
 2106
 2107init_nsub(MS) :-
 2108 	currentEnvironment(Env),
 2109	init_nsub(Env,MS).
 2110init_nsub(MS).
 2111init_nsub(Env,MS) :-
 2112	retractall_head(nsub(_,Env,MS,_,_)),
 2113	!.
 2114
 2115/********************************************************************/
 2116% Test-functions 
 2117
 2118neu1 :- newClassify,
 2119	show_dag([]),printStat. 
 2120show :- getCurrentEnvironment(EnvName),
 2121	environment(EnvName,Env,_),
 2122	showDefconcept(Env),
 2123	showDefprimconcept(Env),
 2124	showDefrole(Env),
 2125        showDefprimrole(Env).
 2126test1(Concept):- 
 2127	environment(EnvName,Env,_),	
 2128	conceptEqualSets(Env,user,MS,Concept,CT,_),
 2129	find_concept2(concepts,Env,MS,Concept,CT).
 2130
 2131test2 :- 
 2132	environment(EnvName,Env,_),	
 2133	conceptEqualSets(Env,user,MS,Concept,CT,_),
 2134	conceptEqualSets(Env,user,MS,Concept1,Concept,_),
 2135	print(Concept),
 2136	print(Concept1),nl,
 2137	fail.
 2138
 2139test3(MS,_) :- 
 2140	environment(EnvName,Env,_),	
 2141	conceptEqualSets(Env,user,MS,Concept,CT,_),
 2142	clause(conceptName(Env,_MS1,_W1,Concept),_),
 2143	conceptEqualSets(Env,user,MS,CT,Concept1,_),
 2144%	conceptName(Env,_MS2,_W2,Concept1),
 2145	print(Concept),print(" "),
 2146	print(CT),print(" "),
 2147	print(Concept1),
 2148	nl,
 2149	fail.
 2150test3(MS,_) :- 
 2151	environment(EnvName,Env,_),	
 2152	conceptSubsets(Env,user,MS,Concept,CT,_),
 2153	clause(conceptName(Env,_MS1,_W1,Concept),_),
 2154	conceptSubsets(Env,user,MS,CT,Concept1,_),
 2155%	not(conceptName(Env,_MS2,_W2,Concept)),
 2156	print(Concept),print(" "),
 2157	print(CT),print(" "),
 2158	print(Concept1),
 2159	nl,
 2160	fail.
 2161test3(MS) :- 
 2162	environment(EnvName,Env,_),	
 2163	roleEqualSets(Env,user,MS,Concept,CT,_),
 2164	clause(roleName(Env,_MS1,_W1,Concept),_),
 2165	roleEqualSets(Env,user,MS,CT,Concept1,_),
 2166%	roleName(Env,MS,Concept1),
 2167	print(Concept),print(" "),
 2168	print(CT),print(" "),
 2169	print(Concept1),
 2170	nl,
 2171	fail.
 2172
 2173test3(MS) :- 
 2174	environment(EnvName,Env,_),	
 2175	roleSubsets(Env,user,MS,Concept,CT,_),
 2176	clause(roleName(Env,_MS1,_W1,Concept),_),
 2177	roleSubsets(Env,user,MS,CT,Concept1,_),
 2178%	not(roleName(Env,_,MS,Concept)),
 2179	print(Concept),print(" "),
 2180	print(CT),print(" "),
 2181	print(Concept1),
 2182	nl,
 2183	fail.
 2184	
 2185% just for fun and test
 2186
 2187neu1(MS) :- newClassify(MS).
 2188
 2189newClassify :-
 2190	getCurrentEnvironment(EnvName),
 2191	newClassify(EnvName,[]).
 2192
 2193newClassify(EnvName) :-
 2194	environment(EnvName,_Env,_),
 2195	!,
 2196	newClassify(EnvName,[]).
 2197newClassify(MS) :-
 2198	(MS = [] ; MS = [_|_]),
 2199	getCurrentEnvironment(EnvName),
 2200	newClassify(EnvName,MS).
 2201
 2202newClassify(EnvName,MS) :-
 2203	environment(EnvName,Env,_),
 2204	testa(Env,MS).
 2205	
 2206testa(Env,MS) :-
 2207	init_new_daten(Env),
 2208	initStat,
 2209	testb(Env,MS),
 2210	buildOrdering(Env,MS,CTree,RTree),
 2211	retractall_head(conceptHierarchy(Env,MS,_)),
 2212	retractall_head(roleHierarchy(Env,MS,_)),
 2213	assert_logged(conceptHierarchy(Env,MS,CTree)),
 2214	assert_logged(roleHierarchy(Env,MS,RTree)),
 2215	ifOption(testOutput,yes,printStat),
 2216%	ifOption(testOutput,yes,show_dag(MS)),
 2217	!.	
 2218testb(Env,MS) :-
 2219        not(find_concept(concepts,Env,MS)),
 2220        not(find_role(roles,Env,MS)).
 2221	
 2222find_concept(concepts,Env,MS) :-
 2223	getConceptName(Env,MS,Concept),
 2224	not(name(Concept,[99,111,110,99,101,112,116|_])),
 2225	ifOption(testOutput,yes,(print(Concept), nl)),
 2226	addCounter(conceptsClassified,1),
 2227	find_concept1(concepts,Env,MS,Concept).
 2228find_role(roles,Env,MS) :-
 2229	getRoleName(Env,MS,Role),
 2230	not(name(Role,[114,111,108,101|_])),
 2231	addCounter(rolesClassified,1),
 2232	find_role1(roles,Env,MS,Role).
 2233
 2234find_role1(roles,Env,MS,Role) :-
 2235	roleEqualSets(Env,user,MS,Role,CT,_),
 2236	find_role2(roles,Env,MS,Role,CT),
 2237	!,
 2238 	fail.
 2239find_role1(roles,Env,MS,Role) :-
 2240	roleSubsets(Env,user,MS,Role,CT,_),
 2241	find_prole2(roles,Env,MS,Role,CT),
 2242 	!,
 2243	fail.
 2244/*
 2245find_role1(roles,Env,MS,Role) :-
 2246	roleEqualSets(Env,user,MS,Role,CT,_),
 2247	find_role11(roles,Env,MS,Role,CT),
 2248	!,
 2249	fail.
 2250find_role1(roles,Env,MS,Role) :-
 2251	roleSubsets(Env,user,MS,Role,CT,_),
 2252	find_role11(roles,Env,MS,Role,CT),
 2253	!,
 2254	fail.
 2255find_role11(roles,Env,MS,Role,CT) :-
 2256	roleEqualSets(Env,user,MS,CT,CT1,_),
 2257	find_prole2(roles,Env,MS,Role,CT1),
 2258	find_role11(roles,Env,MS,Role,CT).
 2259find_role11(roles,Env,MS,Role,CT) :-
 2260	roleSubsets(Env,user,MS,CT,CT1,_),
 2261	find_prole2(roles,Env,MS,Role,CT1),
 2262	find_role11(roles,Env,MS,Role,CT).
 2263*/
 2264
 2265find_role1(roles,Env,MS,Role) :-
 2266	make_succ2(roles,Env,MS,Role),
 2267	!,
 2268	fail.
 2269find_concept1(concepts,Env,MS,Concept) :-
 2270	conceptEqualSets(Env,user,MS,Concept,CT,_),
 2271	find_concept2(concepts,Env,MS,Concept,CT),
 2272	!,
 2273 	fail.
 2274find_concept1(concepts,Env,MS,Concept) :-
 2275	conceptSubsets(Env,user,MS,Concept,CT,_),
 2276	find_pconcept2(concepts,Env,MS,Concept,CT),
 2277 	!,
 2278	fail.
 2279/*
 2280find_concept1(concepts,Env,MS,Concept) :-
 2281	conceptEqualSets(Env,user,MS,Concept,CT,_),
 2282	find_concept11(concepts,Env,MS,Concept,CT),
 2283	!,
 2284	fail.
 2285find_concept1(concepts,Env,MS,Concept) :-
 2286	conceptSubsets(Env,user,MS,Concept,CT,_),
 2287	find_concept11(concepts,Env,MS,Concept,CT),
 2288	!,
 2289	fail.
 2290find_concept11(concepts,Env,MS,Concept,CT) :-
 2291	conceptEqualSets(Env,user,MS,CT,CT1,_),
 2292	find_pconcept2(concepts,Env,MS,Concept,CT1),
 2293	find_concept11(concepts,Env,MS,Concept,CT).
 2294find_concept11(concepts,Env,MS,Concept,CT) :-
 2295	conceptSubsets(Env,user,MS,CT,CT1,_),
 2296	find_pconcept2(concepts,Env,MS,Concept,CT1),
 2297	find_concept11(concepts,Env,MS,Concept,CT).
 2298*/
 2299find_concept1(concepts,Env,MS,Concept) :-
 2300	make_succ2(concepts,Env,MS,Concept),
 2301	!,
 2302	fail.
 2303/***** Entwicklungsecke....
 2304
 2305test fuer den trans.abschluss von roleEqualSets,roleSubsets,concept...
 2306find_role1(roles,Env,MS,Role) :-
 2307	roleEqualSets(Env,user,MS,Role,CT,_),
 2308	find_role11(roles,Env,MS,Role,CT),
 2309	!,
 2310	fail.
 2311find_role11(roles,Env,MS,Role,CT) :-
 2312	find_role2(roles,Env,MS,Role,CT),
 2313	!,
 2314	roleEqualSets(Env,user,MS,CT,CT1,_),
 2315	find_role11(roles,Env,MS,Role,CT1),
 2316	!.
 2317find_role11(roles,Env,MS,Role,CT) :-
 2318	!.
 2319
 2320find_role1(roles,Env,MS,Role) :-
 2321	roleSubsets(Env,user,MS,Role,CT,_),
 2322	find_prole11(roles,Env,MS,Role,CT),
 2323 	!,
 2324	fail.
 2325find_prole11(roles,Env,MS,Role,CT) :-
 2326	find_prole2(roles,Env,MS,Role,CT),
 2327	!,
 2328	roleSubsets(Env,user,MS,CT,CT1,_),
 2329	find_prole11(roles,Env,MS,Role,CT1),
 2330	!.
 2331find_prole11(roles,Env,MS,Role,CT) :-
 2332	!.
 2333*/
 2334
 2335/*******************************************/
 2336
 2337find_concept2(concepts,Env,MS,Concept,CT) :-
 2338	getConceptName(Env,MS,CT),
 2339	(succ(concepts,Env,MS,Topconcept,Concept),
 2340	subsume1(concepts,Env,MS,Topconcept,CT)),
 2341	assert1(nsub(concepts,Env,MS,Concept,CT)),
 2342	assert1(nsub(concepts,Env,MS,CT,Concept)),
 2343	assert_succ(concepts,Env,MS,Topconcept,CT),
 2344	!.	
 2345find_concept2(concepts,Env,MS,Concept,CT) :-
 2346%	getConceptName(Env,_MS1,W1,CT),
 2347	getConceptName(Env,MS,CT),
 2348	(succ(concepts,Env,MS,Topconcept,CT),
 2349	subsume1(concepts,Env,MS,Topconcept,Concept)),
 2350	assert1(nsub(concepts,Env,MS,Concept,CT)),
 2351	assert1(nsub(concepts,Env,MS,CT,Concept)),
 2352	assert_succ(concepts,Env,MS,Topconcept,Concept),
 2353	!.
 2354find_concept2(concepts,Env,MS,Concept,CT) :-
 2355	getConceptName(Env,MS,CT),
 2356	assert1(nsub(concepts,Env,MS,Concept,CT)),
 2357	assert1(nsub(concepts,Env,MS,CT,Concept)),
 2358	assert1(succ(concepts,Env,MS,'top',Concept)),
 2359	assert1(succ(concepts,Env,MS,'top',CT)),
 2360	!.
 2361find_concept2(concepts,Env,MS,Concept,CT) :-
 2362	CT = and([X|[R]]),
 2363	conceptEqualSets(Env,user,MS,Concept1,R,_),
 2364	assert_succ(concepts,Env,MS,X,Concept),
 2365	assert_succ(concepts,Env,MS,Concept1,Concept),		
 2366	!. 
 2367find_concept2(concepts,Env,MS,Concept,CT) :-
 2368	CT = and(L),
 2369	find_concept21(concepts,Env,MS,Concept,L),
 2370	!.
 2371
 2372find_concept2(concepts,Env,MS,Concept,CT) :-
 2373	CT = and([X|[R]]),
 2374	R = some(Role,Concept1),
 2375	getRoleName(Env,MS,Role),
 2376	X == Concept1,
 2377	assert_succ(concepts,Env,MS,X,Concept),	
 2378	!.
 2379
 2380find_concept2(concepts,Env,MS,Concept,CT) :-
 2381	CT = some(Role,Concept1),
 2382	find_concept25(Env,MS,Concept,Concept1),
 2383	!. 
 2384
 2385find_concept2(concepts,Env,MS,Concept,CT) :-
 2386	CT = or([and(L)]),
 2387	find_concept26(concepts,Env,MS,Concept,L),
 2388	!.
 2389	
 2390find_concept2(concepts,Env,MS,Concept,CT) :-
 2391	CT = or([L|R]),
 2392	L = and(L1),
 2393	find_concept3(Env,MS,Concept,R,L1,Z),
 2394	find_concept31(Env,MS,Concept,Z),	
 2395	!.
 2396find_concept2(concepts,Env,MS,Concept,CT) :-
 2397	CT = or(L),
 2398	find_concept26(concepts,Env,MS,Concept,L),
 2399	!.
 2400
 2401find_concept21(concepts,Env,MS,Concept,[]) :-
 2402	!.
 2403find_concept21(concepts,Env,MS,Concept,[X|R]) :-
 2404	getConceptName(Env,MS,X),
 2405	assert_succ(concepts,Env,MS,X,Concept),
 2406	find_concept21(concepts,Env,MS,Concept,R),
 2407	!.
 2408find_concept21(concepts,Env,MS,Concept,[X|R]) :-    
 2409	X = not(R1),
 2410	getConceptName(Env,MS,R1),
 2411	setofOrNil(K,find_concept22(concepts,Env,MS,Concept,R1,K),L),
 2412	find_concept23(concepts,Env,MS,Concept,L),
 2413	find_concept21(concepts,Env,MS,Concept,R),
 2414	!.
 2415find_concept21(concepts,Env,MS,Concept,[X|R]) :-
 2416	find_concept21(concepts,Env,MS,Concept,R),
 2417	!,
 2418	fail.
 2419
 2420find_concept22(concepts,Env,MS,Concept,R1,K) :-
 2421	succ(concepts,Env,MS,K,R1),
 2422	not(succ(concepts,Env,MS,K,Concept)).
 2423
 2424find_concept23(concepts,Env,MS,Concept,[]) :-
 2425	!.	
 2426find_concept23(concepts,Env,MS,Concept,[L1|R1]) :-
 2427	find_concept24(concepts,Env,MS,Concept,L1),
 2428	find_concept23(concepts,Env,MS,Concept,R1),
 2429	!.
 2430find_concept24(concepts,Env,MS,Concept,L1) :-
 2431	succ(concepts,Env,MS,Top,L1),
 2432	succ(concepts,Env,MS,Top,K),
 2433	subsume1(concepts,Env,MS,K,Concept),
 2434	setofOrNil(Nf,succ(concepts,Env,MS,K,Nf),Lnf),
 2435	make_succ1(concepts,Env,MS,K,Lnf,Concept),
 2436	!. 
 2437		
 2438find_concept25(Env,MS,Concept,Concept1) :-
 2439	succ(concepts,Env,MS,K,Concept1),
 2440	setofOrNil(Nf,succ(concepts,Env,MS,Concept1,Nf),Lnf),
 2441	make_succ1(concepts,Env,MS,K,Lnf,Concept),
 2442	fail.
 2443find_concept25(Env,MS,Concept,Concept1).
 2444
 2445find_concept26(concepts,Env,MS,Concept,[C1|R]) :-
 2446	getConceptName(Env,MS,C1),
 2447	subsume1(concepts,Env,MS,C1,Concept),
 2448	assert_succ(concepts,Env,MS,C1,Concept),
 2449	find_concept26(concepts,Env,MS,Concept,R).
 2450
 2451find_concept3(Env,MS,Concept,[],Z,Z) :- 
 2452	!.
 2453find_concept3(Env,MS,Concept,[L|R],Z,K) :-
 2454	L = and(L1),
 2455	intersection_motel(Z,L1,Z1),
 2456	find_concept3(Env,MS,Concept,R,Z1,K),
 2457	!.
 2458
 2459find_concept31(Env,MS,Concept,[]) :-
 2460	!.
 2461find_concept31(Env,MS,Concept,[L1|R1]) :-
 2462	assert_succ(concepts,Env,MS,L1,Concept),
 2463	find_concept31(Env,MS,Concept,R1),
 2464	!.
 2465
 2466% das hier ist die entwicklungsecke....	
 2467/*
 2468% weiss nicht ob das stimmt
 2469find_concept21(concepts,Env,MS,Concept,[X|R]) :-    
 2470	X = all(R1,X1),
 2471	getRoleName(Env,MS,R1),
 2472	getConceptName(Env,MS,X1),
 2473	assert_succ(concepts,Env,MS,X1,Concept),
 2474	find_concept21(concepts,Env,MS,Concept,R),
 2475	!.
 2476*/
 2477% ********************** Primconcepte **************************
 2478% es fehlt noch defprimconcept(_,_,some(_,_..))
 2479%                   "         (_,not(),...)
 2480%                   "         (_,...(),...)
 2481					
 2482find_pconcept2(concepts,Env,MS,PrimConcept,CT) :-
 2483	CT = not(X),
 2484	getConceptName(Env,MS,X),
 2485	cont1a(concepts,Env,MS,[],X,PrimConcept),
 2486%	succ(concepts,Env,MS,Topconcept,X),
 2487	find_pconcept23(Env,MS,X,PrimConcept,Top),
 2488	assert_succ(concepts,Env,MS,Top,PrimConcept),
 2489	assert_succ(concepts,Env,MS,Top,X),
 2490	!.
 2491find_pconcept2(concepts,Env,MS,Primconcept,CT) :-
 2492	CT = and(L),
 2493	find_pconcept24(Env,MS,Primconcept,L),
 2494	!.
 2495
 2496find_pconcept2(concepts,Env,MS,PrimConcept,CT) :-
 2497	getConceptName(Env,MS,CT),
 2498	assert1(sub(concepts,Env,MS,CT,PrimConcept)),
 2499	direct_succ(concepts,Env,MS,[],CT,PrimConcept,Z,L1),
 2500        contb(concepts,Env,MS,Z,L1,PrimConcept),
 2501	!.
 2502
 2503find_pconcept2(concepts,Env,MS,PrimConcept,CT) :-
 2504	CT = some(X,Y),
 2505	find_pconcept21(Env,MS,PrimConcept,X,Y),
 2506	!.
 2507
 2508find_pconcept2(concepts,Env,MS,Primconcept,CT) :-
 2509	CT = and([X|[R]]),
 2510%	getConceptName(Env,MS,W1,X),
 2511	getConceptName(Env,MS,X),
 2512	R = not(Y),
 2513	getConceptName(Env,MS,Y),
 2514	find_pconcept23(Env,MS,X,Y,Top),
 2515	assert_succ(concepts,Env,MS,Top,PrimConcept),	
 2516%	assert1(sub(concepts,Env,MS,PrimConcept)),
 2517	!.
 2518
 2519
 2520
 2521find_pconcept2(concepts,Env,MS,Primconcept,CT) :-
 2522	CT = or([and(L)]),
 2523	find_pconcept26(concepts,Env,MS,Primconcept,L),
 2524	!.
 2525	
 2526find_pconcept2(concepts,Env,MS,Primconcept,CT) :-
 2527	CT = or([L|R]),
 2528	L = and(L1),
 2529	find_pconcept3(Env,MS,Primconcept,R,L1,Z),
 2530	find_pconcept31(Env,MS,Primconcept,Z),	
 2531	!.
 2532find_pconcept2(concepts,Env,MS,Primconcept,CT) :-
 2533	CT = or(L),
 2534	find_pconcept26(concepts,Env,MS,Primconcept,L),
 2535	!.
 2536
 2537find_pconcept26(concepts,Env,MS,Primconcept,[C1|R]) :-
 2538%	getConceptName(Env,_MS,W1,C1),
 2539	getConceptName(Env,MS,X),
 2540	subsume1(concepts,Env,MS,C1,Primconcept),
 2541	find_pconcept27(concepts,Env,MS,Primconcept,C1),
 2542  	find_pconcept26(concepts,Env,MS,Primconcept,R).
 2543
 2544find_pconcept27(concepts,Env,MS,Primconcept,C1):-
 2545	assert1(sub(concepts,Env,MS,C1,Primconcept)),
 2546	direct_succ(concepts,Env,MS,[],C1,PrimConcept,Z,L1),
 2547        contb(concepts,Env,MS,Z,L1,PrimConcept),
 2548	!.
 2549
 2550find_pconcept3(Env,MS,Primconcept,[],Z,Z) :- 
 2551	!.
 2552find_pconcept3(Env,MS,Primconcept,[L|R],Z,K) :-
 2553	L = and(L1),
 2554	intersection_motel(Z,L1,Z1),
 2555	find_pconcept3(Env,MS,Primconcept,R,Z1,K),
 2556	!.
 2557
 2558find_pconcept31(Env,MS,Primconcept,[]) :-
 2559	!.
 2560find_pconcept31(Env,MS,Primconcept,[L1|R1]) :-
 2561	find_pconcept27(concepts,Env,MS,Primconcept,L1),
 2562	find_pconcept31(Env,MS,Primconcept,R1),
 2563	!.
 2564
 2565
 2566find_pconcept21(Env,MS,PrimConcept,X,Y) :-
 2567	Y = or([Y1|[Y2]]),
 2568	conceptEqualSets(Env,user,MS,Concept,some(X,Y1),_),
 2569	conceptEqualSets(Env,user,MS,Concept1,some(X,Y2),_),
 2570	find_pconcept23(Env,MS,Concept1,Concept,Top),
 2571	assert_succ(concepts,Env,MS,Top,PrimConcept),
 2572	!.
 2573
 2574find_pconcept23(Env,MS,X,Y,X) :-
 2575	sub(concepts,Env,MS,X,Y),
 2576	!.
 2577find_pconcept23(Env,MS,X,Y,Y) :-
 2578	sub(concepts,Env,MS,Y,X),
 2579	!.
 2580find_pconcept23(Env,MS,X,Y,Top) :-
 2581	sub(concepts,Env,MS,Top,X),sub(concepts,Env,MS,Top,Y).
 2582
 2583find_pconcept24(Env,MS,Primconcept,[X|R]) :-
 2584	getConceptName(Env,MS,X),
 2585	assert1(sub(concepts,Env,MS,X,PrimConcept)),
 2586	direct_succ(concepts,Env,MS,[],X,PrimConcept,Z,L1),
 2587        contb(concepts,Env,MS,Z,L1,PrimConcept),
 2588	find_pconcept24(Env,MS,Primconcept,R),
 2589	!.
 2590
 2591/*	
 2592find_pconcept2(concepts,Env,MS,Primconcept,CT) :-
 2593	CT = and([X|[R]]),
 2594	getConceptName(Env,_MS1,W1,X),
 2595	getConceptName(Env,_MS2,W2,R),
 2596	direct_succ(concepts,Env,MS,[],X,PrimConcept,Z,L1),
 2597        contb(concepts,Env,MS,Z,L1,PrimConcept),
 2598	!.
 2599
 2600find_pconcept2(concepts,Env,MS,PrimConcept,CT) :-
 2601	conceptName1(Env,MS1,CT),
 2602	find_pconcept23(Env,MS,CT,PrimConcept,Top),
 2603	assert_succ(concepts,Env,MS,Top,PrimConcept),
 2604	assert_succ(concepts,Env,MS,Top,CT),
 2605	!.
 2606*/
 2607
 2608/*************************************************************************
 2609*                    jetzt mit rollen
 2610*/
 2611find_role2(roles,Env,MS,Role,CT) :-
 2612	getRoleName(Env,MS,CT),
 2613	succ(roles,Env,MS,Toprole,Role),
 2614	assert1(nsub(roles,Env,MS,Role,Ct)),
 2615	assert1(nsub(roles,Env,MS,Ct,Role)),
 2616	assert_succ(roles,Env,MS,Toprole,CT),
 2617	!.	
 2618find_role2(roles,Env,MS,Role,CT) :-
 2619	getRoleName(Env,MS,CT),
 2620	succ(roles,Env,MS,Toprole,CT),
 2621	assert1(nsub(roles,Env,MS,Role,Ct)),
 2622	assert1(nsub(roles,Env,MS,Ct,Role)),
 2623	assert_succ(roles,Env,MS,Toprole,Role),
 2624	!.
 2625find_role2(roles,Env,MS,Role,CT) :-	
 2626	getRoleName(Env,MS,CT),
 2627	assert1(nsub(roles,Env,MS,Role,Ct)),
 2628	assert1(nsub(roles,Env,MS,Ct,Role)),
 2629	assert_succ(roles,Env,MS,'top',Role),
 2630	assert_succ(roles,Env,MS,'top',CT),
 2631	!.	
 2632find_role2(roles,Env,MS,Role,CT) :-	
 2633	CT = and([X|[R]]),
 2634	roleEqualSets(Env,user,MS,Role1,R,_),
 2635	assert_succ(roles,Env,MS,X,Role),
 2636	assert_succ(roles,Env,MS,Role1,Role),	
 2637	!. 
 2638find_role2(roles,Env,MS,Role,CT) :-	
 2639	CT = and([X|[R]]),
 2640	getRoleName(Env,MS,X),
 2641	getRoleName(Env,MS,R),
 2642	assert_succ(roles,Env,MS,X,Role),
 2643	assert_succ(roles,Env,MS,R,Roles),
 2644	!.
 2645find_role2(roles,Env,MS,Role,CT) :-	
 2646	CT = and([X|[R]]),
 2647	R = some(_,Role1),
 2648	X == Role1,
 2649	assert_succ(Roles,Env,MS,X,Role),	
 2650	!.
 2651find_role2(roles,Env,MS,Role,CT) :-	
 2652	CT = or([X|[R]]),
 2653	find_role3(Env,MS,Role,X,R).
 2654find_role2(roles,Env,MS,Role,CT) :-
 2655	CT = and(L),
 2656	find_role21(roles,Env,MS,Role,L),
 2657	!.
 2658find_role2(roles,Env,MS,Role,CT) :-
 2659	CT = restr(Role1,Concept),
 2660	assert_succ(roles,Env,MS,Role1,Role),
 2661	!.
 2662
 2663
 2664find_role2(roles,Env,MS,Role,CT) :-
 2665	CT = or([and(L)]),
 2666	find_role26(roles,Env,MS,Role,L),
 2667	!.
 2668	
 2669find_role2(roles,Env,MS,Role,CT) :-
 2670	CT = or([L|R]),
 2671	L = and(L1),
 2672	find_role30(Env,MS,Role,R,L1,Z),
 2673	find_role31(Env,MS,Role,Z),	
 2674	!.
 2675find_role2(roles,Env,MS,Role,CT) :-
 2676	CT = or(L),
 2677	find_role26(roles,Env,MS,Role,L),
 2678	!.
 2679
 2680find_role26(roles,Env,MS,Role,[C1|R]) :-
 2681	getRoleName(Env,MS,C1),
 2682	subsume1(roles,Env,MS,C1,Role),
 2683	assert_succ(roles,Env,MS,C1,Role),
 2684	find_role26(roles,Env,MS,Role,R).
 2685
 2686find_role30(Env,MS,Role,[],Z,Z) :- 
 2687	!.
 2688find_role30(Env,MS,Role,[L|R],Z,K) :-
 2689	L = and(L1),
 2690	intersection_motel(Z,L1,Z1),
 2691	find_role30(Env,MS,Role,R,Z1,K),
 2692	!.
 2693
 2694find_role31(Env,MS,Role,[]) :-
 2695	!.
 2696find_role31(Env,MS,Role,[L1|R1]) :-
 2697	assert_succ(roles,Env,MS,L1,Role),
 2698	find_role31(Env,MS,Role,R1),
 2699	!.
 2700
 2701
 2702find_role3(Env,MS,Role,X,R) :-
 2703	X = and([X1|[R1]]),
 2704	subsume1(roles,Env,MS,Role,R1),
 2705	find_role2(roles,Env,MS,Role,X).
 2706find_role3(Env,MS,Role,X,R) :-
 2707	R = and([X1|[R1]]),
 2708	subsume1(roles,Env,MS,Role,R1),
 2709	find_role2(roles,Env,MS,Role,X).
 2710
 2711find_role21(roles,Env,MS,Role,[]) :-
 2712	!.
 2713find_role21(roles,Env,MS,Role,[X|R]) :-
 2714	getRoleName(Env,MS,X),
 2715	assert_succ(roles,Env,MS,X,Role),
 2716	find_role21(roles,Env,MS,Role,R),
 2717	!.
 2718find_role21(roles,Env,MS,Role,[X|R]) :-
 2719	X = not(R1),
 2720	getRoleName(Env,MS,R1),
 2721	setofOrNil(K,find_role22(roles,Env,MS,Role,R1,K),L),
 2722	find_role23(roles,Env,MS,Role,L),
 2723	!.
 2724find_role22(roles,Env,MS,Role,R1,K) :-
 2725	succ(roles,Env,MS,K,R1),
 2726	not(succ(roles,Env,MS,K,Role)).
 2727
 2728find_role23(roles,Env,MS,Role,[]) :-
 2729	!.	
 2730find_role23(roles,Env,MS,Role,[L1|R1]) :-
 2731	find_role24(roles,Env,MS,Role,L1),
 2732	find_role23(roles,Env,MS,Role,R1),
 2733	!.
 2734find_role24(roles,Env,MS,Role,L1) :-
 2735	succ(roles,Env,MS,Top,L1),
 2736	succ(roles,Env,MS,Top,K),
 2737	subsume1(roles,Env,MS,K,Role),
 2738	setofOrNil(Nf,succ(roles,Env,MS,K,Nf),Lnf),
 2739	make_succ1(roles,Env,MS,K,Lnf,Role),
 2740	!.
 2741
 2742/******** PrimRollen ************************************************/
 2743
 2744find_prole2(roles,Env,MS,PrimRole,CT) :-
 2745	CT = and(L),
 2746	find_prole24(Env,MS,PrimRole,L),
 2747	!.
 2748
 2749find_prole2(roles,Env,MS,PrimRole,CT) :-
 2750	CT = not(X),
 2751	getRoleName(Env,MS,X),
 2752	cont1a(roles,Env,MS,X,PrimRole),
 2753	find_prole23(Env,MS,X,PrimRole,Top),
 2754	assert_succ(roles,Env,MS,Top,PrimRole),
 2755	assert_succ(roles,Env,MS,Top,X),
 2756	!.
 2757
 2758find_prole2(roles,Env,MS,PrimRole,CT) :-
 2759	convertMS(Env,[[],true],MS,[],[W1,G1],_),
 2760	call(G1),
 2761	getRoleName(Env,MS,CT),
 2762	assert1(sub(roles,Env,MS,CT,PrimRole)),
 2763	direct_succ(roles,Env,MS,[],CT,PrimRole,Z,L1),
 2764              contb(roles,Env,MS,Z,L1,PrimRole),
 2765	!.
 2766/*
 2767find_prole2(roles,Env,MS,PrimRole,CT) :-
 2768	CT = and([X|[R]]),
 2769	getRoleName(Env,MS,X),
 2770	getRoleName(Env,MS,R),	
 2771	find_prole23(Env,MS,X,R,Top),
 2772	assert_succ(roles,Env,MS,Top,PrimRole),
 2773	!.
 2774
 2775find_prole2(roles,Env,MS,PrimRole,CT) :-
 2776	getRoleName(Env,MS,CT),
 2777	find_prole23(Env,MS,PrimRole,CT,Top),
 2778	assert_succ(roles,Env,MS,Top,PrimRole),
 2779	assert_succ(roles,Env,MS,Top,CT),
 2780	!.
 2781*/
 2782find_prole2(roles,Env,MS,PrimRole,CT) :-
 2783	CT = some(X,Y),
 2784	find_prole21(Env,MS,PrimRole,X,Y),
 2785	!.
 2786find_prole2(roles,Env,MS,PrimRole,CT) :-
 2787	CT = and([X|[R]]),
 2788	getRoleName(Env,MS,X),
 2789	R = not(Y),
 2790	getRoleName(Env,MS,Y),
 2791	find_prole23(Env,MS,X,Y,Top),
 2792	assert_succ(roles,Env,MS,Top,PrimRole),	
 2793	!.
 2794	
 2795find_prole2(roles,Env,MS,Primrole,CT) :-
 2796	CT = or([L|R]),
 2797	L = and(L1),
 2798	find_prole3(Env,MS,Primrole,R,L1,Z),
 2799	find_prole31(Env,MS,Primrole,Z),	
 2800	!.
 2801find_prole2(roles,Env,MS,Primrole,CT) :-
 2802	CT = or(L),
 2803	find_prole26(roles,Env,MS,Primrole,L),
 2804	!.
 2805
 2806find_prole21(Env,MS,PrimRole,X,Y) :-
 2807	Y = or([Y1|[Y2]]),
 2808	roleEqualSets(Env,user,MS,Role,some(X,Y1),_),
 2809	roleEqualSets(Env,user,MS,Role1,some(X,Y2),_),
 2810	find_prole23(Env,MS,Role,Role1,Top),
 2811	assert_succ(roles,Env,MS,Top,PrimRole),
 2812	!.
 2813
 2814find_prole23(Env,MS,X,Y,X) :-
 2815	sub(roles,Env,MS,X,Y),
 2816	!.
 2817find_prole23(Env,MS,X,Y,Y) :-
 2818	sub(roles,Env,MS,Y,X),
 2819	!.
 2820find_prole23(Env,MS,X,Y,Top) :-
 2821	sub(roles,Env,MS,Top,X),sub(roles,Env,MS,Top,Y).
 2822
 2823find_prole24(Env,MS,PrimRole,[]).
 2824find_prole24(Env,MS,PrimRole,[X|R]) :-
 2825	getRoleName(Env,MS,X),
 2826	assert1(sub(roles,Env,MS,X,PrimRole)),
 2827	direct_succ(roles,Env,MS,[],X,PrimRole,Z,L1),
 2828              contb(roles,Env,MS,Z,L1,PrimRole),
 2829	find_prole24(Env,MS,PrimRole,R),
 2830	!.
 2831
 2832find_prole26(roles,Env,MS,Primrole,[C1|R]) :-
 2833	convertMS(Env,[[],true],MS,[],[W1,G1],_),
 2834	call(G1),
 2835	getRoleName(Env,MS,C1),
 2836	subsume1(roles,Env,MS,C1,Primrole),
 2837	find_prole27(roles,Env,MS,Primrole,C1),
 2838  	find_prole26(roles,Env,MS,Primrole,R).
 2839
 2840find_prole27(roles,Env,MS,Primrole,C1):-
 2841	assert1(sub(roles,Env,MS,C1,Primrole)),
 2842	direct_succ(roles,Env,MS,[],C1,PrimRole,Z,L1),
 2843              contb(roles,Env,MS,Z,L1,Primrole),
 2844	!.
 2845
 2846find_prole3(Env,MS,Primrole,[],Z,Z) :- 
 2847	!.
 2848find_prole3(Env,MS,Primrole,[L|R],Z,K) :-
 2849	L = and(L1),
 2850	intersection_motel(Z,L1,Z1),
 2851	find_prole3(Env,MS,Primrole,R,Z1,K),
 2852	!.
 2853
 2854find_prole31(Env,MS,Primrole,[]) :-
 2855	!.
 2856find_prole31(Env,MS,Primrole,[L1|R1]) :-
 2857	find_prole27(roles,Env,MS,Primrole,L1),
 2858	find_prole31(Env,MS,Primrole,R1),
 2859	!.
 2860
 2861/****************************************************************/
 2862
 2863make_succ(MS) :-           
 2864	currentEnvironment(Env),            
 2865              not(make_succ(concepts,Env,MS)),
 2866	not(make_succ(roles,Env,MS)),!.
 2867make_succ(concepts,Env,MS) :-        
 2868	getConceptName(Env,MS,NewConcept),
 2869	ifOption(testOutput,yes,(print(NewConcept),nl)),
 2870	make_succ2(concepts,Env,MS,NewConcept),
 2871	fail.
 2872make_succ(roles,Env,MS) :-
 2873	getRoleName(Env,MS,NewRole),
 2874	ifOption(testOutput,yes,(print(NewRole),nl)),
 2875	make_succ2(roles,Env,MS,NewRole),
 2876       	fail.
 2877make_succ2(Type,Env,MS,NewConcept) :- 
 2878              NewConcept \== 'top',!,
 2879              NewConcept \== 'bot',!,
 2880              direct_succ(Type,Env,MS,[],'top',NewConcept,X,L),
 2881              contb(Type,Env,MS,X,L,NewConcept),
 2882              !.
 2883
 2884contb(Type,Env,MS,[],L,NewConcept) :- 
 2885        !.
 2886
 2887contb(Type,Env,MS,[X|R],L,NewConcept) :-
 2888        setofOrNil(Y,contc(Type,Env,MS,X,Y,L),L1),
 2889	list_to_set(L1,L2),
 2890        make_succ1(Type,Env,MS,X,L2,NewConcept),
 2891        !,
 2892        contb(Type,Env,MS,R,L,NewConcept).
 2893contb(Type,Env,MS,X,L,NewConcept) :-
 2894	list_to_set(L,L1),	
 2895        make_succ1(Type,Env,MS,X,L1,NewConcept),
 2896        !.
 2897
 2898contc(Type,Env,MS,X,Y,L) :-
 2899        sub(Type,Env,MS,X,Y),member(Y,L).
 2900
 2901direct_succ(Type,Env,MS,_Done,'bot',X,_,[]) :- fail.
 2902direct_succ(Type,Env,MS,Done,X,NewConcept,Z,L1) :-
 2903	subsume1(Type,Env,MS,X,NewConcept),
 2904	setofOrNil(Y,(succ1(Type,Env,MS,X,Y), not(member(Y,[X|Done]))),L),
 2905	!,
 2906	check(Type,Env,MS,[X|Done],L,_,X,NewConcept,Z,L1),
 2907	!.
 2908direct_succ(Type,Env,MS,_Done,X,NewConcept,X,[]) :- 
 2909	!.
 2910
 2911check(Type,Env,MS,Done,[Y|L],_L1,X,NewConcept,Z,L1) :-
 2912        subsume1(Type,Env,MS,Y,NewConcept),
 2913	!,
 2914        direct_succ(Type,Env,MS,Done,Y,NewConcept,Z1,L10),
 2915	!,        	 				 	 	
 2916	conta(Type,Env,MS,[Y|Done],L,L2,X,NewConcept,Z1,L10,Z,L1),
 2917        !.
 2918check(Type,Env,MS,Done,[Y|L],L2,X,NewConcept,Z,L1) :-
 2919	!,
 2920	check(Type,Env,MS,[Y|Done],L,[Y|L2],X,NewConcept,Z,L1).
 2921check(Type,Env,MS,Done,[],L2,X,NewConcept,X,L1) :-
 2922	check1(Type,Env,MS,Done,L2,NewConcept,L1),
 2923	!.
 2924
 2925conta(Type,Env,MS,_Done,[],L2,X,NewConcept,Z1,L10,Z1,L10) :-
 2926        !.
 2927conta(Type,Env,MS,Done,L,L2,X,NewConcept,Z1,L10,Z,L1) :-
 2928        check(Type,Env,MS,Done,L,L2,X,NewConcept,Z2,L11),
 2929 	union1(Z1,Z2,Za),delete1(Za,'top',Z),
 2930	union1(L10,L11,L1),
 2931        !.
 2932check1(_,_,_,_,[],_,[]) :- !.
 2933check1(Type,Env,MS,Done,[Y|L],NewConcept,[Y|L1]) :-
 2934	subsume1(Type,Env,MS,NewConcept,Y),
 2935	!,
 2936	check1(Type,Env,MS,[Y|Done],L,NewConcept,L1).
 2937check1(Type,Env,MS,Done,[Y|L],NewConcept,L1) :-
 2938	not(member(Y,Done)),
 2939	setofOrNil(Z,succ1(Type,Env,MS,Y,Z),L2),
 2940	check1(Type,Env,MS,[Y|Done],L2,NewConcept,L3),
 2941	check1(Type,Env,MS,[Y|Done],L,NewConcept,L4),
 2942	motel_union(L3,L4,L5),
 2943	deleteInList(L5,'top',L1),
 2944	!.
 2945check1(Type,Env,MS,Done,[Y|L],NewConcept,L1) :-
 2946	check1(Type,Env,MS,[Y|Done],L,NewConcept,L1),
 2947	!.
 2948
 2949make_succ1(Type,Env,MS,X,[Y|L],NewConcept) :- 
 2950	not(succ(Type,Env,MS,NewConcept,Y)),
 2951        retract1(succ(Type,Env,MS,X,Y)),
 2952%	assert1(succ(Type,Env,MS,NewConcept,Y)),
 2953        assert_succ(Type,Env,MS,NewConcept,Y),
 2954	!,
 2955	make_succ1(Type,Env,MS,X,L,NewConcept). 
 2956make_succ1(Type,Env,MS,X,[Y|L],NewConcept) :- 
 2957% 	assert1(succ(Type,Env,MS,x,NewConcept)),
 2958        assert_succ(Type,Env,MS,X,NewConcept),
 2959	!,
 2960	make_succ1(Type,Env,MS,X,L,NewConcept).
 2961make_succ1(Type,Env,MS,X,[],NewConcept) :- 
 2962%	assert1(succ(Type,Env,MS,X,NewConcept)),
 2963        assert_succ(Type,Env,MS,X,NewConcept),
 2964	!.
 2965
 2966
 2967/****************  practical funktions ******************************/	
 2968
 2969subsume1(Type,Env,MS,X,Y) :- var(X),!,fail.
 2970subsume1(Type,Env,MS,X,Y) :- var(Y),!,fail.
 2971subsume1(Type,Env,MS,X,'top') :- !,fail.
 2972subsume1(Type,Env,MS,'bot',X) :- !,fail.
 2973subsume1(Type,Env,MS,X,[]) :- !.
 2974subsume1(Type,Env,MS,X,'bot') :- !.
 2975subsume1(Type,Env,MS,'top',X) :- !.
 2976subsume1(Type,Env,MS,X,Y) :- 
 2977	sub(Type,Env,MS,X,Y),
 2978	!.
 2979subsume1(Type,Env,MS,X,Y) :- 
 2980	nsub(Type,Env,MS,X,Y),
 2981	!,
 2982	fail. 
 2983subsume1(Type,Env,MS,X,Y) :- 
 2984	X \== Y,
 2985	addCounter(Type,1),
 2986	subsumes(Type,Env,MS,X,Y), 
 2987	cont(Type,Env,MS,[],X,Y),
 2988	!.
 2989subsume1(Type,Env,MS,X,Y) :- 
 2990	X \== Y,
 2991	cont1a(Type,Env,MS,[],X,Y),
 2992	!,
 2993	fail.
 2994
 2995cont(Type,Env,MS,_,'top',Y).
 2996cont(Type,Env,MS,Done,X,Y) :- 
 2997	assert1(sub(Type,Env,MS,X,Y)),
 2998	succ1(Type,Env,MS,Z,X),
 2999	not(member(Z,Done)),
 3000	cont(Type,Env,MS,[Z|Done],Z,Y),!.
 3001cont(Type,Env,MS,_,X,Y). 
 3002cont1a(Type,Env,MS,_,'bot',X) :- 
 3003	!.
 3004cont1a(Type,Env,MS,_,X,'bot') :- 
 3005	!,fail.
 3006cont1a(Type,Env,MS,Done,X,Y) :-
 3007       member(X,Done), 
 3008       !.
 3009cont1a(Type,Env,MS,Done,X,Y) :-
 3010	assert1(nsub(Type,Env,MS,X,Y)),
 3011	succ1(Type,Env,MS,X,Z),
 3012	cont1a(Type,Env,MS,[X|Done],Z,Y),
 3013	!.
 3014
 3015delete1([X|R],'top',Z) :-
 3016	deleteInList([X|R],'top',Z),
 3017	!.
 3018delete1(X,'top',Z) :-
 3019	!.
 3020
 3021union1([],[],[]).
 3022union1([X|R],[Y|R1],Z):-
 3023	motel_union([X|R],[Y|R1],Z),
 3024	!.
 3025union1([X|R],Y,Z) :-
 3026	motel_union([X|R],[Y],Z),
 3027	!.
 3028union1([X],Y,Z) :-
 3029	motel_union([X],[Y],Z),
 3030	!.
 3031union1(X,[Y],Z) :-
 3032	motel_union([X],[Y],Z),
 3033	!.
 3034union1(X,[Y|R],Z) :-
 3035	motel_union([X],[Y|R],Z),
 3036	!.
 3037union1(X,Y,Z) :-
 3038	motel_union([X],[Y],Z),
 3039	!.
 3040
 3041assert1(G) :- 
 3042	\+ (G),
 3043	assert_logged(G),
 3044	!.
 3045assert1(G) :-
 3046	!.
 3047% assert_succ wurde wegen eines Fehlers in direct_succ(bzw conta) veraendert
 3048% duerfte an der Laufzeit nicht sehr viel ausmachen,ging auch einfacher
 3049% als den Fehler zu finden...
 3050
 3051assert_succ(Type,Env,MS,X,X) :-
 3052	!.
 3053/*
 3054assert_succ(Type,Env,MS,X,RorC) :-
 3055	assert1(succ(Type,Env,MS,X,RorC)),
 3056	cont(Type,Env,MS,[],X,RorC),
 3057	!.
 3058*/
 3059assert_succ(Type,Env,MS,X,RorC) :-
 3060	cont(Type,Env,MS,[],X,RorC),
 3061	not((sub(Type,Env,MS,X,Y),not(var(Y)),sub(Type,Env,MS,Y,RorC),Y \== RorC)),
 3062	assert1(succ(Type,Env,MS,X,RorC)),
 3063	!.
 3064assert_succ(Type,Env,MS,X,RorC).
 3065
 3066
 3067retract1(G) :- 
 3068	retract(G),
 3069	!.
 3070retract1(G) :- 
 3071	!.
 3072
 3073succ1(Type,Env,MS,X,Y) :- 
 3074	succ(Type,Env,MS,X,Y).
 3075%	!.
 3076succ1(Type,Env,MS,X,'bot').
 3077% 	:-  !.
 3078
 3079/*****************************************************************************/
 3080/***************** print and statistic - functions ***************************/
 3081newShowHierarchy :-
 3082	show_dag.
 3083
 3084show_dag :-
 3085	currentEnvironment(Env),
 3086	show_dag(Env,[]).
 3087show_dag(MS) :-
 3088	currentEnvironment(Env),
 3089	show_dag(Env,MS).
 3090show_dag(Env,MS) :-
 3091	!,
 3092	print('Concepts'),nl,
 3093        not(show_dag(concepts,Env,MS,'top',[])),nl,nl,
 3094	print('Roles'),nl,
 3095	not(show_dag(roles,Env,MS,'top',[])).
 3096show_dag(Type,Env,MS,'bot',_) :- !,fail.
 3097show_dag(Type,Env,MS,Node,L) :-
 3098	writes(L),
 3099	print(Node),nl,
 3100	succ(Type,Env,MS,Node,N),
 3101  	show_dag(Type,Env,MS,N,[45|L]),
 3102	fail.
 3103
 3104initStat :-
 3105	!,
 3106	setCounter(subsumptionTests,0),
 3107	setCounter(concepts,0),
 3108	setCounter(roles,0),
 3109	setCounter(conceptsClassified,0),
 3110	setCounter(rolesClassified,0),
 3111	getRuntime(T0),
 3112	setCounter(runtime,T0),
 3113	!.
 3114getStat(CN,CST,RN,RST,T) :-
 3115	!,
 3116	getRuntime(T1),
 3117	getCounter(subsumptionTests,ST),
 3118	getCounter(concepts,CST),
 3119	getCounter(conceptsClassified,CN),
 3120	getCounter(roles,RST),
 3121	getCounter(rolesClassified,RN),
 3122	getCounter(runtime,T0),
 3123	T is T1 - T0,
 3124	!.
 3125printStat :-
 3126	!,
 3127	getStat(CN,CST,RN,RST,T),
 3128	format('Concepts classified:         ~d~n',CN),
 3129	format('Subsumption tests performed: ~d~n',CST),
 3130	format('Roles    classified:         ~d~n',RN),
 3131	format('Subsumption tests performed: ~d~n',RST),
 3132	format('Total runtime:               ~3d sec.~2n',T),
 3133	!.
 3134
 3135buildOrdering(Env,MS,CTree,RTree) :- 
 3136	buildOrdering(concepts,Env,MS,'top',[],CTree),
 3137	buildOrdering(roles,Env,MS,'top',[],RTree),
 3138	!.
 3139
 3140
 3141buildOrdering(Type,Env,MS,'bot',Done,node(['bot'|EquivClass],[])) :-
 3142	!,
 3143	setofOrNil(Z2,(succ(Type,Env,MS,'bot',Z2),succ(Type,Env,MS,Z2,'bot')),EquivClass),
 3144	!.
 3145buildOrdering(Type,Env,MS,Concept1,Done,node([Concept1|EquivClass],SubtreeList)) :-
 3146	setofOrNil(Z1,succ(Type,Env,MS,Concept1,Z1),S1),
 3147	setofOrNil(Z2,(succ(Type,Env,MS,Concept1,Z2),succ(Type,Env,MS,Z2,Concept1)),EquivClass),
 3148	successorSet(S1,EquivClass,Succ),
 3149	append(Done,[Concept1|EquivClass],Done1),
 3150	buildOrderingList(Type,Env,MS,Succ,Done1,SubtreeList).
 3151
 3152buildOrderingList(_Type,_Env,_MS,[],_Done,[]) :-
 3153	!.
 3154buildOrderingList(Type,Env,MS,[C1|CL],Done,SubtreeList) :-
 3155	member(C1,Done),
 3156	!,
 3157	buildOrderingList(Type,Env,MS,CL,Done,SubtreeList).
 3158buildOrderingList(Type,Env,MS,[C1|CL],Done,[Subtree|SubtreeList]) :-
 3159	buildOrdering(Type,Env,MS,C1,Done,Subtree),
 3160	buildOrderingList(Type,Env,MS,CL,Done,SubtreeList),
 3161	!.
 3162
 3163successorSet(S1,EquivClass,S2) :-
 3164	successor_set(S1,EquivClass,S3),
 3165	((S3 \== [], S2 = S3) ; (S2 = ['bot'])),
 3166	!.
 3167
 3168successor_set([],_,[]) :-
 3169	!.
 3170successor_set([C1|CL],EquivClass,S2) :-
 3171	member(C1,EquivClass),
 3172	!,
 3173	successor_set(CL,EquivClass,S2).
 3174successor_set(['bot'|CL],EquivClass,S2) :-
 3175	!,
 3176	successor_set(CL,EquivClass,S2).
 3177successor_set([C1|CL],EquivClass,[C1|S2]) :-
 3178	successor_set(CL,EquivClass,S2).
 3179/**********************************************************************
 3180 *
 3181 * @(#) compileEnv.pl 1.9@(#)
 3182 *
 3183 */
 3184
 3185/**********************************************************************
 3186 *
 3187 * compileEnvironment(FileName)
 3188 * 
 3189 */
 3190
 3191compileEnvironment(FileName) :-
 3192	see(FileName),
 3193	read(environment(EnvName,_Env,_Comment)),
 3194	seen,
 3195	compileEnvironment(FileName,EnvName),
 3196	!.
 3197compileEnvironment(FileName) :-
 3198	% Some file handling error has occured
 3199	seen,
 3200	!, 
 3201	fail.
 3202
 3203compileEnvironment(FileName,EnvName) :-
 3204	see(FileName),
 3205	read(environment(_EnvName,Env,Comment)),
 3206	(removeEnvironment(EnvName) ; true),
 3207	termExpansion(on,Env,CPList),
 3208	tell('/tmp/compile.tmp'),
 3209	write((:- dynamic(constraint/8))), write('.'), nl,
 3210	write((:- dynamic(numb/1))), write('.'), nl,
 3211%	write((:- dynamic(in/9))), write('.'), nl,
 3212%	write((:- dynamic(kb_in/10))), write('.'), nl,
 3213	write((:- dynamic(falsum/2))), write('.'), nl,
 3214%	write((:- dynamic(conceptName/4))), write('.'), nl,
 3215%	write((:- dynamic(roleName/4))), write('.'), nl,
 3216%	write((:- dynamic(conceptEqualSets/6))), write('.'), nl,
 3217	write((:- dynamic(conceptSubsets/6))), write('.'), nl,
 3218%	write((:- dynamic(eq/9))), write('.'), nl,
 3219	write((:- dynamic(inconsistencyCheck/3))), write('.'), nl,
 3220	write((:- dynamic(roleEqualSets/6))), write('.'), nl,
 3221	write((:- dynamic(roleSubsets/6))), write('.'), nl,
 3222	write((:- dynamic(conceptElement/7))), write('.'), nl,
 3223	write((:- dynamic(roleElement/8))), write('.'), nl,
 3224	write((:- dynamic(closed/5))), write('.'), nl,
 3225	write((:- dynamic(sub/5))), write('.'), nl,
 3226	write((:- dynamic(succ/5))), write('.'), nl,
 3227	write((:- dynamic(nsub/5))), write('.'), nl,
 3228	write((:- dynamic(sub3/2))), write('.'), nl,
 3229	write((:- dynamic(succ3/2))), write('.'), nl,
 3230	write((:- dynamic(nsub3/2))), write('.'), nl,
 3231	write((:- dynamic(abductiveDerivation/3))), write('.'), nl,
 3232	write((:- dynamic(consistencyDerivation/3))), write('.'), nl,
 3233	write((:- dynamic(hypothesis/1))), write('.'), nl,
 3234	write((:- dynamic(roleDomain/4))), write('.'), nl,
 3235	write((:- dynamic(roleRange/4))), write('.'), nl,
 3236	write((:- dynamic(roleDefault/4))), write('.'), nl,
 3237	write((:- dynamic(roleNr/4))), write('.'), nl,
 3238	write((:- dynamic(roleDefNr/4))), write('.'), nl,
 3239	write((:- dynamic(roleAttributes/5))), write('.'), nl,
 3240%	write((:- dynamic(given_inflLink/4))), write('.'), nl,
 3241%	write((:- dynamic(given_change/4))), write('.'), nl,
 3242%       write((:- dynamic(value/2))), write('.'), nl,
 3243	write((:- dynamic(motel_option/2))), write('.'), nl,
 3244%	write((:- dynamic(environment/3))), write('.'), nl,
 3245%	write((:- dynamic(conceptHierarchy/3))), write('.'), nl,
 3246%	write((:- dynamic(roleHierarchy/3))), write('.'), nl,
 3247	write((:- dynamic(modalAxiom/6))), write('.'), nl,
 3248%	write((:- dynamic(rel/5))), write('.'), nl,
 3249	write((:- dynamic(compiledPredicate/2))), write('.'), nl,
 3250	writeq((:- asserta_logged(environment(EnvName,Env,Comment)))), write('.'), nl,
 3251	writeq((:- retractall_head(currentEnvironment(_)))), write('.'), nl,
 3252	writeq((:- asserta_logged(currentEnvironment(Env)))), write('.'), nl,
 3253	writeCompiledPredicateFactsToFile(Env,CPList),
 3254	expand_term((in(Env,Name,modal(MS),CN,CON,hyp(HYP),
 3255                        ab(D),call(CALL),PT) :-
 3256	                   kb_in(Env,pr(5),Name,modal(MS),CN,CON,hyp(HYP),
 3257                                 ab(D),call(CALL),PT)),
 3258		    InClause1),
 3259	writeq(InClause1), write('.'), nl,
 3260	expand_term((in(Env,Name,modal(MS),CN,CON,
 3261                        hyp([or(H1),rl(H2),fl(H3)]),ab(noAb),call(CALL),PT) :-
 3262		           clashInHyp(H2), !, fail),
 3263		    InClause2),
 3264	writeq(InClause2), write('.'), nl,
 3265	expand_term(in(Env,X2,X3,X4,X5,X6,X7,X8,X9), Head3),
 3266	writeq((Head3 :- kb_in(Env,pr(3),X2,X3,X4,X5,X6,X7,X8,X9))),
 3267	write('.'), nl,
 3268	expand_term((in(Env,Name,modal(MS),CN,CON,hyp(HYP),
 3269                        ab(D),call(CALL),PT) :-
 3270		          (CN \== 'top', CN \== 'bot', CN \== not('top'), 
 3271                           CN \== not('bot'),
 3272	                   kb_in(Env,pr(3),Name,modal(MS),CN,CON,hyp(HYP),
 3273                                 ab(D),call(CALL),PT))),
 3274		    InClause4),
 3275	writeq(InClause4), write('.'), nl,
 3276	expand_term((in(Env,Name,modal(MS),CN,CON,hyp(HYP),
 3277                        ab(D),call(CALL),PT) :-
 3278		          (CN \== 'top',CN \== 'bot', CN \== not('top'), 
 3279                           CN \== not('bot'),
 3280			   kb_in(Env,pr(1),Name,modal(MS),CN,CON,hyp(HYP),
 3281				 ab(D),call(CALL),PT))),
 3282		    InClause5),
 3283	writeq(InClause5), write('.'), nl,
 3284	repeat,
 3285	read(Clause),
 3286	treatClause(Clause),
 3287	seen,
 3288	told,
 3289	assertConnectionClauses(Env),
 3290	termExpansion(off,Env),
 3291	compile('/tmp/compile.tmp'),
 3292	!.
 3293compileEnvironment(FileName,EnvName) :-
 3294	% Some file handling error has occured
 3295	seen,
 3296	told,
 3297	!,
 3298	fail.
 3299
 3300treatClause('end_of_file') :-
 3301	!.
 3302treatClause((:-dynamic Pred/Arity)) :-
 3303%	write((:-dynamic Pred/Arity)), write('.'), nl,
 3304	!,
 3305	fail.
 3306treatClause((in(_X1,_X2,_X3,_X4,_X5,_X6,_X7,_X8,_X9) :- _Body)) :-
 3307	!,
 3308	fail.
 3309treatClause(X) :-
 3310	expand_term(X,Y),
 3311	writeq(Y), write('.'), nl,
 3312	!,
 3313	fail.
 3314
 3315writeCompiledPredicateFactsToFile(Env,[]) :-
 3316	!.
 3317writeCompiledPredicateFactsToFile(Env,[Pred/Arity|List]) :-
 3318	writeq((compiledPredicate(Env,Pred/Arity))),
 3319	write('.'), nl,
 3320	writeCompiledPredicateFactsToFile(Env,List).
 3321
 3322assertConnectionClauses(Env) :-
 3323	expand_term(constraint(Env,X2,X3,X4,X5,X6,X7,X8),CompConAtom),
 3324	assertz_logged((constraint(Env,X2,X3,X4,X5,X6,X7,X8) :-
 3325		 CompConAtom)),
 3326	expand_term(eq(Env,X2,X3,X4,X5,X6,X7,X8,X9),CompEqAtom),
 3327	assertz_logged((eq(Env,X2,X3,X4,X5,X6,X7,X8,X9) :-
 3328		 CompEqAtom)),
 3329	expand_term(in(Env,X2,X3,X4,X5,X6,X7,X8,X9),CompInAtom),
 3330	assertz_logged((in(Env,X2,X3,X4,X5,X6,X7,X8,X9) :-
 3331		 CompInAtom)),
 3332%	assertz_logged((kb_in(Env,X2,X3,X4,X5,X6,X7,X8,X9,X10) :-
 3333%		 comp_kb_in(Env,X2,X3,X4,X5,X6,X7,X8,X9,X10))),
 3334	expand_term(rel(Env,X2,X3,X4,X5),CompRelAtom),
 3335	assertz_logged((rel(Env,X2,X3,X4,X5) :-
 3336		 CompRelAtom)),
 3337	!.
 3338
 3339termExpansion(on,env(Id),
 3340              [CompCon/8,CompEq/9,CompIn/9,CompKb_in/10,CompRel/6]) :-
 3341	% Generate the names for the compiled in, kb_in, constraint, and rel
 3342	% predicates in environment Id.
 3343	name(Id,IdChars),
 3344	name(in,InChars),
 3345	append(InChars,[95,99,95|IdChars],CompInChars),
 3346	name(CompIn,CompInChars),
 3347	name(constraint,ConChars),
 3348	append(ConChars,[95,99,95|IdChars],CompConChars),
 3349	name(CompCon,CompConChars),
 3350	name(eq,EqChars),
 3351	append(EqChars,[95,99,95|IdChars],CompEqChars),
 3352	name(CompEq,CompEqChars),
 3353	name('kb_in',Kb_inChars),
 3354	append(Kb_inChars,[95,99,95|IdChars],CompKb_inChars),
 3355	name(CompKb_in,CompKb_inChars),
 3356	name('rel',RelChars),
 3357	append(RelChars,[95,99,95|IdChars],CompRelChars),
 3358	name(CompRel,CompRelChars),
 3359	% Abolish any previously asserted clauses for the 
 3360	% compiled predicades
 3361	abolish(CompCon/8),
 3362	abolish(CompEq/9),
 3363	abolish(CompIn/9),
 3364	abolish(CompKb_in/10),
 3365	abolish(CompRel/6),
 3366	% Generate the atoms for these predicates 
 3367	CompConAtom =.. [CompCon|[X4,X1,X2,X3,X5,X6,X7,X8]],
 3368	CompEqAtom =.. [CompEq|[X4-X5,X1,X2,X3,X6,X7,X8,X9]],
 3369	CompInAtom =.. [CompIn|[X4-X5,X1,X2,X3,X6,X7,X8,X9]],
 3370	CompKb_inAtom =.. [CompKb_in|[X5-X6,X1,X2,X3,X4,X7,X8,X9,X10]],
 3371	CompRelAtom =.. [CompRel|[X1,X2,X3,X4,X5,X6]],
 3372	% Assert the term_expansion rules needed to translate the
 3373	% interpreted clauses into compiled clauses.
 3374	abolish(term_expansion/2),
 3375	assertz_logged((term_expansion((Head :- Body),(Head1 :- Body1)) :-
 3376	term_expansion(Head,Head1),
 3377	term_expansion(Body,Body1))),
 3378	assertz_logged((term_expansion((L, Body), (L1,Body1)) :-
 3379	term_expansion(L,L1),
 3380	term_expansion(Body,Body1))),
 3381	assertz_logged((term_expansion((L; Body), (L1,Body1)) :-
 3382	term_expansion(L,L1),
 3383	term_expansion(Body,Body1))),
 3384	assertz_logged((term_expansion(\+Atom,\+Atom1) :-
 3385	term_expansion(Atom,Atom1))),
 3386	assertz_logged((term_expansion(constraint(X1,X2,X3,X4,X5,X6,X7,X8),
 3387				CompConAtom))),
 3388	assertz_logged((term_expansion(eq(X1,X2,X3,X4,X5,X6,X7,X8,X9),
 3389				CompEqAtom))),
 3390	assertz_logged((term_expansion(in(X1,X2,X3,X4,X5,X6,X7,X8,X9),
 3391				CompInAtom))),
 3392	assertz_logged((term_expansion(kb_in(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),
 3393				CompKb_inAtom))),
 3394	assertz_logged((term_expansion(rel(X1,X2,X3,X4,X5),
 3395				CompRelAtom))),
 3396	assertz_logged((term_expansion(once(Body1),once(Body2)) :-
 3397		term_expansion(Body1,Body2))),
 3398	assertz_logged((term_expansion(call(Body1),call(Body2)) :-
 3399		 term_expansion(Body1,Body2))),
 3400	assertz_logged(term_expansion(X,X)),
 3401	!.
 3402termExpansion(off,_) :-
 3403	abolish(term_expansion/2),
 3404	!.
 3405
 3406/**********************************************************************
 3407 *
 3408 * @(#) cnf.pl 1.2@(#)
 3409 *
 3410 */
 3411
 3412/***********************************************************************
 3413 *
 3414 * negate(+C1,-C2)
 3415 * C2 is just the term not(C1).
 3416 *
 3417 */
 3418
 3419negate(not(C1),C1) :- !.
 3420negate(C1,not(C1)) :- !.
 3421
 3422/***********************************************************************
 3423 *
 3424 * invert(+R1,-R2)
 3425 * R2 is just the term inverse(R1).
 3426 *
 3427 */
 3428
 3429invert(inverse(R),R) :- !.
 3430invert(R,inverse(R)) :- !.
 3431
 3432/***********************************************************************
 3433 *
 3434 * normalizeNot(+C1,-C2)
 3435 * applies the laws
 3436 *      not(and([A,B]))   -> and([not(A),not(B)])
 3437 *      not(or([A,B]))    -> or([not(A),not(B)])
 3438 *      not(not(A))       -> A
 3439 *      not(all(R,C))     -> some(R,not(C))
 3440 *      not(some(R,C))    -> all(R,not(C))
 3441 *      not(atleast(N,R)) -> atmost(N-1,R)
 3442 *      not(atmost(N,R))  -> atleast(N+1,R)
 3443 *      not(b(O,P,C))     -> d(O,P,not(C))
 3444 *      not(d(O,P,C))     -> b(O,P,not(C))
 3445 * to C1 as long as possible to get C2.
 3446 *
 3447 */
 3448
 3449normalizeNot(not(and([C1,C2|L1])),or(L3)) :-
 3450	!,
 3451	hop_map(negate,[C1,C2|L1],L2),
 3452	hop_map(normalizeNot,L2,L3).
 3453normalizeNot(not(and([C1])),C2) :-
 3454	negate(C1,C2).
 3455normalizeNot(not(and([])),'bot') :-
 3456	!.
 3457normalizeNot(not(set(L)),not(set(L))) :-
 3458	!.
 3459normalizeNot(not(or([C1,C2|L1])),and(L3)) :-
 3460	!,
 3461	hop_map(negate,[C1,C2|L1],L2),
 3462	hop_map(normalizeNot,L2,L3).
 3463normalizeNot(not(or([C1])),C2) :-
 3464	negate(C1,C2).
 3465normalizeNot(not(or([])),'top') :-
 3466	!.
 3467normalizeNot(not(all(R,C1)),some(R,C2)) :-
 3468	normalizeNot(not(C1),C2).
 3469normalizeNot(not(some(R,C1)),all(R,C2)) :-
 3470	normalizeNot(not(C1),C2).
 3471normalizeNot(not(atleast(N,R)),atmost(M,R)) :-
 3472	M is N-1.
 3473normalizeNot(not(atmost(N,R)),atleast(M,R)) :-
 3474	M is N+1.
 3475normalizeNot(not(b(O,P,C1)),d(O,P,C2)) :-
 3476	normalizeNot(not(C1),C2).
 3477normalizeNot(not(d(O,P,C1)),b(O,P,C2)) :-
 3478	normalizeNot(not(C1),C2).
 3479normalizeNot(not(bc(O,P,C1)),dc(O,P,C2)) :-
 3480	normalizeNot(not(C1),C2).
 3481normalizeNot(not(dc(O,P,C1)),bc(O,P,C2)) :-
 3482	normalizeNot(not(C1),C2).
 3483normalizeNot(not(b(O,P)),d(O,P)) :-
 3484	!.
 3485normalizeNot(not(d(O,P)),b(O,P)) :-
 3486	!.
 3487normalizeNot(not(bc(O,P)),dc(O,P)) :-
 3488	!.
 3489normalizeNot(not(dc(O,P)),bc(O,P)) :-
 3490	!.
 3491normalizeNot(not(not(C1)),C3) :-
 3492	normalizeNot(C1,C3).
 3493normalizeNot(not(set([])),'top') :- !.
 3494normalizeNot(C1,C1).
 3495
 3496/***********************************************************************
 3497 *
 3498 * normalizeInverse(+R1,-R2)
 3499 * applies the laws
 3500 *      inverse(and([R,S])) -> and([inverse(R),inverse(S)])
 3501 *      inverse(inverse(R)) -> R
 3502 * to R1 as long as possible to get R2.
 3503 *
 3504 */
 3505
 3506normalizeInverse(inverse(and(RL1)),and(RL3)) :-
 3507	hop_map(invert,RL1,RL2),
 3508	hop_map(normalizeInverse,RL2,RL3),
 3509	!.
 3510normalizeInverse(inverse(inverse(R1)),R3) :-
 3511	normalizeInverse(R1,R3).
 3512normalizeInverse(R1,R1).
 3513
 3514/***********************************************************************
 3515 *
 3516 * motel_flatten(+C1,-C2)
 3517 * deletes unnecessary occurrences of `and' and `or' in C1 to get C2.
 3518 *
 3519 */
 3520
 3521motel_flatten(and(L1),and(L2)) :-
 3522	!,
 3523	hop_map(motel_flatten,L1,L3),
 3524	flattenAnd([],L3,L2).
 3525motel_flatten(or(L1),or(L2)) :-
 3526	!,
 3527	hop_map(motel_flatten,L1,L3),
 3528	flattenOr([],L3,L2).
 3529motel_flatten(set(L1),set(L1)) :-
 3530	!.
 3531motel_flatten(all(R1,C1),all(R2,C2)) :-
 3532	motel_flatten(R1,R2),
 3533	motel_flatten(C1,C2).
 3534motel_flatten(some(R1,C1),some(R2,C2)) :-
 3535	motel_flatten(R1,R2),
 3536	motel_flatten(C1,C2).
 3537motel_flatten(atleast(N,R1),atleast(N,R2)) :-
 3538	motel_flatten(R1,R2).
 3539motel_flatten(atmost(N,R1),atmost(N,R2)) :-
 3540	motel_flatten(R1,R2).
 3541motel_flatten(b(O,P,C1),b(O,P,C2)) :-
 3542	motel_flatten(C1,C2).
 3543motel_flatten(d(O,P,C1),d(O,P,C2)) :-
 3544	motel_flatten(C1,C2).
 3545motel_flatten(bc(O,P,C1),bc(O,P1,C2)) :-
 3546	motel_flatten(P,P1),
 3547	motel_flatten(C1,C2).
 3548motel_flatten(dc(O,P,C1),dc(O,P1,C2)) :-
 3549	motel_flatten(P,P1),
 3550	motel_flatten(C1,C2).
 3551motel_flatten(not(C1),not(C2)) :-
 3552	!,
 3553	motel_flatten(C1,C2).
 3554motel_flatten(inverse(R1),inverse(R2)) :-
 3555	motel_flatten(R1,R2).
 3556motel_flatten(C1,C1).
 3557
 3558
 3559/***********************************************************************
 3560 *
 3561 * flattenAnd(+L1,+L2,-L3)
 3562 * eliminates occurrences of `and' in L2 to get L2'. L3 is the result
 3563 * of appending L2' to L1.
 3564 *
 3565 */
 3566
 3567flattenAnd(L1,[and(L2)|L3],L4) :-
 3568	!,
 3569%	flattenAnd([],L2,L5),
 3570	L5 = L2,
 3571	append(L1,L5,L6),
 3572	flattenAnd(L6,L3,L4).
 3573flattenAnd(L1,[C1|L3],L4) :-
 3574	append(L1,[C1],L6),
 3575	flattenAnd(L6,L3,L4).
 3576flattenAnd(L1,[],L1).
 3577
 3578/***********************************************************************
 3579 *
 3580 * flattenOr(+L1,+L2,-L3)
 3581 * eliminates occurrences of `or' in L2 to get L2'. L3 is the result
 3582 * of appending L2' to L1.
 3583 *
 3584 */
 3585 
 3586flattenOr(L1,[or(L2)|L3],L4) :-
 3587	!,
 3588%	flattenOr([],L2,L5),
 3589	L5 = L2,
 3590	append(L1,L5,L6),
 3591	flattenOr(L6,L3,L4).
 3592flattenOr(L1,[C1|L3],L4) :-
 3593	append(L1,[C1],L6),
 3594	flattenOr(L6,L3,L4).
 3595flattenOr(L1,[],L1).
 3596
 3597/***********************************************************************
 3598 *
 3599 * distributeAnd(and(+L1),or(+L2),or(-L3))
 3600 * here or(L3) has the form
 3601 *     or([C_1,...,C_n])
 3602 * where C_i is the result of applying de Morgan's laws to
 3603 * and(L1|[A_i]) 
 3604 * where A_i is the ith element of L2.
 3605 *
 3606 */
 3607
 3608distributeAnd(and(L1),or([C2|L2]),or([C3|L4])) :-
 3609	% L3 := L1 and C2
 3610	append(L1,[C2],L3),
 3611	% C3 := deMorganAnd(L3)
 3612	deMorgan(and(L3),C3),
 3613	% build other disjuncts
 3614	distributeAnd(and(L1),or(L2),or(L4)).
 3615distributeAnd(and(_L1),or([]),or([])).
 3616
 3617/***********************************************************************
 3618 *
 3619 * distributeOr(or(+L1),and(+L2),and(-L3))
 3620 * here and(L3) has the form
 3621 *     and([C_1,...,C_n])
 3622 * where C_i is the result of applying de Morgan's laws to
 3623 * or(L1|[A_i]) 
 3624 * where A_i is the ith element of L2.
 3625 *
 3626 */
 3627	
 3628distributeOr(or(L1),and([C2|L2]),and([C3|L4])) :-
 3629	% L3 := L1 or C2
 3630	append(L1,[C2],L3),
 3631	% C3 := deMorgan(L3)
 3632	deMorgan(or(L3),C3),
 3633	% build other conjuncts
 3634	distributeOr(or(L1),and(L2),and(L4)).
 3635distributeOr(or(_L1),and([]),and([])).
 3636	
 3637/***********************************************************************
 3638 *
 3639 * deMorganAnd(+L1,+L2,-C1)
 3640 * applies de Morgan's law
 3641 *      and([A,or([B,C])]) -> or([and([A,B]),and([A,C])])
 3642 * to and(L1|L2) as long as possible to get C1.
 3643 *
 3644 */
 3645
 3646deMorganAnd(L1,[or(L2)|L3],L4) :-
 3647	append(L1,L3,L5),
 3648	distributeAnd(and(L5),or(L2),L4).
 3649deMorganAnd(L1,[C1|L3],L4) :-
 3650	append(L1,[C1],L5),
 3651	deMorganAnd(L5,L3,L4).
 3652deMorganAnd(L1,[],and(L1)).
 3653
 3654/***********************************************************************
 3655 *
 3656 * deMorganOr(+L1,+L2,-C1)
 3657 * applies de Morgan's law
 3658 *      or([A,or([B,C])]) -> and([or([A,B]),or([A,C])])
 3659 * to or(L1|L2) as long as possible to get C1.
 3660 *
 3661 */
 3662
 3663deMorganOr(L1,[and(L2)|L3],L4) :-
 3664	append(L1,L3,L5),
 3665	distributeOr(or(L5),and(L2),L4).
 3666deMorganOr(L1,[C1|L3],L4) :-
 3667	append(L1,[C1],L5),
 3668	deMorganOr(L5,L3,L4).
 3669deMorganOr(L1,[],or(L1)).
 3670
 3671/***********************************************************************
 3672 *
 3673 * deMorgan(+C1,-C2)
 3674 * applies de Morgan's laws to C1
 3675 *      and([A,or([B,C])]) -> or([and([A,B]),and([A,C])])
 3676 *      or([A,and([B,C])]) -> and([or([A,B]),or([A,C])])
 3677 * as long as possible to get C2.
 3678 *
 3679 */
 3680
 3681deMorgan(and(L1),C1) :-
 3682	deMorganAnd([],L1,C1).
 3683deMorgan(or(L1),C1) :-
 3684	deMorganOr([],L1,C1).
 3685deMorgan(C1,C1) :-
 3686	!.
 3687
 3688/***********************************************************************
 3689 *
 3690 * cnf(+C1,-C2)
 3691 * C2 is the conjunctive normalform of C1.
 3692 *
 3693 */
 3694
 3695cnf(C1,C6) :-
 3696	normalizeNot(C1,C2),
 3697	motel_flatten(C2,C3),
 3698	normalizeInverse(C3,C4),
 3699	deMorgan(C4,C5),
 3700	motel_flatten(C5,C6).
 3701
 3702/**********************************************************************
 3703 *
 3704 * @(#) conceptFunctions.pl 1.5@(#)
 3705 *
 3706 */
 3707
 3708/***********************************************************************
 3709 *
 3710 * memberConcept(+Concept,+Dag)
 3711 * Arguments: Concept     concept name
 3712 *            Dag         subsumption hierarchy
 3713 * checks wether or not Concept occurs in the subsumption hierarchy.
 3714 *
 3715 */
 3716
 3717memberConcept(Concept,Dag) :-
 3718	memberElement(Concept,Dag).
 3719
 3720memberConceptSubtrees(Concept,List) :-
 3721	memberElementSubtrees(Concept,List).
 3722
 3723/***********************************************************************
 3724 *
 3725 * memberDirectSubConcepts(+Concept,+Dag)
 3726 * Arguments: Concept     concept name
 3727 *            Dag         subsumption hierarchy
 3728 * checks wether or not Concept occurs in the direct subconcepts of
 3729 * the 'top' concept of Dag.
 3730 *
 3731 */
 3732
 3733memberDirectSubConcepts(Concept,node(_CL,NL)) :-
 3734	!,
 3735	memberDirectSubElements(Concept,NL).
 3736
 3737memberDirectSubConcepts(Concept,List) :-
 3738	memberDirectSubElements(Concept,List).
 3739
 3740/***********************************************************************
 3741 *
 3742 * getDirectSuperConcepts(+EnvName,+MS,+Concept,-CL)
 3743 * Arguments: EnvName     environment identifier
 3744 *            MS          modal context
 3745 *            Concept     concept name
 3746 *            CL          list of concept names
 3747 * CL is the list of all concept names which are direct super concepts
 3748 * of Concept.
 3749 *
 3750 */
 3751
 3752getDirectSuperConcepts(EnvName,MS,Concept,CL) :-
 3753	environment(EnvName,Env,_),
 3754	conceptHierarchy(Env,MS,Dag),
 3755	getDirectSuperElements(Concept,CL,Dag).
 3756
 3757
 3758/***********************************************************************
 3759 *
 3760 * getAllSuperConcepts(+EnvName,+MS,+Concept,-CL)
 3761 * Arguments: EnvName     environment identifier
 3762 *            MS          modal context
 3763 *            Concept     concept name
 3764 *            CL          list of concept names
 3765 * CL is the list of all concept names which are super concepts of
 3766 * Concept.
 3767 *
 3768 */
 3769
 3770getAllSuperConcepts(EnvName,MS,Concept,CL) :-
 3771	environment(EnvName,Env,_),
 3772	conceptHierarchy(Env,MS,Dag),
 3773	getAllSuperElements(Concept,CL,Dag).
 3774
 3775/***********************************************************************
 3776 *
 3777 * getDirectSubConcepts(+EnvName,+MS,+Concept,-CL)
 3778 * Arguments: EnvName     environment identifier
 3779 *            MS          modal context
 3780 *            Concept     concept name
 3781 *            CL          list of concept names
 3782 * CL is the list of all concept names which are direct super concepts
 3783 * of Concept.
 3784 *
 3785 */
 3786
 3787getDirectSubConcepts(EnvName,MS,Concept,CL) :-
 3788	environment(EnvName,Env,_),
 3789	conceptHierarchy(Env,MS,Dag),
 3790	getDirectSubElements(Concept,CL,Dag).
 3791
 3792/***********************************************************************
 3793 *
 3794 * getAllSubConcepts(+EnvName,+MS,+Concept,-CL)
 3795 * Arguments: EnvName     environment identifier
 3796 *            MS          modal context
 3797 *            Concept     concept name
 3798 *            CL          list of concept names
 3799 * CL is the list of all concept names which are super concepts of 
 3800 * Concept.
 3801 *
 3802 */
 3803
 3804getAllSubConcepts(EnvName,MS,Concept,CL) :-
 3805	environment(EnvName,Env,_),
 3806	conceptHierarchy(Env,MS,Dag),
 3807	getAllSubElements(Concept,CL,Dag).
 3808
 3809/***********************************************************************
 3810 *
 3811 * getConcepts(+MS,-CL)
 3812 * Arguments: EnvName     environment identifier
 3813 *            MS          modal context
 3814 *            CL          list of concept names
 3815 * CL is the list of all concept names in the subsumption hierarchy.
 3816 *
 3817 */
 3818
 3819getConcepts(EnvName,MS,['top'|CL]) :-
 3820	getAllSubConcepts(EnvName,MS,'top',CL).
 3821
 3822/***********************************************************************
 3823 *
 3824 * testDirectSuperConcept(+EnvName,+MS,+Concept1,+Concept2,-Concept)
 3825 * Arguments: EnvName        environment identifier
 3826 *            MS             modal context
 3827 *            Concept1       concept name
 3828 *            Concept2       concept name
 3829 *            Concept        concept name
 3830 * Concept is Concept1 iff Concept1 is a direct superconcept of Concept2
 3831 * or
 3832 * Concept is Concept2 iff Concept2 is a direct superconcept of Concept1
 3833 * otherwise
 3834 * the predicate fails.
 3835 *
 3836 */
 3837
 3838testDirectSuperConcept(EnvName,MS,Concept1,Concept2,Concept) :-
 3839	environment(EnvName,Env,_),
 3840	conceptHierarchy(Env,MS,Dag),
 3841	testDirectSuperElement(Concept1,Concept2,Concept,Dag).
 3842
 3843/***********************************************************************
 3844 *
 3845 * testDirectSubConcept(+EnvName,+MS,+Concept1,+Concept2,-Concept)
 3846 * Arguments: EnvName        environment identifier
 3847 *            MS             modal context
 3848 *            Concept1       concept name
 3849 *            Concept2       concept name
 3850 *            Concept        concept name
 3851 * Concept is Concept1 iff Concept1 is a direct subconcept of Concept2
 3852 * or
 3853 * Concept is Concept2 iff Concept2 is a direct subconcept of Concept1
 3854 * otherwise
 3855 * the predicate fails.
 3856 *
 3857 */
 3858
 3859testDirectSubConcept(EnvName,MS,Concept1,Concept2,Concept) :-
 3860	environment(EnvName,Env,_),
 3861	conceptHierarchy(Env,MS,Dag),
 3862	testDirectSubElement(Concept1,Concept2,Concept,Dag).
 3863
 3864/***********************************************************************
 3865 *
 3866 * testSuperConcept(+EnvName,+MS,+Concept1,+Concept2,-Concept)
 3867 * Arguments: EnvName        environment identifier
 3868 *            MS             modal context
 3869 *            Concept1       concept name
 3870 *            Concept2       concept name
 3871 *            Concept        concept name
 3872 * Concept is Concept1 iff Concept1 is a direct superconcept of Concept2
 3873 * or
 3874 * Concept is Concept2 iff Concept2 is a direct superconcept of Concept1
 3875 * otherwise
 3876 * the predicate fails.
 3877 *
 3878 */
 3879
 3880testSuperConcept(EnvName,MS,Concept1,Concept2,Concept) :-
 3881	environment(EnvName,Env,_),
 3882	conceptHierarchy(Env,MS,Dag),
 3883	testSuperElement(Concept1,Concept2,Concept,Dag).
 3884
 3885/***********************************************************************
 3886 *
 3887 * testSubConcept(+EnvName,+MS,+Concept1,+Concept2,-Concept)
 3888 * Arguments: EnvName        environment identifier
 3889 *            MS             modal context
 3890 *            Concept1       concept name
 3891 *            Concept2       concept name
 3892 *            Concept        concept name
 3893 * Concept is Concept1 iff Concept1 is a direct superconcept of Concept2
 3894 * or
 3895 * Concept is Concept2 iff Concept2 is a direct superconcept of Concept1
 3896 * otherwise
 3897 * the predicate fails.
 3898 *
 3899 */
 3900
 3901testSubConcept(EnvName,MS,Concept1,Concept2,Concept) :-
 3902	environment(EnvName,Env,_),
 3903	conceptHierarchy(Env,MS,Dag),
 3904	testSubElement(Concept1,Concept2,Concept,Dag).
 3905
 3906/***********************************************************************
 3907 *
 3908 * getCommonSuperConcepts(+EnvName,+MS,+CL1,-CL2)
 3909 * Arguments: EnvName  environment identifier
 3910 *            MS       modal context
 3911 *            CL1      list of concept names
 3912 *            CL2      list of concept names
 3913 * CL2 is the list of all concept names subsuming all concepts in CL1.
 3914 *
 3915 */
 3916
 3917getCommonSuperConcepts(EnvName,MS,CL1,CL2) :-
 3918	hop_map(getAllSuperConcepts,[EnvName,MS],CL1,CLL1),
 3919	intersection_motel(CLL1,CL2).
 3920
 3921/***********************************************************************
 3922 *
 3923 * getCommonSubConcepts(+EnvName,+MS,+CL1,-CL2)
 3924 * Arguments: EnvName  environment identifier
 3925 *            MS       modal context
 3926 *            CL1      list of concept names
 3927 *            CL2      list of concept names
 3928 * CL2 is the list of all concept names which are subsumed by all
 3929 * concepts in CL1.
 3930 *
 3931 */
 3932
 3933getCommonSubConcepts(EnvName,MS,CL1,CL2) :-
 3934	hop_map(getAllSubConcepts,[EnvName,MS],CL1,CLL1),
 3935	intersection_motel(CLL1,CL2).
 3936
 3937/***********************************************************************
 3938 *
 3939 * getAllObjects(+EnvName,+MS,+O)
 3940 *
 3941 */
 3942
 3943getAllObjects(EnvName,MS,O13) :-
 3944	!,
 3945	environment(EnvName,Env,_),
 3946	setofOrNil(X1,[C1,AX1]^(conceptElement(Env,MS,_,user,X1,C1,AX1)),O1),
 3947	setofOrNil(X2,[R2,Y2,AX2]^roleElement(Env,MS,_,user,X2,Y2,R2,AX2),O2),
 3948	setofOrNil(Y3,[R3,X3,AX3]^roleElement(Env,MS,_,user,X3,Y3,R3,AX3),O3),
 3949	motel_union( O1,O2,O12),
 3950	motel_union(O12,O3,O13),
 3951	!.
 3952/**********************************************************************
 3953 *
 3954 * @(#) constraints.pl 1.2@(#)
 3955 *
 3956 */
 3957
 3958/**********************************************************************
 3959 *
 3960 * solveConstraint(MS,(card,app((FF:R),X),Rel,N),hyp(HYPS),call(CALLS))
 3961 * if Rel is '>=', 
 3962 *    the predicate succeeds if the cardinality of 
 3963 *    app((FF:R),X) in modal context MS is greater than N.
 3964 *    If N is a variable, it will be instantiated with the greatest
 3965 *    number M such that the cardinality of  app((FF:R),X) in modal 
 3966 *    context MS is provably greater than M.
 3967 * if Rel is '=<', 
 3968 *    the predicate succeeds if the cardinality of 
 3969 *    app((FF:R),X) in modal context MS is smaller than N.
 3970 *    If N is a variable, it will be instantiated with the greatest
 3971 *    number M such that the cardinality of  app((FF:R),X) in modal 
 3972 *    context MS is provably smaller than M.
 3973 *
 3974 */
 3975
 3976solveConstraint(Env,MS,(card,app((FF:R),X),Rel,N),(M,S),hyp(HYPS),ab(D),call(CALLS),PTO) :-
 3977%	SolveHead = solveConstraint(MS,(card,app((FF:R),X),Rel,N),hyp(HYPS)),
 3978%	cCS(CALLS,SolveHead),
 3979%	CALLS1 = [SolveHead|CALLS],
 3980	length(CALLS,XXX),
 3981%	format('trying ~d  solve(~w(~w)) ~w ~w~n',[XXX,R,X,Rel,N]),
 3982	collectAllFillers(Env,MS,R,X,HYPS,D,CALLS,S),
 3983	computeNumber(S,Rel,(M,PTAbox)),
 3984	continueSolve(Env,MS,(card,app((FF:R),X),Rel,N),hyp(HYPS),ab(D),call(CALLS),(M,PTAbox),PT),
 3985	PTO = proved(card(R,X,Rel,N),hyp(HYPS),basedOn(PT)).
 3986	
 3987
 3988computeNumber([],'=<',(noRestriction,basedOn(noAboxEntries))) :- !.
 3989computeNumber([],'>=',(noRestriction,basedOn(noAboxEntries))) :- !.
 3990computeNumber(S,_Rel,(M,and(PL))) :-
 3991	reduceToSolutionSet(S,EL,PL),
 3992	length(EL,M).
 3993
 3994reduceToSolutionSet([],[],[]) :- !.
 3995reduceToSolutionSet([(E1,PT1,_)|L],L2,L3) :-
 3996	member((E1,_PT2,_R2),L),
 3997	!,
 3998	reduceToSolutionSet(L,L2,L3).
 3999reduceToSolutionSet([(E1,PT1,_)|L],[E1|L2],[PT1|L3]) :-
 4000	reduceToSolutionSet(L,L2,L3).
 4001
 4002continueSolve(_,_,(card,_,'=<',N),hyp(_),ab(_),call(_),(M,_PTAbox),_) :-
 4003	number(M),
 4004	nonvar(N),
 4005	M >= N,
 4006	!,
 4007	fail.
 4008continueSolve(Env,MS,(card,app((FF:R),X),Rel,N),hyp(HYPS),ab(D),call(CALLS),(M1,PTAbox),PT3) :-
 4009	collectAllConstraints(Env,MS,FF,R,X,Rel,HYPS,D,CALLS,S),
 4010	findNumberRestriction(Rel,(M1,PTAbox),S,(M3,PT3)),
 4011	!,
 4012	comparison(Rel,M3,N).
 4013
 4014collectAllFillers(Env,MS,R,X,HYPS,D,CALLS,S) :-
 4015	EqLiteral = eqGenerator(Env,AX,RN,S,O,MS,Y,app((FF:R),X),HYPS,D,CALLS,PT),
 4016	bagof((Y,PT,[Env,MS,R,X,HYPS,D,CALLS]),AX^RN^S^O^FF^EqLiteral,S),
 4017	!.
 4018collectAllFillers(_,_,_,_,_,_,_,[]) :-
 4019	!.
 4020
 4021
 4022collectAllConstraints(Env,MS,FF,R,X,Rel,HYPS,D,CALLS,S) :-
 4023%	constructConHead(Env,rn(AX,RN,S,O),MS,FF,R,X,Rel,M2,HYPS,D,CALLS,PT,C1),
 4024	C1 = constraint(Env,rn(AX,RN,S,O),MS,(card,app((FF:R),X),Rel,M2),
 4025                       hyp(HYPS),ab(D),call(CALLS),PT),
 4026	bagof((M2,PT,[Env,MS,FF,R,X,Rel,HYPS,D,CALLS]),AX^RN^S^O^FF^C1,S),
 4027	!.
 4028collectAllConstraints(_,_MS,_FF,_R,_X,_Rel,_HYPS,_D,_CALLS,[]) :-
 4029	!.
 4030
 4031
 4032/**********************************************************************
 4033 * 
 4034 * comparison(+Rel,+M,?N)
 4035 * if N is a variable then N is instantiated with M and the predicate
 4036 * succeeds.
 4037 * if N is a number, the predicates succeeds if then goal Rel(M,N)
 4038 * succeeds.
 4039 *
 4040 */
 4041
 4042comparison(_Rel,M3,N) :-
 4043	var(N),
 4044	!,
 4045	N = M3.
 4046comparison(Rel,M3,N) :-
 4047	number(M3), number(N),
 4048	Goal =.. [Rel,M3,N],
 4049	call(Goal).
 4050	
 4051/**********************************************************************
 4052 *
 4053 * findNumberRestristriction(+Rel,+L,-N)
 4054 * if Rel is '=<' then N will be instantiated with the smallest number
 4055 * in the list of numbers L.
 4056 * if Rel is '>=' then N will be instantiated with the greatest number
 4057 * in the list of numbers L.
 4058 *
 4059 */
 4060
 4061findNumberRestriction('=<',(noRestriction,PT1),[],(1000000,PT1)) :- !.
 4062findNumberRestriction('>=',(noRestriction,PT1),[],(0,PT1)) :- !.
 4063findNumberRestriction('>=',(N,PT1),[],(N,PT1)) :- !.
 4064findNumberRestriction('=<',(N,PT1),[],(1000000,noConstraintsFound)) :- !.
 4065findNumberRestriction(_,(noRestriction,_),[(N1,PT2,_)],(N1,PT2)) :- !.
 4066findNumberRestriction('=<',(M,_PT1),[(N1,PT2,_)],(N1,PT2)) :-
 4067	N1 =< M,
 4068	!.
 4069findNumberRestriction('=<',(M,PT1),[(_N1,_,_)],(M,PT1)) :-
 4070	!.
 4071findNumberRestriction('>=',(M,PT1),[(N1,_,_)],(M,PT1)) :-
 4072	M >= N1,
 4073	!.
 4074findNumberRestriction('>=',(_M,_),[(N1,PT2,_)],(N1,PT2)) :-
 4075	!.
 4076findNumberRestriction('>=',(K,PT1),[(N1,_,_)|NL],(N2,PT3)) :-
 4077	findNumberRestriction('>=',(K,PT1,_),NL,(N2,PT3)),
 4078	N2 >= N1,
 4079	!.
 4080findNumberRestriction('=<',(K,PT1),[(N1,_,_)|NL],(N2,PT3)) :-
 4081	findNumberRestriction('=<',(K,PT1,_),NL,(N2,PT3)),
 4082	N2 =< N1,
 4083	!.
 4084findNumberRestriction(_,_,[(N1,PT1,_)|_NL],(N1,PT1)) :-
 4085	!.
 4086
 4087
 4088
 4089
 4090
 4091
 4092
 4093
 4094/**********************************************************************
 4095 *
 4096 * @(#) construct.pl 1.11@(#)
 4097 *
 4098 */
 4099inProofTerm(MS,rn(AX,Rule,_,_),D,X,HYPS,PT1,PT) :-
 4100	nonvar(AX),
 4101	conceptSubsets(_Env,_user,MS1,C1,C2,AX),
 4102	PT = proved(in(MS1,D,X),usingAxiom(defprimconcept(C1,C2)),basedOn(PT1)),
 4103	!.
 4104inProofTerm(MS,rn(AX,Rule,_,_),D,X,HYPS,PT1,PT) :-
 4105	nonvar(AX),
 4106	conceptEqualSets(_Env,_user,MS1,C1,C2,AX),
 4107	PT = proved(in(MS1,D,X),usingAxiom(defconcept(C1,C2)),basedOn(PT1)),
 4108	!.
 4109inProofTerm(MS,rn(AX,Rule,_,_),D,X,HYPS,PT1,PT) :-
 4110	nonvar(AX),
 4111	conceptElement(_Env,MS1,_,user,C1,C2,AX),
 4112	PT = proved(in(MS1,D,X),usingAxiom(assert_ind(C1,C2)),basedOn(PT1)),
 4113	!.
 4114inProofTerm(MS,rn(AX,Rule,_,_),D,X,HYPS,PT1,PT) :-
 4115	!.
 4116
 4117inProofTerm(MS,Name,D,X,HYPS,PT1,PT) :-
 4118	PT = proved(in(MS,Name,D,X),basedOn(PT1)),
 4119	!.
 4120inProofTerm(MS,D,X,HYPS,PT1,PT) :-
 4121	PT = proved(in(MS,D,X),basedOn(PT1)),
 4122	!.
 4123
 4124eqProofTerm(MS,Y,_FF,R,X,HYPS,PT1,PT) :-
 4125	nonvar(R),
 4126	atomic(R),
 4127	!,
 4128	Rel =.. [R,MS,X,Y],
 4129	PT = proved(Rel,basedOn(PT1)),
 4130	!.
 4131eqProofTerm(MS,Y,_FF,R,X,HYPS,PT1,PT) :-
 4132	Rel = rel(R,MS,X,Y),
 4133	PT = proved(Rel,basedOn(PT1)),
 4134	!.
 4135conProofTerm(MS,R,X,Rel,N,HYPS,PT1,PT) :-
 4136	PT = proved(card(R,MS,X,Rel,N),basedOn(PT1)),
 4137	!.
 4138/***********************************************************************
 4139 *
 4140 * makeTerm(+TermPieces,-Term)
 4141 *
 4142 */
 4143
 4144makeTerm(Term,Term) :-
 4145	var(Term),
 4146	!.
 4147makeTerm(Term,Term) :-
 4148	atomic(Term),
 4149	!.
 4150makeTerm([Functor|ArgList],Term) :-
 4151	hop_map(makeTerm,ArgListTerms,ArgList),
 4152	Term =.. [Functor|ArgListTerms].
 4153makeTerm(Term,Term).
 4154
 4155%element(X) :-
 4156%	atomic(X),
 4157%	!.
 4158%element(X) :-
 4159%	var(X),
 4160%	!.
 4161element(_) :- !.
 4162
 4163relation(R,RN,X1,Y1) :-
 4164%	nonvar(R),
 4165%	R =.. [RN,X1,Y1].
 4166	T =.. [RN,X1,Y1],
 4167	R = T.
 4168
 4169eqGenerator(Env,AX,RN,S,O,MS,X,Y,HYPS,D,CALLS,PT) :-
 4170	eq(Env,rn(AX,RN,S,O),modal(MS),X,Y,hyp(HYPS),ab(D),call(CALLS),PT),
 4171	nonvar(X),
 4172	nonvar(Y),
 4173	atomic(X).
 4174
 4175gensymbol(Symbol,_L,NewSymbol) :-
 4176	gensym(Symbol,NewSymbol),
 4177	!.
 4178
 4179
 4180/**********************************************************************
 4181 *
 4182 * ruleName(+AxiomName,+RuleName,+Orientation)
 4183 *
 4184 */
 4185
 4186ruleName(AxiomName,RuleName,Origin,Orientation,
 4187	 rn(AxiomName,RuleName,Origin,Orientation)) :- 
 4188	!.
 4189
 4190reverseOrientation(lInR,rInL) :- !.
 4191reverseOrientation(rInL,lInR) :- !.
 4192
 4193
 4194typeOfDefinition(_,_,C,system) :-
 4195	var(C),
 4196	!.
 4197typeOfDefinition(Env,MS,C,user) :-
 4198	getConceptName(Env,MS,C),
 4199	!.
 4200typeOfDefinition(_,_,C,system) :-
 4201	atomic(C),
 4202	name(C,[99,111,110,99,101,112,116|_]),
 4203	!.
 4204typeOfDefinition(Env,MS,R,user) :-
 4205	getRoleName(Env,MS,R),
 4206	!.
 4207typeOfDefinition(_,_,R,system) :-
 4208	atomic(R),
 4209	name(R,[114,111,108,101|_]),
 4210	!.
 4211typeOfDefinition(Env,MS,not(C),Type) :-
 4212	!,
 4213	typeOfDefinition(Env,MS,C,Type).
 4214typeOfDefinition(_,_,normal(C),system) :-
 4215	!.
 4216typeOfDefinition(_,_,not(normal(C)),system) :-
 4217	!.
 4218typeOfDefinition(_,_,_,user) :-
 4219	!.
 4220
 4221% someInterpretation([]).
 4222% someInterpretation([I1|IL]) :-
 4223% 	call(I1),
 4224% 	someInterpretation(IL).
 4225% 
 4226% allInterpretation([]) :-
 4227% 	fail.
 4228% allInterpretation([I1|IL]) :-
 4229% 	(call(I1) ; allInterpretation(IL)).
 4230% 
 4231% roleConjunction(X,IL) :-
 4232% 	var(X),
 4233% 	someInterpretation(IL).
 4234% roleConjunction(X,IL) :-
 4235% 	nonvar(X),
 4236% 	name(X,[115,107,111,108,101,109|_]),
 4237% 	allInterpretation(IL).
 4238% roleConjunction(X,IL) :-
 4239% 	nonvar(X),
 4240% 	not(name(X,[115,107,111,108,101,109|_])),
 4241% 	someInterpretation(IL).
 4242
 4243
 4244/***********************************************************************
 4245 *
 4246 * convertMS(Env,+MS1,+ModalOperator,WVL1,-MS2,WVL2)
 4247 * Arguments: MS1                modal context
 4248 *            ModalOperator      modal operator
 4249 *            WVL1               list of free world variables already
 4250 *                               generated during the conversion
 4251 *            MS2                modal context
 4252 *            WVL2               list of all free world variables 
 4253 *                               generated during the conversion
 4254 * MS2 is the translation of ModalOperator appended to MS1.
 4255 *
 4256 */
 4257
 4258genagent(X,_,X) :-
 4259	var(X),
 4260	!.
 4261genagent(all,free,_A) :-
 4262	!.
 4263genagent(all,skolemize,A) :-
 4264	gensym(agent,A),
 4265	!.
 4266genagent(A,_,A) :-
 4267	!.
 4268
 4269convertMS(positive,Env,Start,MS,WVL1,End,WVL2) :-
 4270	!,
 4271	convertMS(Env,Start,MS,WVL1,End,WVL2).
 4272convertMS(negative,Env,Start,MS1,WVL1,End,WVL2) :-
 4273	!,
 4274	hop_map(negate,MS1,MS2),
 4275	hop_map(normalizeNot,MS2,MS3),
 4276	convertMS(Env,Start,MS3,WVL1,End,WVL2).
 4277	
 4278
 4279convertMS(_Env,_,MS,WVL,[_W1,true],WVL) :-
 4280	var(MS),
 4281	!.
 4282convertMS(_Env,[MS1,Lits1],[],WVL,[MS1,Lits1],WVL) :-
 4283	!.
 4284convertMS(Env,[MS1,Lits1],[d(MOp,A)|L],WVL,[MS3,Lits3],WVL3) :-
 4285	gensym(wp,WP),
 4286	WPTerm = [WP,WVL],
 4287	genagent(A,skolemize,Agent),
 4288	MS2 = app(WPTerm:m(MOp,Agent),MS1),
 4289	convertMS(Env,[MS2,Lits1],L,WVL,[MS3,Lits3],WVL3),
 4290	!.
 4291convertMS(Env,[MS1,Lits1],[b(MOp,A)|L],WVL,[MS3,Lits3],WVL3) :-
 4292	genagent(A,free,Agent),
 4293	Lit = rel(Env,_,m(MOp,Agent),MS1,MS2),
 4294	convertMS(Env,[MS2,(Lit,Lits1)],L,[MS2|WVL],[MS3,Lits3],WVL3),
 4295	!.
 4296convertMS(Env,[MS1,Lits1],[dc(MOp,C)|L],WVL,[MS3,Lits3],WVL3) :-
 4297	gensym(wp,WP),
 4298	WPTerm = [WP,WVL],
 4299	genagent(all,skolemize,Agent),
 4300	MS2 = app(WPTerm:m(MOp,Agent),MS1),
 4301	getQuery(Env,MS1,C,Agent,_Exp,Body),
 4302	convertMS(Env,[MS2,(once(Body),Lits1)],L,WVL,[MS3,Lits3],WVL3),
 4303	!.
 4304convertMS(Env,[MS1,Lits1],[bc(MOp,C)|L],WVL,[MS3,Lits3],WVL3) :-
 4305	genagent(all,free,Agent),
 4306	Lit = rel(Env,_,m(MOp,Agent),MS1,MS2),
 4307	getQuery(Env,MS1,C,Agent,_Exp,Body),
 4308	convertMS(Env,[MS2,((once(Body),Lit),Lits1)],L,[MS2|WVL],[MS3,Lits3],WVL3),
 4309	!.
 4310
 4311
 4312/***********************************************************************
 4313 *
 4314 * THE STRUCTURE OF THE IN-CLAUSES
 4315 * 
 4316 * 1) THE HEAD
 4317 *    in(Env,RN,modal(W),A1,X,hyp(C1),ab(D),call(H1),Exp)
 4318 *    Env is a internal environment name
 4319 *    RN  is a rule name
 4320 *    W   is a world
 4321 *    A1  is a concept name or the negation of a concept name
 4322 *    X   is a free variable
 4323 *    C1  is a list of clauses --- the hypotheses that can be used
 4324 *    D   is a name identifying a specific abductive derivation
 4325 *    H1  is a list of calls   --- the calls to in that have already
 4326 *                                 been used
 4327 *    Exp is a explanation term
 4328 * 2) THE BODY
 4329 *
 4330 */
 4331
 4332/***********************************************************************
 4333 *
 4334 * constructMLHead(+ModalSequence,
 4335 *                 +ConceptName,+Constraint,
 4336 *                 +Hypotheses,+CallStack,-Inhead)
 4337 * 
 4338 */
 4339
 4340constructInHead(Env,Name,MS,CN,CON,HYP,D,CALL,PT1,InHead) :-
 4341	inProofTerm(MS,Name,CN,CON,HYP,PT1,PT),
 4342	InHead = in(Env,Name,modal(MS),CN,CON,hyp(HYP),ab(D),call(CALL),PT),
 4343	!.
 4344
 4345constructKBHead(Env,Priority,Name,MS,CN,CON,HYP,D,CALL,PT1,InHead) :-
 4346	inProofTerm(MS,Name,CN,CON,HYP,PT1,PT),
 4347	InHead = kb_in(Env,Priority,Name,modal(MS),CN,CON,hyp(HYP),ab(D),call(CALL),PT),
 4348	!.
 4349
 4350constructMLHead(Env,Name,MS,CN,CON,HYP,D,CALL,PT1,InHead) :-
 4351	inProofTerm(MS,Name,CN,CON,HYP,PT1,PT),
 4352	InHead = kb_in(Env,pr(3),Name,modal(MS),CN,CON,hyp(HYP),ab(D),call(CALL),PT),
 4353	!.
 4354
 4355getEnvironment(kb_in(Env,pr(_),_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),_),Env).
 4356getEnvironment(in(Env,_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),_),Env).
 4357getModalSequence(kb_in(_,pr(_),_,modal(MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),_),MS).
 4358getModalSequence(in(_,_,modal(MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),_),MS).
 4359getConceptName(kb_in(_,pr(_),_,modal(_MS),CN,_CON,hyp(_HYP),ab(_),call(_CALL),_),CN).
 4360getConceptName(in(_,_,modal(_MS),CN,_CON,hyp(_HYP),ab(_),call(_CALL),_),CN).
 4361getConstraint(kb_in(_,pr(_),_,modal(_MS),_CN,CON,hyp(_HYP),ab(_),call(_CALL),_),CON).
 4362getConstraint(in(_,_,modal(_MS),_CN,CON,hyp(_HYP),ab(_),call(_CALL),_),CON).
 4363getHypotheses(kb_in(_,pr(_),_,modal(_MS),_CN,_CON,hyp(HYP),ab(_),call(_CALL),_),HYP).
 4364getHypotheses(in(_,_,modal(_MS),_CN,_CON,hyp(HYP),ab(_),call(_CALL),_),HYP).
 4365getCallStack(kb_in(_,pr(_),_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(CALL),_),CALL).
 4366getCallStack(in(_,_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(CALL),_),CALL).
 4367getExplanation(kb_in(_,pr(_),_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),E),E).
 4368getExplanation(in(_,_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),E),E).
 4369getInExplanation(kb_in(_,pr(_),_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),
 4370	         proved(I,_)),I).
 4371getInExplanation(in(_,_,modal(_MS),_CN,_CON,hyp(_HYP),ab(_),call(_CALL),
 4372	         proved(I,_)),I).
 4373
 4374/**********************************************************************
 4375 *
 4376 * constructEqHead(Env,+MS,+Y,+F,+R,+X,+HYPS,+CALLS,-L)
 4377 *
 4378 */
 4379
 4380constructEqHead(Env,Name,MS,Y,F,R,X,HYPS,D,CALLS,PT1,L) :-
 4381	eqProofTerm(MS,Y,F,R,X,HYPS,PT1,PT),
 4382	L = eq(Env,Name,modal(MS),Y,app((F:R),X),hyp(HYPS),ab(D),call(CALLS),PT),
 4383	!.
 4384
 4385/**********************************************************************
 4386 *
 4387 * constructEqMark(+MS,+Y,+F,+R,+X,+HYPS,+CALLS,+AN,-L)
 4388 *
 4389 */
 4390
 4391constructEqMark(Name,MS,Y,F,R,X,HYPS,_D,_CALLS,L) :-
 4392	HYPS = [or(H1),rl(H2),fl(H3)],
 4393	L = eq(Name,modal(MS),Y,app((F:R),X),hyp(H1)),
 4394	!.
 4395
 4396/**********************************************************************
 4397 *
 4398 * constructEqCall(Env,+MS,+Y,+F,+R,+X,+HYPS,+CALLS,+AN,-L)
 4399 *
 4400 */
 4401
 4402constructEqCall(Env,rn(AX,RN,_Source,Orientation),bodyMC(MS1),headMC(MS2),
 4403	        Y,F,R,X,HYPS,D,CALLS,PT,L) :-
 4404	constructEqMark(rn(AX,RN,_S1,Orientation),MS2,Y,F,R,X,HYPS,D,CALLS,C1),
 4405	L = eq(Env,rn(_AX2,_RN2,_S2,_O2),modal(MS1),Y,app((F:R),X),
 4406               hyp(HYPS),ab(D),call([C1|CALLS]),PT),
 4407	!.
 4408
 4409/***********************************************************************
 4410 *
 4411 * constructMLMark(+ModalSequence,+ConceptName,+Constraint,
 4412 *                      +AxiomName,-LoopCheck)
 4413 *
 4414 */
 4415
 4416constructMLMark(Name,MS,CN,CON,HYPS,D,LoopCheck) :-
 4417	HYPS = [or(H1),rl(H2),fl(H3)],
 4418	LoopCheck = in(Name,modal(MS),CN,CON,hyp(H1),ab(D)),
 4419	!.
 4420
 4421constructMLMark(kb_in(_,Pr,Name,modal(MS),CN,CON,hyp(HYP),ab(D),call(_),_),LoopCheck) :-
 4422	HYPS = [or(H1),rl(H2),fl(H3)],
 4423	LoopCheck = in(Name,modal(MS),CN,CON,hyp(H1),ab(D)),
 4424	!.
 4425constructMLMark(in(_,Pr,Name,modal(MS),CN,CON,hyp(HYP),ab(D),call(_),_),LoopCheck) :-
 4426	HYPS = [or(H1),rl(H2),fl(H3)],
 4427	LoopCheck = in(Name,modal(MS),CN,CON,hyp(H1),ab(D)),
 4428	!.
 4429constructMLMark(in(_,Name,modal(MS),CN,CON,hyp(HYP),ab(D),call(_),_),LoopCheck) :-
 4430	HYPS = [or(H1),rl(H2),fl(H3)],
 4431	LoopCheck = in(Name,modal(MS),CN,CON,hyp(H1),ab(D)),
 4432	!.
 4433
 4434/***********************************************************************
 4435 *
 4436 * constructMLCall(+Env,rn(+AX1,+RN1,+S1,+O1),bodyMC(MS1),headMC(MS2), 
 4437 *                 +ConceptName,+Variable,
 4438 *                 +Hypotheses,+DerivationName,+CallStack,+Proofterm,
 4439 *                 -InTerm)
 4440 *
 4441 * The information in rn(AX1,RN1,S1,O1)  is used in the following way:
 4442 * AX1, RN1, and O1 is used in the construction of the MLMark
 4443 * which is added to the call stack. If AX1 is `no' then the MLMark is
 4444 * not added to the call stack at all.
 4445 * S1 is used in the construction of InHead. If S1 is a variable, any 
 4446 * rule can be used to prove the call. If S1 is `user' then only user
 4447 * provided rules may be used. If S1 is `system' then only system provided
 4448 * rules may be used.
 4449 *
 4450 */
 4451
 4452constructMLCall(Env,rn(AX1,RN1,S1,O1),bodyMC(MS1),headMC(MS2),
 4453                CN,CON,HYPS,D,CALLS,PT1,InHead) :-
 4454	HYPS = [or(H1),rl(H2),fl(H3)],
 4455	constructMLMark(rn(AX1,RN1,_S2,_O2),MS2,CN,CON,HYPS,D,Mark),
 4456	convert_loop(AX1,CALLS,Mark,CALLS1),
 4457	getNegatedConcept(CN,C2),
 4458	InHeadH = in(_NameH,modal(MS1),C2,CON,hyp(_H),ab(_D)),
 4459	getSource(S1,Source),
 4460	InHead = in(Env,rn(_AX3,_RN3,Source,_O3),modal(MS1),CN,CON,
 4461                    hyp([or(H1),rl([InHeadH|H2]),fl(H3)]),
 4462                    ab(D),call(CALLS1),PT1),
 4463	!.
 4464
 4465
 4466getSource(V1,_V2) :-
 4467	var(V1),
 4468	!.
 4469getSource(any,_V2) :-
 4470	!.
 4471getSource(V1,V1) :-
 4472	!.
 4473
 4474getNegatedConcept(CN,not(CN)) :-
 4475	var(CN),
 4476	!.
 4477getNegatedConcept(CN,C2) :-
 4478	normalizeNot(not(CN),C2),
 4479	!.
 4480
 4481/***********************************************************************
 4482 *
 4483 * constructConHead(Env,+Name,+MS,+F,+R,+X,+Rel,+N,
 4484 *                  +HYPS,+CALLS,-Literal)
 4485 *
 4486 */
 4487
 4488constructConHead(Env,Name,MS,F,R,X,Rel,N,HYPS,D,CALLS,PT1,L) :-
 4489	conProofTerm(MS,R,X,Rel,N,HYPS,PT1,PT),
 4490	L = constraint(Env,Name,MS,(card,app((F:R),X),Rel,N),
 4491                       hyp(HYPS),ab(D),call(CALLS),PT),
 4492	!.
 4493
 4494/***********************************************************************
 4495 *
 4496 * constructConMark(+MS,+F,+R,+X,+Rel,+N,+HYPS,+CALLS,+AN,-Literal)
 4497 *
 4498 */
 4499
 4500constructConMark(Name,MS,F,R,X,Rel,N,HYPS,_D,_CALLS,L) :-
 4501	HYPS = [or(H1),rl(H2),fl(H3)],
 4502	L = constraint(Name,MS,(card,app((F:R),X),Rel,N),hyp(H1)),
 4503	!.
 4504
 4505constructConMark(constraint(_,Name,MS,(card,A,Rel,N),hyp(HYPS),ab(_D),call(_CALLS),_PT),L) :-
 4506	HYPS = [or(H1),rl(H2),fl(H3)],
 4507	L = constraint(Name,MS,(card,A,Rel,N),hyp(H1)),
 4508	!.
 4509
 4510/***********************************************************************
 4511 *
 4512 * constructSolveConMark(+MS,+F,+R,+X,+Rel,+N,+HYPS,+CALLS,+AN,-Literal)
 4513 *
 4514 */
 4515
 4516constructSolveConMark(Name,MS,F,R,X,Rel,N,HYPS,_D,_CALLS,L) :-
 4517	HYPS = [or(H1),rl(H2),fl(H3)],
 4518	L = solveConstraint(Name,MS,(card,app((F:R),X),Rel,N),hyp(H1)),
 4519	!.
 4520
 4521constructSolveConMark(constraint(_,Name,MS,(card,A,Rel,N),hyp(HYPS),ab(_D),call(_CALLS),_PT),L) :-
 4522	HYPS = [or(H1),rl(H2),fl(H3)],
 4523	L = solveConstraint(Name,MS,(card,A,Rel,N),hyp(H1)),
 4524	!.
 4525
 4526/***********************************************************************
 4527 *
 4528 * constructConCall(Env,+MS,+F,+R,+X,+Rel,+N,+HYPS,+CALLS,+AN,-Literal)
 4529 *
 4530 */
 4531
 4532constructConCall(Env,bodyMC(MS1),headMC(MS2),F,R,X,Rel,N,HYPS,D,CALLS,AN,PT1,L) :-
 4533	constructConMark(MS2,F,R,X,Rel,N,HYPS,D,CALLS,AN,Mark),
 4534        L = constraint(Env,_Name,MS1,(card,app((F:R),X),Rel,N),
 4535                       hyp(HYPS),ab(D),call([Mark|CALLS]),PT1),
 4536	!.
 4537
 4538
 4539addDefaultML(I1,L1) :-
 4540	var(L1),
 4541	!,
 4542	L1 = [I1|_L2],
 4543	!.
 4544addDefaultML(I1,[_|L1]) :-
 4545	addDefaultML(I1,L1),
 4546	!.
 4547
 4548memberDML(I1,L) :-
 4549	nonvar(L),
 4550	L = [I1|L2],
 4551	!.
 4552memberDML(I1,L) :-
 4553	nonvar(L),
 4554	L = [_|L2],
 4555	memberDML(I1,L2).
 4556
 4557
 4558/**********************************************************************
 4559 *
 4560 * getAxiom(+Env,+MS,AX)
 4561 * succeeds if AX is an axiom in environment Env and modal context
 4562 * MS.
 4563 *
 4564 */
 4565	
 4566getAxiom(Env,MS,Ax) :-
 4567	axiom(Env,MS,Ax).
 4568
 4569/**********************************************************************
 4570 *
 4571 * getConceptName(+Env,+MS,CN)
 4572 * succeeds if CN is a concept name in environment Env and modal context
 4573 * MS.
 4574 *
 4575 */
 4576
 4577getConceptName(Env,MS1,CN) :-
 4578	convertMS(negative,Env,[[],true],MS1,[],[W1,G1],_),
 4579	clause(conceptName(Env,_,W1,CN),_),
 4580	once((call(G1),conceptName(Env,_,W1,CN))).
 4581
 4582/**********************************************************************
 4583 *
 4584 * getRoleName(+Env,+MS,CN)
 4585 * succeeds if CN is a role name in environment Env and modal context
 4586 * MS.
 4587 *
 4588 */
 4589
 4590getRoleName(Env,MS1,CN) :-
 4591	convertMS(negative,Env,[[],true],MS3,[],[W1,G1],_),
 4592	clause(roleName(Env,_,W1,CN),_),
 4593	once((call(G1),roleName(Env,_,W1,CN))).
 4594
 4595
 4596/**********************************************************************
 4597 *
 4598 * @(#) dag.pl 1.3@(#)
 4599 *
 4600 */
 4601
 4602/***********************************************************************
 4603 *
 4604 * memberElement(+Element,+Dag)
 4605 * Parameter: Element     element name
 4606 *            Dag         subsumption hierarchy
 4607 * checks wether or not Element occurs in the subsumption hierarchy.
 4608 *
 4609 */
 4610
 4611memberElement(Element,node(CL,_NL)) :-
 4612	member(Element,CL),
 4613	!.
 4614memberElement(Element,node(_CL,NL)) :-
 4615	memberElementSubtrees(Element,NL),
 4616	!.
 4617
 4618memberElementSubtrees(_Element,[]) :-
 4619	!,
 4620	fail.
 4621memberElementSubtrees(Element,[N1|_NL]) :-
 4622	memberElement(Element,N1),
 4623	!.
 4624memberElementSubtrees(Element,[_N1|NL]) :-
 4625	memberElementSubtrees(Element,NL).
 4626
 4627/***********************************************************************
 4628 *
 4629 * memberDirectSubElements(+Element,+Dag)
 4630 * Parameter: Element     element name
 4631 *            Dag         subsumption hierarchy
 4632 * checks wether or not Element occurs in the direct subelements of
 4633 * the 'top' element of Dag.
 4634 *
 4635 */
 4636
 4637memberDirectSubElements(Element,node(_CL,NL)) :-
 4638	!,
 4639	memberDirectSubElements(Element,NL).
 4640
 4641memberDirectSubElements(_Element,[]) :-
 4642	!,
 4643	fail.
 4644memberDirectSubElements(Element,[node(CL,_NL1)|_NL]) :-
 4645	member(Element,CL),
 4646	!.
 4647memberDirectSubElements(Element,[_N1|NL]) :-
 4648	memberDirectSubElements(Element,NL).
 4649
 4650/***********************************************************************
 4651 *
 4652 * getDirectSuperElements(+Element,-CL,+Dag)
 4653 * Parameter: Dag         subsumption hierarchy
 4654 *            Element     element name
 4655 *            CL          list of element names
 4656 * CL is the list of all element names which are direct super elements
 4657 * of Element.
 4658 *
 4659 */
 4660
 4661getDirectSuperElements(Element,CL,node(CL,NL)) :-
 4662	memberDirectSubElements(Element,node(CL,NL)),
 4663	!.
 4664getDirectSuperElements(Element,CL,node(_,NL)) :-
 4665	getDirectSuperElements(Element,CL,NL).
 4666
 4667getDirectSuperElements(_Element,[],[]) :-
 4668	!.
 4669getDirectSuperElements(Element,CL,[N1|NL]) :-
 4670	getDirectSuperElements(Element,CL1,N1),
 4671	getDirectSuperElements(Element,CL2,NL),
 4672	motel_union(CL1,CL2,CL).
 4673
 4674/***********************************************************************
 4675 *
 4676 * getAllSuperElements(+Element,-CL,+Dag)
 4677 * Parameter: Element     element name
 4678 *            CL          list of element names
 4679 *            Dag         subsumption hierarchy
 4680 * CL is the list of all element names which are super elements of
 4681 * Element.
 4682 *
 4683 */
 4684
 4685getAllSuperElements(Element,CL,Dag) :-
 4686	getAllSuperElements(Element,CL,[],Dag).
 4687
 4688getAllSuperElements(Element,CL1,CL1,node(CL,_NL)) :-
 4689	member(Element,CL),
 4690	!.
 4691getAllSuperElements(Element,CL3,CL1,node(CL,NL)) :-
 4692	motel_union(CL,CL1,CL2),
 4693	getAllSuperElements(Element,CL3,CL2,NL).
 4694
 4695getAllSuperElements(_Element,[],_CL1,[]) :-
 4696	!.
 4697getAllSuperElements(Element,CL2,CL1,[N1|NL]) :-
 4698	getAllSuperElements(Element,CL3,CL1,N1),
 4699	getAllSuperElements(Element,CL4,CL1,NL),
 4700	motel_union(CL3,CL4,CL2).
 4701
 4702
 4703/***********************************************************************
 4704 *
 4705 * getDirectSubElements(+Element,-CL,+Dag)
 4706 * Parameter: Element     element name
 4707 *            CL          list of element names
 4708 *            Dag         subsumption hierarchy
 4709 * CL is the list of all element names which are direct sub elements
 4710 * of Element.
 4711 *
 4712 */
 4713
 4714getDirectSubElements(Element,CL1,node(CL,NL)) :-
 4715	member(Element,CL),
 4716	!,
 4717	getSubElements(CL1,NL).
 4718getDirectSubElements(Element,CL1,node(_CL,NL)) :-
 4719	getDirectSubElements(Element,CL1,NL).
 4720
 4721getDirectSubElements(_Element,[],[]) :-
 4722	!.
 4723getDirectSubElements(Element,CL,[N1|NL]) :-
 4724	getDirectSubElements(Element,CL1,N1),
 4725	getDirectSubElements(Element,CL2,NL),
 4726	motel_union(CL1,CL2,CL).
 4727
 4728getSubElements([],[]) :-
 4729	!.
 4730getSubElements(CL,[node(CL1,_)|NL]) :-
 4731	getSubElements(CL2,NL),
 4732	motel_union(CL1,CL2,CL).
 4733
 4734
 4735/***********************************************************************
 4736 *
 4737 * getAllSubElements(+Dag,+Element,-CL,+Dag)
 4738 * Parameter: Element     element name
 4739 *            CL          list of element names
 4740 *            Dag         subsumption hierarchy
 4741 * CL is the list of all element names which are sub elements of 
 4742 * Element
 4743 *
 4744 */
 4745
 4746getAllSubElements(Element,CL1,node(CL,NL)) :-
 4747	member(Element,CL),
 4748	!,
 4749	getElements(CL1,NL).
 4750getAllSubElements(Element,CL1,node(_CL,NL)) :-
 4751	getAllSubElements(Element,CL1,NL),
 4752	!.
 4753
 4754getAllSubElements(_Element,[],[]) :-
 4755	!.
 4756getAllSubElements(Element,CL,[N1|NL1]) :-
 4757	getAllSubElements(Element,CL2,N1),
 4758	getAllSubElements(Element,CL3,NL1),
 4759	motel_union(CL2,CL3,CL).
 4760
 4761/***********************************************************************
 4762 *
 4763 * getElements(-CL,+Dag)
 4764 * Parameter: CL     list of element names
 4765 *            Dag    subsumption hierarchy
 4766 * CL is the list of all element names in the subsumption hierarchy.
 4767 *
 4768 */
 4769
 4770getElements(CL,node(CL1,NL)) :-
 4771	getElements(CL2,NL),
 4772	motel_union(CL1,CL2,CL).
 4773getElements([],[]) :-
 4774	!.
 4775getElements(CL,[N1|NL]) :-
 4776	getElements(CL1,N1),
 4777	getElements(CL2,NL),
 4778	motel_union(CL1,CL2,CL).
 4779
 4780
 4781/***********************************************************************
 4782 *
 4783 * testDirectSuperElement(+Element1,+Element2,-Element,+Dag)
 4784 * Parameter: Element1       element name
 4785 *            Element2       element name
 4786 *            Element        element name
 4787 *            Dag            subsumption hierarchy
 4788 * Element is Element1 iff Element1 is a direct superelement of Element2
 4789 * or
 4790 * Element is Element2 iff Element2 is a direct superelement of Element1
 4791 * otherwise
 4792 * the predicate fails
 4793 *
 4794 */
 4795
 4796testDirectSuperElement(Element1,Element2,Element1,node(CL,NL)) :-
 4797	member(Element1,CL),
 4798	!,
 4799	memberDirectSubElements(Element2,node(CL,NL)).
 4800testDirectSuperElement(Element1,Element2,Element2,node(CL,NL)) :-
 4801	member(Element2,CL),
 4802	!,
 4803	memberDirectSubElements(Element1,node(CL,NL)).
 4804
 4805/***********************************************************************
 4806 *
 4807 * testDirectSubElement(+Element1,+Element2,-Element,+Dag)
 4808 * Parameter: Element1       element name
 4809 *            Element2       element name
 4810 *            Element        element name
 4811 *            Dag            subsumption hierarchy
 4812 * Element is Element1 iff Element1 is a direct subelement of Element2
 4813 * or
 4814 * Element is Element2 iff Element2 is a direct subelement of Element1
 4815 * otherwise
 4816 * the predicate fails
 4817 *
 4818 */
 4819
 4820testDirectSubElement(Element1,Element2,Element2,node(CL,NL)) :-
 4821	member(Element1,CL),
 4822	!,
 4823	memberDirectSubElements(Element2,node(CL,NL)).
 4824testDirectSubElement(Element1,Element2,Element1,node(CL,NL)) :-
 4825	member(Element2,CL),
 4826	!,
 4827	memberDirectSubElements(Element1,node(CL,NL)).
 4828
 4829
 4830/***********************************************************************
 4831 *
 4832 * testSuperElement(+Element1,+Element2,-Element,+Dag)
 4833 * Parameter: Element1       element name
 4834 *            Element2       element name
 4835 *            Element        element name
 4836 *            Dag            subsumption hierarchy
 4837 * Element is Element1 iff Element1 is a direct superelement of Element2
 4838 * or
 4839 * Element is Element2 iff Element2 is a direct superelement of Element1
 4840 * otherwise
 4841 * the predicate fails
 4842 *
 4843 */
 4844
 4845testSuperElement(Element1,Element2,Element1,node(CL,NL)) :-
 4846	member(Element1,CL),
 4847	!,
 4848	memberElementSubtrees(Element2,NL).
 4849testSuperElement(Element1,Element2,Element2,node(CL,NL)) :-
 4850	member(Element2,CL),
 4851	!,
 4852	memberElementSubtrees(Element1,NL).
 4853
 4854
 4855/***********************************************************************
 4856 *
 4857 * testSubElement(+Element1,+Element2,-Element,+Dag)
 4858 * Parameter: Element1       element name
 4859 *            Element2       element name
 4860 *            Element        element name
 4861 *            Dag            subsumption hierarchy
 4862 * Element is Element1 iff Element1 is a direct superelement of Element2
 4863 * or
 4864 * Element is Element2 iff Element2 is a direct superelement of Element1
 4865 * otherwise
 4866 * the predicate fails
 4867 *
 4868 */
 4869
 4870testSubElement(Element1,Element2,Element1,node(CL,NL)) :-
 4871	member(Element2,CL),
 4872	!,
 4873	memberElementSubtrees(Element1,NL).
 4874testSubElement(Element1,Element2,Element2,node(CL,NL)) :-
 4875	member(Element1,CL),
 4876	!,
 4877	memberElementSubtrees(Element2,NL).
 4878
 4879
 4880/***********************************************************************
 4881 *
 4882 * getCommonSuperElements(+CL1,-CL2,+Dag)
 4883 * Parameter: CL1      list of element names
 4884 *            CL2      list of element names
 4885 *            Dag      subsumption hierarchy
 4886 * CL2 is the list of all element names subsuming all elements in CL1.
 4887 *
 4888 */
 4889
 4890getCommonSuperElements(CL1,CL2,Dag) :-
 4891	hop_map(getAllSuperElements,[Dag],CL1,CLL1),
 4892	intersection_motel(CLL1,CL2).
 4893
 4894/***********************************************************************
 4895 *
 4896 * getCommonSubElements(+CL1,-CL2,Dag)
 4897 * Parameter: CL1      list of element names
 4898 *            CL2      list of element names
 4899 *            Dag      subsumption hierarchy
 4900 * CL2 is the list of all element names which are subsumed by all
 4901 * elements in CL1.
 4902 *
 4903 */
 4904
 4905getCommonSubElements(CL1,CL2,Dag) :-
 4906	hop_map(getAllSubElements,[Dag],CL1,CLL1),
 4907	intersection_motel(CLL1,CL2).
 4908
 4909
 4910
 4911
 4912
 4913
 4914
 4915
 4916/**********************************************************************
 4917 *
 4918 * @(#) env.pl 1.21@(#)
 4919 *
 4920 */
 4921
 4922
 4923/**********************************************************************
 4924 *
 4925 * getCurrentEnvironment(EnvName)
 4926 * gets the name of the current environment
 4927 *
 4928 */
 4929
 4930getCurrentEnvironment(EnvName) :-
 4931	currentEnvironment(Env),
 4932	environment(EnvName,Env,_),
 4933	!.
 4934
 4935/**********************************************************************
 4936 *
 4937 * makeEnvironment(+Name,+Comment)
 4938 * creates new environement with name Name. Comment can be any string
 4939 * Name will become the current environment.
 4940 *
 4941 */
 4942
 4943makeEnvironment(Name,Comment) :-
 4944	getTwoRandomNumbers(RT,CT),
 4945	FirstChar is 97 + (CT mod 26),
 4946	Runtime   is (RT mod 10000),
 4947	name(Runtime,RTChars),
 4948	name(EnvIdentifier,[FirstChar|RTChars]),
 4949	asserta_logged(environment(Name,env(EnvIdentifier),Comment)),
 4950	retractall_head(currentEnvironment(_)),
 4951	asserta_logged(currentEnvironment(env(EnvIdentifier))),
 4952	!.
 4953
 4954/**********************************************************************
 4955 *
 4956 * showEnvironment(+Name)
 4957 * 
 4958 */
 4959
 4960showEnvironment :- 
 4961	getCurrentEnvironment(Name),
 4962	showEnvironment(Name),
 4963	!.
 4964
 4965showEnvironment(EnvName) :-
 4966	environment(EnvName,Name,Comment),
 4967	write('Knowledge base '), 
 4968	write(EnvName), 
 4969	nl,
 4970	write('('),
 4971	write(Comment),
 4972	write(')'),
 4973	nl,
 4974	showModalAxioms(Name),
 4975	showDefprimconcept(Name),
 4976	showDefconcept(Name),
 4977	showDefprimrole(Name),
 4978	showDefrole(Name),
 4979	showDefclosed(Name),
 4980	showAssertConcept(Name),
 4981	showAssertRole(Name),
 4982	showFDW(Name),
 4983	!.
 4984
 4985showModalAxioms(Name) :-
 4986	modalAxioms(Name,user,K,C,MOp,A),
 4987	(nonvar(A) ; (A = C)),
 4988	write('        '), write('     modalAxioms('), write(K), write(','),
 4989	write(MOp), write(','), write(A), write(')'), nl,
 4990	fail.
 4991showModalAxioms(_) :-
 4992	!.
 4993showAssertConcept(Name) :-
 4994	clause(conceptElement(Name,MS,_,user,A,C,Ax),_),
 4995	write(Ax), write(':     assert_ind('), write(MS), write(','),
 4996	write(A), write(','), write(C), write(')'), nl,
 4997	fail.
 4998showAssertConcept(_) :-
 4999	!.
 5000showAssertRole(Name) :-
 5001	clause(roleElement(Name,MS,_,user,A,B,R,Ax),_),
 5002	write(Ax), write(':     assert_ind('), write(MS), write(','),
 5003	write(A), write(','), write(B), write(','), write(R), write(')'), nl,
 5004	fail.
 5005showAssertRole(_) :-
 5006	!.
 5007showDefconcept(Name) :-
 5008	conceptEqualSets(Name,user,MS,CN,CT,Ax),
 5009	write(Ax), write(':     defconcept('), write(MS), write(','),
 5010	write(CN), write(','), write(CT), write(')'), nl,
 5011	fail.
 5012showDefconcept(_Name) :-
 5013	!.
 5014showDefprimconcept(Name) :-
 5015	conceptSubsets(Name,user,MS,CN,CT,Ax),
 5016	write(Ax), write(': defprimconcept('), write(MS), write(','),
 5017	write(CN), write(','), write(CT), write(')'), nl,
 5018	fail.
 5019showDefprimconcept(_Name) :-
 5020	!.
 5021showDefrole(Name) :-
 5022	roleEqualSets(Name,user,MS,CN,CT,Ax),
 5023	write(Ax), write(':        defrole('), write(MS), write(','),
 5024	write(CN), write(','), write(CT), write(')'), nl,
 5025	fail.
 5026showDefrole(_Name) :-
 5027	!.
 5028showDefprimrole(Name) :-
 5029	roleSubsets(Name,user,MS,CN,CT,Ax),
 5030	write(Ax), write(':    defprimrole('), write(MS), write(','),
 5031	write(CN), write(','), write(CT), write(')'), nl,
 5032	fail.
 5033showDefprimrole(_Name) :-
 5034	!.
 5035showDefclosed(Name) :-
 5036	closed(Name,MS,X,Y,R),
 5037	write('axiom   '), write(':     defclosed('), write(MS), write(','),
 5038	write(X), write(','), write(Y), write(','), write(R), write(')'),
 5039	nl,
 5040	fail.
 5041showDefclosed(_Name) :-
 5042	!.
 5043
 5044
 5045/**********************************************************************
 5046 *
 5047 * removeEnvironment(+Name)
 5048 *
 5049 */
 5050
 5051removeEnvironment :-
 5052	getCurrentEnvironment(EnvName),
 5053	!,
 5054	removeEnvironment(EnvName).
 5055
 5056
 5057removeEnvironment(Name) :-
 5058	clearEnvironment(Name),
 5059	retractall_head(environment(Name,_,_)),
 5060	retract(currentEnvironment(Name)),
 5061	asserta_logged(currentEnvironment(env(e0))),
 5062	!.
 5063removeEnvironment(_Name) :-
 5064	% if we get here, Name was not the current environemt
 5065	!.
 5066
 5067/***********************************************************************
 5068 *
 5069 * clearEnvironment(Name)
 5070 *
 5071 */
 5072
 5073clearEnvironment :- 
 5074	getCurrentEnvironment(EnvName),
 5075	clearEnvironment(EnvName),
 5076	!.
 5077
 5078clearEnvironment(EnvName) :-
 5079	environment(EnvName,Env,_),
 5080	retractCompiledPredicates(Env),
 5081	retractallEnv(Env,in/9),
 5082	retractallEnv(Env,kb_in/10),
 5083	retractallEnv(Env,eq/9),
 5084	retractallEnv(Env,constraint/8),
 5085	retractallEnv(Env,rel/5),
 5086	retractallEnv(Env,closed/5),
 5087	retractallEnv(Env,compiledPredicate/2),
 5088	retractallEnv(Env,conceptElement/7),
 5089	retractallEnv(Env,conceptEqualSets/6),
 5090	retractallEnv(Env,conceptHierarchy/3),
 5091	retractallEnv(Env,conceptName/4),
 5092	retractallEnv(Env,conceptSubsets/6),
 5093	retractallEnv(Env,environment/3),
 5094	retractallEnv(Env,given_change/4),
 5095	retractallEnv(Env,given_inflLink/4),
 5096	retractallEnv(Env,modalAxioms/6),
 5097	retractallEnv(Env,roleAttributes/5),
 5098	retractallEnv(Env,roleDefault/4),
 5099	retractallEnv(Env,roleDefNr/4),
 5100	retractallEnv(Env,roleDomain/4),
 5101	retractallEnv(Env,roleElement/8),
 5102	retractallEnv(Env,roleEqualSets/6),
 5103	retractallEnv(Env,roleHierarchy/3),
 5104	retractallEnv(Env,roleName/4),
 5105	retractallEnv(Env,roleNr/5),
 5106	retractallEnv(Env,roleRange/4),
 5107	retractallEnv(Env,roleSubsets/6),
 5108	retractallEnv(Env,sub/4),
 5109	retractallEnv(Env,succ/4),
 5110	retractallEnv(Env,abductiveDerivation/3),
 5111	retractallEnv(Env,consistencyDerivation/3),
 5112	retractallEnv(Env,hypothesis/1),
 5113	retractallEnv(Env,inconsistencyCheck/3),
 5114	retractallEnv(Env,motel_option/2),
 5115	retractallEnv(Env,nsub/4),
 5116	retractallEnv(Env,nsub3/2),
 5117	retractallEnv(Env,sub3/2),
 5118	retractallEnv(Env,succ3/2),
 5119	!.
 5120
 5121/**********************************************************************
 5122 *
 5123 * retractCompiledPredicates(+Env)
 5124 * if the environment Env contains compiled predicates, then for each
 5125 * compiled predicate Pred there is a fact 
 5126 *                    compilePredicate(Env,Pred/Arity).
 5127 * So when the environment is to be removed, we just abolish the 
 5128 * compiled predicates.
 5129 *
 5130 */
 5131
 5132retractCompiledPredicates(Env) :-
 5133	compiledPredicate(Env,Pred/Arity),
 5134	abolish(Pred/Arity),
 5135	fail.
 5136retractCompiledPredicates(_) :-
 5137	!.
 5138
 5139
 5140/**********************************************************************
 5141 *
 5142 * initEnvironment(Name)
 5143 *
 5144 */
 5145
 5146initEnvironment :- 
 5147	getCurrentEnvironment(EnvName),
 5148	initEnvironment(EnvName),
 5149	!.
 5150
 5151initEnvironment(EnvName) :-
 5152	clearEnvironment(EnvName),
 5153	environment(EnvName,Env,_),
 5154	assert_logged(theory(Env,
 5155	[
 5156        (in([],P,pair(X,Y)) <== equal(X,Z), in([],P,pair(Z,Y))),
 5157	(in([],P,pair(X,Y)) <== equal(Y,Z), in([],P,pair(X,Z))),
 5158	(in([],C,X) <== equal(X,Y), in([],C,Y)),
 5159	(equal(X,Y) <== equal(Y,X)),
 5160	(equal(X,X) <== true),
 5161	(in(MS,'top',X) <== true)])),
 5162	assertInRules(Env),
 5163	% Assert equality axioms
 5164	assertEqRule(Env,1),
 5165	% Assert 'top' role
 5166skipped	assertEqRule(Env,2),
 5167	assertEqRule(Env,3),
 5168	% Proof by hypothesis for roles (Test 14.07.92)
 5169	assertEqRule(Env,4),
 5170	% Assert 'top' concept
 5171	assertInRule(Env,1),
 5172	% Assert 'bot' concept
 5173	assertInRule(Env,2),
 5174	% Proof by hypothesis for concepts
 5175	assertInRule(Env,3),
 5176	% Assert X in some(r,c) => X in atleast(1,r)
 5177skipped	gensym(axiom,AN11),
 5178skipped	assertInRule(Env,3,AN11),
 5179	% Assert X in atleast(1,r) => X in some(r,'top')
 5180skipped	assertInRule(Env,4,AN11),
 5181	% Assert X in atmost(0,r) => X in all(r,c)
 5182skipped	gensym(axiom,AN10),
 5183skipped	assertInRule(Env,1,AN10),
 5184	% Assert X in all(r,'bot') => X in atmost(0,r)
 5185skipped	assertInRule(Env,2,AN10),
 5186	% Assert not('top') law
 5187	% necessary for inconsistent knowledge bases?
 5188	% bad influence on runtime!
 5189skipped	assertInRule(Env,4),
 5190	% Assert double negation laws
 5191	gensym(axiom,AN6),
 5192skipped	assertInRule(Env,5,AN6),
 5193skipped	assertInRule(Env,6,AN6),
 5194	% Concrete domains
 5195	gensym(axiom,AN7),
 5196skipped	assertInRule(Env,7,AN7),
 5197skipped	assertInRule(Env,8,AN7),
 5198skipped	assertInRule(Env,9,AN7),