1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%% $Id: translate_modal.pl,v 1.3 1994/05/31 20:03:48 gerd Exp $
    3%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    4
    5:- module_interface(translate_modal). /*%--------------------------------------
    6
    7Written by Zoltan Rigo.\bigskip
    8
    9This module implements The translation of modal formulae into
   10first order formulae with terms representing the paths.
   11This has been done according to the translation proposed in
   12
   13Francoise Clerin-Debart
   14Theories equationelles et de contraintes pour la demonstration
   15automatique en logique multi-modale
   16PhD Thesis
   17Caen University, France,
   181992
   19
   20\PL*/
   21:- export translate_modal/2.
   22
   23:- begin_module(translate_modal).   24/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   25
   26Do we need all of those?
   27
   28\PL*/
   29
   30:-      get_flag(library_path,OldPath),
   31	union(["/u/home/procom/System"],OldPath,FullPath),
   32	set_flag(library_path,FullPath).   33
   34:-	lib(lists),
   35        lib(options).   36
   37
   38/*Pl%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   39
   40We introduce ihe input language to the system.
   41
   42The language should agree with the language of the problem
   43collection to be developed. Similarly, the precedences require some more work.
   44
   45\PL*/
   46
   47:- op(1100, xfy, 'implies').   48:- op(1000, xfy, 'and').      %    Otter: op(780, , &).
   49:- op(1050, xfy, 'or').       %           op(790, , |).
   50:- op( 400,  fy, 'not').      %           op(500, , -).
   51
   52:- op( 600,  fy, 'forall').   %           op(?, ?, all).
   53:- op( 600,  fy, 'exists').   %           op(?, ?, exists).
   54
   55:- op( 600,  fy, 'box').      % 
   56:- op( 600,  fy, 'diamond').  % (precedence of : is 600)
   57
   58
   59/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   60
   61Firstly, we define an output option. This is not yet set into power (25/8/94)
   62but this is supposed to become a kind of default.
   63Then we set a global variable for the identification of the Skolem functions.
   64
   65\PL*/
   66
   67:- define_option 'translate_modal:output_file' = '...translated_modals.ppp'.
   68
   69:-setval(skolemCounter,1).   70
   71
   72/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   73
   74\Predicate translate_modal/2(+InStream, +OutStream).
   75
   76This predicate conforms to the \ProCom{} filter specification. In a
   77failure-driven loop clauses are read form the stream |InStream|.
   78After transforming the clause into its negated normalform, the modal formula
   79will be translated.
   80
   81
   82
   83\PL*/
   84
   85translate_modal(Stream,OutStream) :-
   86        is_option('translate_modal:output_file',File),
   87	open(File,write,CSTStream),
   88        repeat,
   89	read(Stream,Clause),
   90	( Clause = end_of_file ->
   91	    true
   92
   93%%%	; Clause = (# _) ->
   94%%%	   writeclause(OutStream,Clause),
   95%%%	   fail
   96
   97	; make_nnf(Clause,0,NormalClause),
   98	  transform(NormalClause,TranslatedClause),
   99          normalize_path(TranslatedClause,NormalizedClause),
  100	  printf(OutStream,"%vQDMw.\n",[NormalizedClause]),
  101          fail
  102	),
  103	close(CSTStream),
  104	( current_module('modal logic') ->
  105	    true
  106	;   create_module('modal logic')
  107        ),
  108	call(compile(File),'modal logic'),
  109	!.
  110/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  111
  112\Predicate transform/2(+Formula, -TranslatedFormula),
  113
  114The binary predicate |transform| is a top level predicate for the following
  115predicate of the same name. A number of initial parameters is set.
  116This predicate has been introduced merely for legibility.
  117
  118\PL*/
  119
  120
  121transform(Formula, TranslatedFormula):-
  122	transform(0,Formula,[],[],TranslatedFormula).
  123
  124
  125/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  126\Predicate transform/5(?PathTerm,
  127                       +Formula,
  128                       ?ClassicalVariables
  129                       ?PathVariables,
  130                       -TranslatedFormula),
  131
  132
  133To transform the |Formula|, which is assumed to be a modal formula in negation
  134normal form, into a 1st order formula, free of modal operators.
  135Hereby, new function symbols will be introduced, using the term representing
  136the path information as an additional argument.
  137
  138The |PathTerm| is built during the translation process. |ClassicalVariables|
  139is a list of the variables of the logic, |PathVariables| is a list of the
  140path variables. 
  141The skolem counter is a global variable, hence it does not occur in the
  142arguments of the predicate.
  143
  144The translation is carried out according to the algorithm presented in the
  145thesis.
  146
  147\PL*/
  148
  149transform(PathTerm,Formula,ClassVars,PathVars,Result):-
  150    (
  151
  152/*PL  A variable is really easy to translate... \PL*/
  153
  154      var(Formula) ->
  155        Result = Formula
  156
  157
  158/*PL The classical connectives split the translation into two branches, the
  159 results of which will be chucked together. \PL*/
  160
  161     ; Formula =.. [implies, Formula1, Formula2] ->
  162	make_nnf(not Formula1, 0, NewFormula),
  163	transform(PathTerm,NewFormula,ClassVars,PathVars,Intermediate1),
  164	transform(PathTerm,Formula2,ClassVars,PathVars,Intermediate2),
  165	Result =.. ['or', Intermediate1, Intermediate2]
  166
  167     ; Formula =.. [and, Formula1, Formula2] ->
  168	transform(PathTerm,Formula1,ClassVars,PathVars,Intermediate1),
  169        transform(PathTerm,Formula2,ClassVars,PathVars,Intermediate2),
  170        Result =.. ['and', Intermediate1, Intermediate2]
  171
  172     ; Formula =.. [or, Formula1, Formula2] ->
  173        transform(PathTerm,Formula1,ClassVars,PathVars,Intermediate1),
  174        transform(PathTerm,Formula2,ClassVars,PathVars,Intermediate2),
  175        Result =.. ['or', Intermediate1, Intermediate2]
  176
  177/*PL Here it becomes obvious why a negation normalform is required:
  178 The negation does not take into account possibly occuring
  179 quantifiers and modal operators. \PL*/
  180
  181     ; Formula =.. [not, Formula] ->
  182        transform(PathTerm,Formula,ClassVars,PathVars,Intermediate),
  183        Result =.. ['not', Intermediate]
  184
  185
  186/*PL The universal quantifier.\\
  187
  188 It is explained in greater detail, because the following clauses
  189 tackle the problem very similar.
  190
  191 At first we copy the formula to achieve a unique variable naming.
  192 Therefore, we collect all the variables, copy the whole formula,
  193 and unify nearly all the old and new variables, except for the quantified
  194 variable.\PL*/
  195
  196     ; Formula =.. [forall, :(Var, Formula1)] ->
  197        term_variables(Formula1,VarList),
  198        copy_term(Formula1 + VarList, NewFormula1 + CopyVarList),
  199        drei(VarList,CopyVarList,Var),
  200
  201/*PL We extend the list of the classical variables...\PL*/
  202
  203        NewClassVars = [Var | ClassVars],
  204
  205/*PL And transform the formula...\\
  206 In the formula, we use the new variables (variable names) to avoid 
  207 confusion about variable naming.\PL*/
  208
  209        transform(PathTerm,NewFormula1,NewClassVars,PathVars,Intermediate),
  210        Result = Intermediate
  211
  212/*PL The existential quantifier\\
  213
  214 ... works similar. We take into account that we introduce a new skolem
  215 function (named '$kolemN', where N stands for a unique number, taken from
  216 the global variable skolemCounter.
  217
  218 Otherwise, the same term copying idea as for the universal quantifier
  219 applies.
  220
  221 Additionally, the handling of the skolem counter is introduced.
  222 The value of the global variables skolemCounter is read, stored in a
  223 variable which in turn is used for generating the name of the skolem
  224 function. Then, the value of the variable is incremented.\PL*/
  225
  226     ; Formula =.. [exists, :(Var, Formula1)] ->
  227        term_variables(Formula1,VarList),
  228        copy_term(Formula1 + VarList + Var,NewFormula1 + CopyVarList + NewVar),
  229        drei(VarList,CopyVarList,Var),
  230	getval(skolemCounter,Value),
  231	incval(skolemCounter),
  232        concat_atom(['$kolem',Value],NewFunctionSymbol),
  233        append([PathTerm], ClassVars, Arguments),
  234	transform(PathTerm,NewFormula1,ClassVars,PathVars,Intermediate),
  235        NewVar =.. [NewFunctionSymbol | Arguments ],
  236        Result = Intermediate
  237
  238/*PL The modal box operator\\
  239
  240... applies the same ideas as above. The term PathTerm is extended by
  241 a newly generated variable, and the rest of the formula will be translated.
  242\PL*/
  243
  244     ; Formula =.. [box, Formula1] ->
  245        NewPath =.. ['+', PathTerm, X ],
  246        NewPathVars = [ X | PathVars ],
  247        transform(NewPath,Formula1,ClassVars,NewPathVars,Intermediate),
  248        Result = Intermediate
  249
  250/*PL The modal diamond operator\\
  251 ... is basically the same, just mixes the principles of a modal operator
  252 together with skolemization. Suitably enough, the skolem functions here
  253 are called $kolemPath, thus enabling to distinguish later, where they come
  254 from.\PL*/
  255
  256     ; Formula =.. [diamond, Formula1] ->
  257	getval(skolemCounter,Value),
  258	incval(skolemCounter),
  259        concat_atom(['$kolemPath',Value],NewPathFunctionSymbol),
  260        append([PathTerm], ClassVars, Arguments),
  261        NewFunction =.. [NewPathFunctionSymbol | Arguments],
  262        NewPath =.. ['+', PathTerm, NewFunction ],
  263        transform(NewPath,Formula1,ClassVars,PathVars,Intermediate),
  264        Result = Intermediate
  265
  266/*PL If we don't find any of the known operators of the language, we
  267 have to treat the operator in a very boring way: we translate the
  268 arguments but not the operator symbol.\PL*/
  269
  270     ; Formula =.. [OtherFunctor | ArgList] ->
  271        transform_a_list(PathTerm,ArgList,ClassVars,PathVars,
  272                      IntermediateArgList),
  273        Result =.. [OtherFunctor , PathTerm | IntermediateArgList]
  274
  275
  276     ).
  277
  278/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  279
  280\Predicate transform_a_list/5(?PathTerm,
  281		              +ArgumentList,
  282                              ?ClassicalVariables
  283                              ?PathVariables,
  284                              -TranslatedArgumentList)
  285
  286It acts as the predicate |transform| but works on a list.
  287
  288This should be applied to transform the list of arguments of any functor
  289not known to the system.
  290
  291The sixth argument from above (|SortInformation|) is omitted as no new
  292sort information is expected to come up at this level.
  293
  294\PL*/
  295
  296transform_a_list(_,[],_,_,[]).
  297
  298transform_a_list(PathTerm,[H|T],ClassVars,PathVars,Result):-
  299    transform(PathTerm,H,ClassVars,PathVars,I1),
  300    transform_a_list(PathTerm,T,ClassVars,PathVars,I2),
  301    Result = [I1 | I2].
  302
  303/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  304
  305\Predicate make_nnf/3(+Formula, ?Polarity, -NormalizedFormula
  306
  307As the translation assumes a formula in its negation normalform,
  308we have to transform the formula before translating it. This has been
  309done in a rather conventional way, analysing the formula structure and
  310changing the operators to their duals, according to the polarity.
  311
  312\PL*/
  313
  314make_nnf(Formula,Polarity,NormalFormula):-
  315	( var(Formula) ->
  316	    ( Polarity = 0 ->
  317	         NormalFormula = Formula
  318	    ; Polarity = 1 ->
  319	         NormalFormula =.. [not, Formula])
  320
  321	; Formula =.. [implies, Formula1, Formula2] ->
  322	     make_nnf(not Formula1, Polarity, NormalFormula1),
  323	     make_nnf(Formula2, Polarity, NormalFormula2),
  324	     NormalFormula =.. [or, NormalFormula1, NormalFormula2]
  325
  326	; Formula =.. [and, Formula1, Formula2] ->
  327	     make_nnf(Formula1, Polarity, NormalFormula1),
  328	     make_nnf(Formula2, Polarity, NormalFormula2),
  329	     NormalFormula =.. [and, NormalFormula1, NormalFormula2]
  330
  331	; Formula =.. [or, Formula1, Formula2] ->
  332	     make_nnf(Formula1, Polarity, NormalFormula1),
  333	     make_nnf(Formula2, Polarity, NormalFormula2),
  334	     NormalFormula =.. [or, NormalFormula1, NormalFormula2]
  335
  336	; Formula =.. [not, Formula1] ->
  337	     ( Formula1 =.. [not, NewFormula] ->
  338		 make_nnf(NewFormula, Polarity, NormalFormula)
  339	     ; NewPolarity is (Polarity + 1) mod 2,
  340	       make_nnf(Formula1, NewPolarity, NormalFormula))
  341
  342	; Formula =.. [forall, :(Var, Formula1)] ->
  343	     ( Polarity = 0 ->
  344		 make_nnf(Formula1, Polarity, NewFormula1),
  345		 NormalFormula =.. [forall, :(Var, NewFormula1)]
  346	     ; Polarity = 1 ->
  347	          make_nnf(Formula1, Polarity, NewFormula1),
  348		  NormalFormula =.. [exists, :(Var, NewFormula1)])
  349
  350	; Formula =.. [exists, :(Var, Formula1)] ->
  351	     ( Polarity = 0 ->
  352		 make_nnf(Formula1, Polarity, NewFormula1),
  353		 NormalFormula =.. [exists, :(Var, NewFormula1)]
  354	     ; Polarity = 1 ->
  355	          make_nnf(Formula1, Polarity, NewFormula1),
  356		  NormalFormula =.. [forall, :(Var, NewFormula1)])
  357
  358	; Formula =.. [box, Formula1] ->
  359	     ( Polarity = 0 ->
  360		 make_nnf(Formula1, Polarity, NewFormula1),
  361		 NormalFormula =.. [box, NewFormula1]
  362	     ; Polarity = 1 ->
  363	          make_nnf(Formula1, Polarity, NewFormula1),
  364		  NormalFormula =.. [diamond, NewFormula1])
  365
  366	; Formula =.. [diamond, Formula1] ->
  367	     ( Polarity = 0 ->
  368		 make_nnf(Formula1, Polarity, NewFormula1),
  369		 NormalFormula =.. [diamond, NewFormula1]
  370	     ; Polarity = 1 ->
  371	          make_nnf(Formula1, Polarity, NewFormula1),
  372		  NormalFormula =.. [box, NewFormula1])
  373
  374	; Formula = _Anything_else ->
  375	     ( Polarity = 0 ->
  376		 NormalFormula = Formula
  377	     ; Polarity = 1 ->
  378	         NormalFormula =.. [not, Formula])
  379	 ).
  380	  
  381
  382/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  383
  384\Predicate normalize_path/2(+Formula, -NormalizedFormula).
  385
  386This predicate normalises the path terms in the formula according to the
  387new convention introduced in Caen. (We co-operate, so this might explain
  388the mess.)
  389
  390This code was written by Gilbert Boyreau.
  391
  392\PL*/
  393normalize_path(Var,Var2) :-
  394	var(Var),
  395	!,
  396	Var = Var2.
  397normalize_path(Atom,Atom2) :-
  398	atomic(Atom),
  399	!,
  400	Atom = Atom2.
  401normalize_path(+(A1,Arg),
  402	      NormalArg) :-
  403	A1 == 0,
  404	!,
  405	normalize_path(Arg,NormalArg).
  406normalize_path(+(Arg,A2),
  407	      NormalArg) :-
  408	A2 == 0,
  409	!,
  410	normalize_path(Arg,NormalArg).
  411normalize_path(+(A1,C),
  412	      Normal) :-
  413	nonvar(A1),
  414	A1 = +(A,B),
  415	!,
  416	normalize_path(+(A,+(B,C)),
  417			Normal).
  418normalize_path(+(A,B),
  419	      +(NormalA,NormalB)) :-
  420	!,
  421	normalize_path(A,NormalA),
  422	normalize_path(B,NormalB).
  423
  424normalize_path(Term,NormalTerm) :-
  425	Term =.. [F|Args],
  426	normalize_path_list(Args,NormalArgs),
  427	NormalTerm =.. [F|NormalArgs].
  428
  429normalize_path_list([],[]).
  430normalize_path_list([H|T],[NormalH|NormalT]) :-
  431	!,
  432	normalize_path(H,NormalH),
  433	normalize_path_list(T,NormalT).
  434
  435/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  436
  437\Predicate drei/3(+VarList, -CopyVarList, +Variable).
  438
  439This is an auxiliary predicate used to copy lists of veriables,
  440which may be  necessary to avoid erroneous unifications of the systems.
  441
  442We take the |VarList|. All variables identical to |Variable| are fine,
  443if they are not identical, we unify the corresponding heads of the lists.
  444This is to unify nearly every old variable with the new ones, but not the
  445newly introduced variable.
  446
  447\PL*/
  448
  449drei([],[],_).
  450
  451drei([H|T],[H1|T1],Var):-
  452	(H == Var ->
  453	    true
  454	; H = H1
  455        ),
  456	drei(T,T1,Var).
  457
  458/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  459
  460The following predicate is for testing purposes only.
  461
  462Its meaning should be evident.
  463
  464\PL*/
  465
  466tm_file_to_file(Infile,Outfile) :-
  467	open(Infile,read,Stream),
  468	( Outfile = '' ->
  469	    translate_modal(Stream,output)
  470	;   open(Outfile,write,OutStream),
  471	    translate_modal(Stream,OutStream),
  472	    close(OutStream)
  473        ),
  474	close(Stream).
  475
  476/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  477
  478\EndProlog */