1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2%% $Id: tom.pl,v 1.3 1994/05/31 20:03:48 gerd Exp $ 3%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 4:- module(tom , []). 5/*%-------------------------------------- 6 7\input{tom_man} 8 9\PL*/ 10 11:- export(tom/2). 12 13:- module(tom). 14 15/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 16 17This is a magic cookie for identification. Dear user, don't you worry! 18 19\PL*/ 20 21info(filter,"1.1","Translation of multi-modal formulae into clause form"). 22 23/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 24 25A few general options are set... 26 27\PL*/ 28 29%:- get_flag(library_path,OldPath), 30% union(["/u/home/procom/System"],OldPath,FullPath), 31% set_flag(library_path,FullPath). 32 33:- set_flag(syntax_option,nl_in_quotes). 34 35other_prolog_libs:- 36 lib(lists), 37 lib(options), 38 lib(op_def), 39 lib(numbervars). 40 41:- op(500, fx, $). 42 43/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 44 45Now, we define an output option |'Tom:log_file'|. If this is set to |on|, the output of 46the filter will be written to a log file, the name of which results from 47the original name of the problem. This happens additionally to sending the 48output to a stream. 49\PL*/ 50:- define_option('Tom:log_file' = on). 51 52/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 53 54Furthermore, we set a global variable for the identification of the Skolem functions. 55\PL*/ 56:- setval(skolemCounter,1). 57 58/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 59 60Lastly, we declare a 61dynamic predicate. This is necessary as we assert the Prolog clauses 62of the theory part to the Prolog data base and flush the data base in the end. 63 64\PL*/ 65 66:- dynamic constraint/3. 67 68/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 69 70The global counter |current_depth| is somewhat fictional. This has been done 71to give the depth bound some limit. 72 73\PL*/ 74 75:- setval(current_depth,10000). 76 77/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 78 79We read the internal language of the system. If you don't like it, then provide 80your own. We suggest to use the filter |mpp.pl| prior to this one though 81(|tom.pl|, that is). 82 83\PL*/ 84 85:- compile('tom_ops.pl'). 86 87/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 88 89\Predicate tom/2(+InStream, +OutStream). 90 91This, being the main filter predicate, conforms to the \ProCom{} filter 92specification. In a 93failure-driven loop clauses are read from the stream |InStream|. 94A case split treats all (possible) events (well, the ones I could think of 95anyway). 96 97The first part of this clause sets up a frame for the rest. Several options 98are set to their default values. The \ProCom{} option |input_filter| is 99checked according to the option |'Tom:method'|. Furthermore, the latter 100option determines which file to compile for further processing. 101 102\PL*/ 103 104tom(InStream,OutStream) :- 105 is_option(input_file,InputFileNameAtom), 106 set_default_options, 107 ( is_option('Tom:method',constraints) -> 108 compile('tom_constraints.pl'), 109 is_option(input_filter,AListOfFilters), 110 ( member('constraints',AListOfFilters) -> 111 true 112 ; writeln(OutStream," 113*** Filter constraints not provided. Trying to fix this..."), 114 set_option(input_filter = constraints) 115 ) 116 ; compile('tom_inference.pl') 117 ), 118 ( is_option('Tom:log_file') -> 119 concat_atom(['...',InputFileNameAtom,'.pl'],File), 120 set_option('tee:file' = File), 121 is_option(input_filter,AnotherListOfFilters), 122 ( AnotherListOfFilters = [tom, AnyFilter | Tail], 123 ( AnyFilter = tee -> 124 true 125 ; set_option(input_filter = [tom, tee, AnyFilter | Tail]) 126 ) 127 ; set_option(input_filter = [tom, tee]) 128 ) 129 ; true 130 ), 131 setval(skolemCounter,1), 132 repeat, 133 read(InStream,Clause), 134/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 135 136If we encounter the end of the input file, we are done. 137\PL*/ 138 ( Clause = end_of_file -> 139 true 140 141/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 142It is possible to enter any clause in Prolog format. Thus the user 143can specify any kind of formula as an axiom. However, the reader 144has to make sure that all conventions are taken care of, especially 145the conventions concerning naming etc. The auxiliary predicate is 146always called |$Rmod| followed by an underscore and the name of an 147accessibility relation. These Prolog predicate names have to be quoted 148as there might be problems for the system in understanding names 149beginning with the |$| sign. 150\begin{description} 151\item[Example:] \begin{verbatim} 152# modal_axiom_formula(('$Rmod_a'(X + Y) :- 153 '$Rmod_a'(X), 154 '$Rmod_a'(Y))).\end{verbatim} 155\end{description} 156This is the formula for the transitivity of the accessibility relation |a|. 157No other things are done. We discourage the use of this option. 158 159\PL*/ 160 ; Clause = (# modal_axiom_formula(Axiom)) -> 161 find_type(Axiom,Type), 162 assert(constraint(Type,Axiom,matrix)), 163 fail 164 165/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 166Of course, there is the possibility of specifying one of the standard 167axioms of the accessibility relation of the modal logic (i.e.\ transitive, 168serial etc.) by using the command |# use_axiom_schema|. The name of the 169schema or its (usual) abbreviation, and in either case the sort this axiom 170refers to needs to be specified. No quotes are necessary but brackets. 171 172\begin{description} 173\item[Example:] \begin{verbatim} 174 # modal_axiom_schema(transitive, a). 175 \end{verbatim} 176%\Xsample{{\tt \# modal\_axiom\_schema(transitive,a).} 177In this clause, the transitivity of the accessibility relation |a| is 178specified. However, nothing else is done. 179\end{description} 180 181\PL*/ 182 ; Clause = (# modal_axiom_schema(Axiom,Sort)) -> 183 assert_axiom_schema(Axiom,Sort), 184 fail 185 186/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 187A third possibility provides the specification of one of the standard 188modal systems. Again, the corresponding sort has to be given. A list of all 189the known axiom schemas and theories will be presented later. 190 191If you want to use one of the standard modal logics, we suggest to use this 192form as all necessary options are set accordingly. 193 194\Xsample{{\tt \# modal\_standard\_theory(s4,a).} 195Here, the logic S4 is used for the accessibity relation |a|. Other possible 196logics are KD, KD4, KD5, KD45, KT, KT4, KT5, KT45, and S5.} 197 198At the moment, however, only the logics KD, KT4, and S4 are recognised. 199\PL*/ 200 ; Clause = (# modal_standard_theory(Theory, Sort)) -> 201 assert_theory(Theory,Sort), 202 fail 203 204/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 205In case we don't recognise any of the above commands we just write the 206entire line of the input file to the output file. After all, what do 207{\em we} know? 208 209\Xsample{{\tt \# this\_is\_a\_comment.} As it says \dots} 210 211\PL*/ 212 ; Clause = (# _) -> 213 writeclause(OutStream,Clause), 214 fail 215 216/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 217If we have a decent modal formula, we start a series of procedures. 218If a normal form is desired, we perform the predicate which was to be 219specified in the option |'Tom:normal_form'|. The default for this is the 220negation normal form. Then, the formula is translated into a list of clauses. 221These clauses are transformed into a Prolog format and put in the Prolog 222database, having the type |matrix|. 223\PL*/ 224 ; is_option('Tom:normal_form',NormalFormPredicate), 225 ( NormalFormPredicate = off -> 226 Clause = NormalFormula 227 ; Call_NF =.. [NormalFormPredicate, Clause, NormalFormula], 228 call(Call_NF) 229 ), 230 transform(NormalFormula, ClauseList), 231 ( member(Formula, ClauseList), 232 build_clause(Formula,FinalClause), 233 find_type(FinalClause,TypeOfClause), 234 assert(constraint(TypeOfClause,FinalClause,matrix)), 235 fail 236 ; true 237 ), 238 fail 239 240 ), 241 !, 242/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 243Now, the clauses from the Prolog database have to be written to |OutStream|. 244This is being carried out by the predicate |write_matrix/1|. The constraints 245are treated in the predicate |write_extras/1|. The exact definition of these 246two predicates is loaded according to the option |'Tom:method'|. Of course, 247the Prolog database is cleared at the end. 248\PL*/ 249 write_matrix(OutStream), 250 retract_all(constraint((_ / _),_,matrix)), 251 ( is_option('Tom:method',constraints) -> 252 write_extras(OutStream) 253 ; write_extras(InputFileNameAtom) 254 ), 255 retract_all(constraint((_ / _),_,_)). 256 257/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 258 259\Predicate transform/2(+Formula, -ClauseList). 260 261The binary predicate |transform| is a top level predicate for the following 262predicate of the same name. A number of initial parameters is set. 263This predicate has been introduced merely for legibility. Its result is 264a list of clauses representing the translated formula. However, the result 265is not complete in a sense that parts of the original formula cannot be found 266in the clauses as they were put into the theory part. 267 268\PL*/ 269 270transform(Formula, ClauseList):- 271 transform(Formula,0,[],ClauseList). 272 273/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 274\Predicate transform/4(+Formula, 275 ?PathTerm, 276 ?ClassicalVariables, 277 -ClauseList). 278 279 280To transform the modal formula |Formula| into a first order formula, free of 281modal operators. 282Hereby, new function symbols will be introduced, using the term representing 283the path information as an additional argument. 284 285The |PathTerm| is built during the translation process. |ClassicalVariables| 286is a list of the variables of the logic. This list is used for Skolemisation 287of existentially quantified variables. These variables can be either 288classical variables or variables introduced during translation. 289 290The Skolem counter which is important for a unique naming of the 291Skolem functions is a global variable, hence it does not occur in the 292arguments of the predicate. 293 294The translation is carried out accordingly to the algorithm presented 295in the PhD thesis of F. Debart. 296 297However, the difference to the proposed translation is, that the result of 298the predicate is a list of clauses rather than a translated formula. This is 299due to the fact that some parts of the translated formula would go into the 300theory part. We store these parts in an internal database at the moment we 301build them. Another issue is Skolemisation. It was possible to Skolemise 302while translating because we keep track of the governing universally 303quantified variables. Thus there is no need to produce a prenex normal form. 304 305\PL*/ 306 307/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 308\begin{description} 309\item[A variable] is easy to translate. 310\end{description} 311\PL*/ 312transform(Formula,_PathTerm,_ClassVars,[Formula]):- 313 var(Formula), 314 !. 315/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 316\begin{description} 317\item[The classical connectives] split the translation into two branches, 318 the results of which will be chucked together. 319 320 By using the |intersection| predicate, we achieve that the lists of 321 variables, |ClassVars1| and |ClassVars2|, contains only the variables 322 which occur in the formula to be translated. This has been introduced 323 to reduce the complexity of the Skolem functions to be introduced. 324\end{description} 325\PL*/ 326transform( and(Formula1,Formula2), PathTerm, ClassVars, Result):- 327 !, 328 term_variables(Formula1,Variables1), 329 term_variables(Formula2,Variables2), 330 intersection(Variables1,ClassVars,ClassVars1), 331 intersection(Variables2,ClassVars,ClassVars2), 332 transform(Formula1,PathTerm,ClassVars1,Intermediate1), 333 transform(Formula2,PathTerm,ClassVars2,Intermediate2), 334 append(Intermediate1,Intermediate2,Result). 335/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 336This works similar to the above. It had to be extended by a call of a merging 337predicate. This predicate can be specified in the option |'Tom:merging_predicate'|. 338The default for this option is |merge_clauses|. Any predicate can be used 339as long as it has an arity of three and the arguments are expected to be 340clause lists. 341\PL*/ 342transform( or(Formula1,Formula2), PathTerm, ClassVars,Result):- 343 !, 344 term_variables(Formula1,Variables1), 345 term_variables(Formula2,Variables2), 346 intersection(Variables1,ClassVars,ClassVars1), 347 intersection(Variables2,ClassVars,ClassVars2), 348 transform(Formula1,PathTerm,ClassVars1,Clauses1), 349 transform(Formula2,PathTerm,ClassVars2,Clauses2), 350 is_option('Tom:merging_predicate',MergePredicate), 351 Call =.. [MergePredicate, Clauses1, Clauses2, Result], 352 call(Call). 353/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 354\begin{description} 355\item[The negation] Here it becomes obvious why a negation normal form is 356desirable: the negation does not take into account any possibly occurring 357quantifiers and modal operators. 358\end{description} 359\PL*/ 360transform(not(Formula),PathTerm,_ClassVars,[not(Result)]):- 361 !, 362 ( var(Formula) -> 363 Result = Formula 364 ; Formula =.. [AnyPredicate | Arguments], 365 transform_arguments(Arguments, PathTerm, TransformedArguments), 366 ( name(AnyPredicate, [36,82 | _]) -> 367 Result =.. [AnyPredicate | TransformedArguments] 368 ; Result =.. [AnyPredicate, PathTerm | TransformedArguments] 369 ) 370 ). 371/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 372\begin{description} 373\item[The universal quantifier] 374 It is explained in greater detail, because the following clauses 375 tackle the problem very similar. 376 377 First of all we find out whether the quantified variable actually 378 occurs in the formula. If it doesn't, we simply proceed on the formula. 379 380 If the variable does occur in the formula, we copy the formula to 381 achieve a unique variable naming. 382 Therefore, we collect all the variables, copy the whole formula, 383 and unify nearly all the old and new variables, except for the quantified 384 variable. Then, the list of classical variables is extended and the 385 rest of the formula ist transformed. We used the newly introduced 386 variables to avoid confusion about variable naming. 387\end{description} 388\PL*/ 389transform(forall(:(Var, Formula1)),PathTerm,ClassVars, Result):- 390 !, 391 term_variables(Formula1,VarList), 392 ( member(Var,VarList) -> 393 copy_term(Formula1 + VarList, NewFormula1 + CopyVarList), 394 unify_partially(VarList,CopyVarList,Var), 395 NewClassVars = [Var | ClassVars], 396 transform(NewFormula1,PathTerm,NewClassVars,Result) 397 ; transform(Formula1,PathTerm,ClassVars,Result) 398 ). 399/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 400\begin{description} 401\item[The existential quantifier] 402 works similar. We take into account that we introduce a new skolem 403 function (named '|$kolemN|', where N stands for a unique number, taken 404 from the global variable |skolemCounter|. 405 406 Otherwise, the same term copying idea as for the universal quantifier 407 applies. 408 409 Additionally, the handling of the skolem counter is introduced. 410 The value of the global variable |skolemCounter| is read, stored in a 411 variable which in turn is used for generating the name of the Skolem 412 function. Then, the value of the variable is incremented. 413\end{description} 414\PL*/ 415transform(exists(:(Var, Formula1)),PathTerm,ClassVars, Intermediate):- 416 !, 417 term_variables(Formula1,VarList), 418 copy_term(Formula1 + VarList + Var, 419 NewFormula1 + CopyVarList + NewVar), 420 unify_partially(VarList,CopyVarList,Var), 421 getval(skolemCounter,Value), 422 incval(skolemCounter), 423 concat_atom(['$kolem',Value],NewFunctionSymbol), 424 transform(NewFormula1,PathTerm,ClassVars,Intermediate), 425 NewVar =.. [NewFunctionSymbol, PathTerm | ClassVars ]. 426/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 427\begin{description} 428\item[The multi-modal box operator] 429 The sort of the modality is indicated by an atom (well, it is 430 supposed to anyway) followed by a colon and the formula the modal 431 operator refers to. 432 As this predicate is understood as being a premise of a conclusion 433 (is it a constraint on a universally quantified variable), it has to 434 be prepended to the clauses which result from the translation of the 435 rest of the formula. 436\end{description} 437\PL*/ 438transform(box(:(Sort,Formula1)),PathTerm,ClassVars, Result):- 439 !, 440 NewPath = PathTerm + X, 441 concat_atom(['$Rmod_',Sort],NewSymbol), 442 AuxFunction =.. [NewSymbol, X], 443 transform(Formula1,NewPath,ClassVars, Intermediate), 444 process_premise(Intermediate,Result,AuxFunction). 445/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 446\begin{description} 447\item[The mono-modal box operator] 448 applies the same ideas as above. The argument |PathTerm| is extended by 449 a newly generated variable, and the rest of the formula will be 450 translated. 451\end{description} 452\PL*/ 453transform(box(Formula1),PathTerm,ClassVars, Intermediate):- 454 !, 455 NewPath =.. ['+', PathTerm, _ ], 456 transform(Formula1,NewPath,ClassVars, Intermediate). 457/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 458\begin{description} 459\item[The modal diamond operator] 460 is basically the same, just mixes the principles of a modal operator 461 together with Skolemisation. Suitably enough, the Skolem functions here 462 are called |$kolemPath|, thus enabling to distinguish later, where they 463 come from. 464 465 As the predicate introduced in this clause is a constraint on an 466 existentially quantified variable, it is a conjunct to the rest 467 of the formula. As this conjunct forms a clause on its own and 468 it consists of the auxiliary predicate only, it belongs to the 469 theory part of the problem. Hence, this clause is stored in the 470 Prolog database with the type |theory|. If the option |'Tom:method'| 471 is set to |inference|, this clause is still part of the matrix. 472\end{description} 473\PL*/ 474transform(diamond(:(Sort, Formula1)),PathTerm,ClassVars, Intermediate):- 475 !, 476 getval(skolemCounter,Value), 477 incval(skolemCounter), 478 concat_atom(['$kolemPath',Value],NewPathFunctionSymbol), 479 NewFunction =.. [NewPathFunctionSymbol, PathTerm | ClassVars], 480 NewPath = PathTerm + NewFunction, 481 concat_atom(['$Rmod_',Sort],NewSymbol), 482 AuxFunction =.. [NewSymbol, NewFunction], 483 ( is_option('Tom:method',inference) -> 484 assert(constraint((NewSymbol / 1),AuxFunction,matrix)) 485 ; assert(constraint((NewSymbol / 1),AuxFunction, theory)) 486 ), 487 transform(Formula1,NewPath,ClassVars, Intermediate). 488/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 489\begin{description} 490\item[The mono-modal diamond operator] is a simplified case of the multi-modal 491 operator. Here, simply the |PathTerm| is extended. 492\end{description} 493\PL*/ 494transform(diamond(Formula1),PathTerm,ClassVars, Intermediate):- 495 !, 496 getval(skolemCounter,Value), 497 incval(skolemCounter), 498 concat_atom(['$kolemPath',Value],NewPathFunctionSymbol), 499 NewFunction =.. [NewPathFunctionSymbol , PathTerm | ClassVars], 500 NewPath = PathTerm + NewFunction, 501 transform(Formula1,NewPath,ClassVars, Intermediate). 502/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 503\begin{description} 504\item[An arbitrary function or predicate symbol (rigid and non-rigid)] 505 If we don't find any of the known operators of the language, we 506 have to treat the operator in a very boring way: we translate the 507 arguments but not the operator symbol. 508\end{description} 509\PL*/ 510transform(Formula,PathTerm,_ClassVars, [Result]):- 511 Formula =.. [AnyPredicate | ArgList], 512 !, 513 transform_arguments(ArgList,PathTerm,TransformedArgs), 514 ( name(AnyPredicate, [36,82 | _]) -> 515 Result =.. [AnyPredicate | TransformedArgs] 516 ; Result =.. [AnyPredicate , PathTerm | TransformedArgs] 517 ). 518/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 519This predicate performs the translation on the arguments of a predicate or 520function symbols. The implemented strategy is a recursion on the list of 521arguments. 522\PL*/ 523transform_arguments([],_PathTerm,[]). 524 525transform_arguments([H|T],PathTerm,[NH|NT]):- 526 transform_single_argument(H,PathTerm,NH), 527 transform_arguments(T,PathTerm,NT). 528/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 529This predicate translates a term of the language. If the term is a variable, 530then the result of the translation yields the variable again. If it is a 531constant or a function symbol, it has to be examined whether it is flexible 532or rigid. In the former case, one argument will be added to the argument list. 533\PL*/ 534transform_single_argument(X,_P,X):- 535 var(X), 536 !. 537 538transform_single_argument(Term, PathTerm, TransformedTerm):- 539 Term =.. [Function | Arguments], 540 transform_arguments(Arguments, PathTerm, TransformedArguments), 541 ( name(Function, [36,82 | _]) -> 542 TransformedTerm =.. [Function | TransformedArguments] 543 ; TransformedTerm =.. [Function, PathTerm | TransformedArguments] 544 ). 545/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 546 547\Predicate process_premise/3 (+InClauseList, -OutClauseList, +Premise). 548 549This predicate is used to prepend the clauses from |InCLauseList| with 550the |Premise|. If the clause is an implication already, we make the 551premise more complex. Otherwise, the new clause becomes an implication. 552 553\PL*/ 554 555process_premise([],[],_Constraint). 556 557process_premise([H | T],[NH | NT],Constraint):- 558 ( H = implies(Premise, Conclusion) -> 559 NH = implies(and(Constraint, Premise), Conclusion) 560 ; NH = implies(Constraint, H) 561 ), 562 process_premise(T, NT, Constraint). 563 564/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 565 566\Predicate unify_partially/3(+VarList, -CopyVarList, +Variable). 567 568This is an auxiliary predicate used to copy lists of veriables, 569which may be necessary to avoid erroneous unifications of the systems. 570 571We take the |VarList|. All variables which are identically to |Variable| are fine, 572if they are not identical, we unify the corresponding heads of the lists. 573This is to unify nearly every old variable with the new ones, {\em but not} 574the newly introduced variable. 575 576\PL*/ 577 578unify_partially([],[],_). 579 580unify_partially([H|T],[H1|T1],Var):- 581 (H == Var -> 582 true 583 ; H = H1 584 ), 585 unify_partially(T,T1,Var). 586 587/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 588 589\Predicate build_clause/2 (+Clause, -PrologClause). 590 591This is a simple but powerful predicate is to transform a |Clause| from 592our internal format into a |PrologClause|, a clause in a Prolog like 593format. 594 595\PL*/ 596 597build_clause(and(F1,F2),(BF1,BF2)):- 598 !, 599 build_clause(F1,BF1), 600 build_clause(F2,BF2). 601 602build_clause(or(F1,F2),(BF1;BF2)):- 603 !, 604 build_clause(F1,BF1), 605 build_clause(F2,BF2). 606 607build_clause(implies(F1,F2),(BF2 :- BF1)):- 608 !, 609 build_clause(F1,BF1), 610 build_clause(F2,BF2). 611 612build_clause(not(F1),-BF1):- 613 !, 614 build_clause(F1,BF1). 615 616build_clause(F,F). 617 618/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 619 620\Predicate find_type/2 (+Clause, -Type). 621 622We attempt to find the main function name and the arity of the head 623literal of the clause. This is important for a well ordered output of 624all the clauses. We collect function name and arity in a pair called |Type|. 625\PL*/ 626 627find_type(Variable, (variable / 0)):- 628 var(Variable), 629 !. 630 631find_type((Head :- _Tail), Type):- 632 !, 633 find_type(Head, Type). 634 635find_type((Literal1;_Literal2), Type):- 636 !, 637 find_type(Literal1, Type). 638 639find_type( -(Literal), Type):- 640 !, 641 find_type(Literal, Type). 642 643find_type(Literal, (Functor / Arity)):- 644 functor(Literal,Functor,Arity). 645 646/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 647 648The following part contains predicates dealing with the theory not depending 649on the particular problem, i.e.\ formula(e). 650 651We provide the opportunity to use a standard axiom schema. As it is 652known, there are modal axioms characterising a property of an 653accessibility relation. The name of the property (in teletype font) 654can be used to specify this axiom schema. 655%For some of the schemas, abbreviations are common. 656The following table contains a survey of which 657properties and which abbreviations are known to the system: 658 659\makevertother 660\begin{center} 661\begin{tabular}{l|c|l} 662property of the & permitted & corresponding \\ 663accessibility relation & abbreviation & modal axiom schema \\ 664 \hline 665{\tt transitive} & {\tt 4} & \( \Box \varphi \to \Box \Box \varphi\)\\ 666{\tt euclidean} & {\tt 5} & \( \diamond \varphi \to \Box \diamond \varphi\)\\ 667%{\tt symmetric} & {\tt b} & \( \varphi \to \Box \diamond \varphi\\ 668%{\tt serial} & {\tt d} & \( \Box \varphi \to \diamond \varphi\)\\ 669{\tt reflexive} & {\tt t} & \( \Box \varphi \to \varphi\)\\ 670%{\tt partly\_functional} & {\tt pf} & \( \diamond \varphi \to \Box \varphi\)\\ 671%{\tt functional} & {\tt f} & \( \diamond \varphi \to \Box \varphi\)\\ 672%{\tt weakly\_dense } & {\tt wd} & \( \Box \Box \varphi \to \Box \varphi\)\\ 673%{\tt weakly\_connected} & {\tt wc} & \( \Box((\varphi_2 \wedge \Box \varphi_2) \to \varphi_1) \vee \Box((\varphi_1 \wedge \Box \varphi_1) \to \varphi_2)\)\\ 674%{\tt connected} & {\tt c} & \( \Box (\Box \varphi_2 \to \varphi_1) \vee \Box(\Box \varphi_1 \to \varphi_2)\)\\ 675%{\tt weakly\_directed} & {\tt wi} & \( \diamond \Box \varphi \to \Box \diamond \varphi \) 676\end{tabular} 677\end{center} 678\makevertactive 679 680 681Together with an axiom schema, the user has to specify which sort this schema 682refers to (because we are dealing with multi-modal logics). Thus it is 683possible to specify for each sort exactly the accessibility relation we want. 684 685There are two more axiom schemas which can be specified: the {\tt interaction} 686schema and the {\tt total} schema. The former states an inclusion relation 687between two accessibility relations (hence it is of any interest in a multi-modal case only) and the latter schema states that the relation is total. 688 689It is planned to include many more axioms for greater flexibility of this 690module. 691\PL*/ 692 693assert_axiom_schema(interaction,[H,T]):- 694 concat_atom(['$Rmod_',H],Functor1), 695 Rel1 =.. [Functor1, Var], 696 concat_atom(['$Rmod_',T],Functor2), 697 Rel2 =.. [Functor2, Var], 698 assert(constraint((Functor2 / 1),(Rel2 :- Rel1),interaction)). 699 700assert_axiom_schema(4,Sort):- 701 concat_atom(['$Rmod_',Sort],Functor), 702 Rel1 =.. [Functor, Var1], 703 Rel2 =.. [Functor, Var2], 704 Rel3 =.. [Functor, Var1 + Var2], 705 assert(constraint((Functor / 1),(Rel3 :- (Rel1,Rel2)),transitive)). 706 707assert_axiom_schema(transitive,Sort):- 708 concat_atom(['$Rmod_',Sort],Functor), 709 Rel1 =.. [Functor, Var1], 710 Rel2 =.. [Functor, Var2], 711 Rel3 =.. [Functor, Var1 + Var2], 712 assert(constraint((Functor / 1),(Rel3 :- (Rel1,Rel2)),transitive)). 713 714assert_axiom_schema(5,Sort):- 715 concat_atom(['$Rmod_',Sort],Functor), 716 Rel1 =.. [Functor1, Var1], 717 Rel2 =.. [Functor1, Var2], 718 Rel3 =.. [Functor1, Var1 + Var2], 719 assert(constraint((Functor / 1),(Rel2 :- (Rel1, Rel3)),euclidean)). 720 721assert_axiom_schema(euclidean,Sort):- 722 concat_atom(['$Rmod_',Sort],Functor), 723 Rel1 =.. [Functor1, Var1], 724 Rel2 =.. [Functor1, Var2], 725 Rel3 =.. [Functor1, Var1 + Var2], 726 assert(constraint((Functor / 1),(Rel2 :- (Rel1, Rel3)),euclidean)). 727 728%assert_axiom_schema(b,Sort):- 729% concat_atom(['$Rmod_',Sort],Functor), 730% ... 731% assert(constraint((Functor / Arity),AxiomClause,Type)). 732 733%assert_axiom_schema(symmetric,Sort):- 734% concat_atom(['$Rmod_',Sort],Functor), 735% ... 736% assert(constraint((Functor / Arity),AxiomClause,Type)). 737 738%assert_axiom_schema(d,Sort):- 739% concat_atom(['$Rmod_',Sort],Functor), 740% ... 741% assert(constraint((Functor / Arity),AxiomClause,Type)). 742 743%assert_axiom_schema(serial,Sort):- 744% concat_atom(['$Rmod_',Sort],Functor), 745% ... 746% assert(constraint((Functor / Arity),AxiomClause,Type)). 747 748assert_axiom_schema(t,Sort):- 749 concat_atom(['$Rmod_',Sort],Functor), 750 ( is_option('Tom:method' ,inference) -> 751 Type = matrix 752 ; Type = reflexive 753 ), 754 Relation =.. [Functor, 0], 755 assert(constraint((Functor / 1),Relation,Type)). 756 757assert_axiom_schema(reflexive,Sort):- 758 concat_atom(['$Rmod_',Sort],Functor), 759 ( is_option('Tom:method' ,inference) -> 760 Type = matrix 761 ; Type = reflexive 762 ), 763 Relation =.. [Functor, 0], 764 assert(constraint((Functor / 1),Relation,Type)). 765 766assert_axiom_schema(total,Sort):- 767 concat_atom(['$Rmod_',Sort],Functor), 768 ( is_option('Tom:method', inference) -> 769 Type = matrix 770 ; Type = total 771 ), 772 concat_atom(['$kolemPath_',Sort],Constant), 773 Relation =.. [Functor, Constant], 774 assert(constraint((Functor / 1),Relation,Type)). 775 776/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 777% T : box A imp A 778% reflexivity 779% forall w_1 : w_1 K w_1 780 781% B : A imp box diamond A 782% symmetry 783% forall w_1, w_2 : w_1 K w_2 implies w_2 K w_1 784 785% 4 : box A imp box box A 786% transitivity 787% forall w_{1,2,3} : w_1 K w_2 and w_2 K w_3 imp w_1 K w_3 788 789% 5 : diamond A imp box diamond A 790% euclidean 791% forall w_{1,2,3} : w_1 K w_2 and w_1 K w_3 imp w_2 K w_3 792 793% PF: diamond A imp box A 794% partly functional 795% forall w_{1,2,3} : w_1 K w_2 and w_1 K w_3 imp w_2 = w_3 796 797% F : diamond A imp box A 798% functional 799% forall w_1 exists! w_2 : w_1 K w_2 800 801% WD: box box A imp box A 802% weakly dense 803% forall w_{1,2} : w_1 K w_2 imp (exists w_3 : w_1 K w_3 and w_3 K w_2) 804 805% WC: box((B and box B) imp A) or box((A and box A) imp B) 806% weakly connected 807% forall w_{1,2,3} : w_1 K w_2 and w_1 K w_3 imp w_2 K w_3 or 808% w_3 K w_2 or 809% w_2 = w_3 810 811% C : box (box B imp A) or box(box A imp B) 812% connected 813% forall w_{1,2,3} : w_1 K w_2 and w_1 K w_3 imp w_2 K w_3 or w_3 K w_2 814 815% WI: diamond box A imp box diamond A 816% weakly directed 817% forall w_{1,2,3} : w_1 K w_2 and w_1 K w_3 imp 818% (exists w_4 : w_2 K w_4 and w_3 K w_4) 819\PL*/ 820 821/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 822 823\Predicate assert_theory/3 (+OutStream, +Theory, +Sort). 824 825This is an output predicate providing the opportunity to specify one of the 826classical modal theories |Theory| for the sort |Sort|. This theory will be 827written to |OutStream|. The following theories are known at the moment: 828%{\tt k, k5, k4, kb, 829%kd, k45, kdb, kt, kd4, kd5, kb4, ktb, kt4} (also known as {\tt s4}), {\tt kd45, 830%kt5} (also known as {\tt s5}). However, only for the theories 831{\tt s4} ({\tt kt4}) and {\tt kd}. All the options, such as unification and 832path normalisation, are set accordingly. 833 834It is also possible to concatenate the letters of the axioms. The result is an 835atom, for instance {\tt k4}, {\tt kb5}, etc. However, the user should bear in 836mind that all the necessary options must bet set by himself then. 837 838\PL*/ 839 840assert_theory(s4,Sort):- 841 set_option('Tom:special_path_term' = normalize_path), 842 set_option('Tom:special_unification' = normalize_unify_a1), 843 set_option('ProCom::post_link' = ['normalize_unify_a1.pl']), 844 assert_axiom_schema(t,Sort), 845 assert_axiom_schema(4,Sort). 846 847assert_theory(kt4,Sort):- 848 set_option('Tom:special_path_term' = normalize_path), 849 set_option('Tom:special_unification' = normalize_unify_a1), 850 set_option('ProCom::post_link' = ['normalize_unify_a1.pl']), 851 assert_axiom_schema(t,Sort), 852 assert_axiom_schema(4,Sort). 853 854assert_theory(s5,Sort):- 855% set_option('Tom:special_path_term' = normalize_path), 856% set_option('Tom:special_unification' = normalize_unify_a1), 857% set_option('ProCom::post_link' = ['normalize_unify_a1.pl']), 858 assert_axiom_schema(t,Sort), 859 assert_axiom_schema(5,Sort). 860 861assert_theory(kt5,Sort):- 862% set_option('Tom:special_path_term' = normalize_path), 863% set_option('Tom:special_unification' = normalize_unify_a1), 864% set_option('ProCom::post_link' = ['normalize_unify_a1.pl']), 865 assert_axiom_schema(t,Sort), 866 assert_axiom_schema(5,Sort). 867 868assert_theory(kd,_Sort):- 869 set_option('Tom:special_path_term' = off), 870 set_option('Tom:special_unification' = off). 871 872%assert_theory(kt,Sort):- 873% set_option('Tom:special_path_term' = off), 874% set_option('Tom:special_unification' = unify_1), 875% set_option('ProCom::post_link' = ['unify_1.pl']), 876% assert_axiom_schema(t,Sort). 877 878%assert_theory(kd4,Sort):- 879% set_option('Tom:special_path_term' = normalize_path), 880% set_option('Tom:special_unification' = normalize_unify_a), 881% set_option('ProCom::post_link' = ['normalize_unify_a.pl']), 882% assert_axiom_schema(4,Sort). 883 884%assert_theory(kd5,Sort):- 885% set_option('Tom:special_path_term' = ????), 886% set_option('Tom:special_unification' = ????), 887% assert_axiom_schema(5,Sort). 888 889%assert_theory(kd45,Sort):- 890% set_option('Tom:special_path_term' = ????), 891% set_option('Tom:special_unification' = ????), 892% assert_axiom_schema(4,Sort), 893% assert_axiom_schema(5,Sort) 894 895assert_theory(Theory,Sort):- 896 name(Theory, TheoryStringList), 897 assert_theory_aux(TheoryStringList,Sort). 898 899assert_theory_aux([],_Sort). 900 901assert_theory_aux([H | T],Sort):- 902 name(AxiomName,[H]), 903 assert_axiom_schema(AxiomName, Sort), 904 assert_theory_aux(T, Sort). 905 906/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 907 908\Predicate set_default_options/0 (none). 909 910This predicate provides the following \ProCom{} options: 911 912\makevertother 913\begin{center} 914\begin{tabular}{l|l|l} 915 & option name & currently recognised values \\ \hline 9161. & {\tt 'Tom:method'} & {\tt constraints}, \underline{{\tt inference}} \\ 9172. & {\tt 'Tom:merging\_predicate'} & {\tt off}, \underline{{\tt 918merge\_clauses}} \\ 9193. & {\tt 'Tom:normal\_form'} & {\tt off}, \underline{{\tt 920negation\_normal\_form}} \\ 9214. & {\tt 'Tom:special\_path\_term'} & {\tt off}, \underline{{\tt 922normalize\_path}} \\ 9235. & {\tt 'Tom:special\_unification'} & {\tt off}, \underline{{\tt 924normalize\_unify\_a1}} \\ 9256. & {\tt 'Tom:log\_file'} & {\tt off}, \underline{{\tt on}} \\ 926(7.) & ({\tt 'Tom:theory\_optimization'}) & ({\tt off}, \underline{{\tt on}}) 927\end{tabular} 928\end{center} 929\makevertactive 930 931The options are examined whether they are defined already. If they are not 932defined, they will be defined and set to the default values. Default values are 933the logic S4, i.e.\ a path normalization, a A1-unification, a negation normal 934form, and the usual merging predicate. This refers to the underlined values in 935the table. 936 937The implementation uses a failure driven loop on the list |OptionList| that 938contains pairs consisting of an option name and its default value. 939 940In a second loop, the files providing the predicates are loaded. 941\PL*/ 942set_default_options:- 943 OptionList = [('Tom:method',inference), 944 ('Tom:merging_predicate',merge_clauses), 945 ('Tom:normal_form',negation_normal_form), 946 ('Tom:special_path_term',normalize_path), 947 ('Tom:special_unification',normalize_unify_a1)], 948 ( member((OptionName,DefaultValue),OptionList), 949 ( is_option(OptionName,_AnyValue) 950 ; define_option(OptionName = DefaultValue) 951 ), 952 fail 953 ; true 954 ), 955 ( member(Option,['Tom:merging_predicate', 956 'Tom:normal_form']), 957 is_option(Option,Value), 958 ( Value = off -> 959 true 960 ; concat_atom([Value,'.pl'],FullFileName), 961 compile(FullFileName) 962 ), 963 fail 964 ; true 965 ), 966 ( is_option('Tom:method',constraints) -> 967 define_option('Tom:theory_optimization' = on) 968 ; true 969 ). 970 971/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 972 973The following predicate is for testing purposes only. 974Its meaning should be evident. 975 976\PL*/ 977tm_file_to_file(Infile,Outfile) :- 978 open(Infile,read,Stream), 979 ( Outfile = '' -> 980 tom(Stream,output) 981 ; open(Outfile,write,OutStream), 982 tom(Stream,OutStream), 983 close(OutStream) 984 ), 985 close(Stream). 986/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 987 988\EndProlog */