/**************************************************************************
*
*        SCAN INTERFACE FOR CORRESPONDENCE THEORY
*                AND CIRCUMSCRIPTION
*
*              H. J. Ohlbach,  1. 12. 1994
*
*
* This file contains Prolog functions for two different 
* translation operations for logical formulae:
* - A translation of  Hilbert style axiomatic specifications for 
*   nonclassical logics to second-order predicate logic.
* - A translation of first order predicate logic formulae
*   to the second order circumscription formula.
* 
* For both versions an input file for the Otter based SCAN algorithm
* can be generated from a suitable specification file.
*
* We use standard Clocksin Mellish Prolog 
* (except open and close instead of tell and told).
* Everything works at least for Quintus and SICStus Prolog, and for eclipse.
*
* I tried to implement a comfortable error handling such that many errors
* can be figured out in one run. 
*
**************************************************************************/



/**************************************************************************
* 
*                  VARIOUS CONFIGURATION PARAMETERS
*
**************************************************************************/

/* scan_file is the which is used as input file for scan. 
   The predicate 'translate' writes to this file.
   The default is '/tmp/scan.in'.
   It can be redefined with 'scan_input_file'. */
  

:-dynamic(scan_file/1).

scan_file('/tmp/scan.in').
scan_input_file(File) :-
	retract(scan_file(_)), 
	assert(scan_file(File)).

/* lazy_parse_file is a temporary file which is used for parsing 
   Otter formulae as Prolog terms (see the 'parse' predicate). */

lazy_parse_file('/tmp/scan-lazy-parse').


rr_max(1000). /* Limit for the number of recursive rewrite calls, 
	         to stop nonterminating rewrite systems */


/* Default parameters for the SCAN program, 
   translated into corresponding set, clear and assign commands.
   They can be overwritten and extended with the 'set' predicate. */

:-dynamic(otter/2).
:-dynamic(otter/3).


otter(assign,max_seconds,100).
/*
otter(set,print_lists_at_end).
otter(set,binary_c_res).
otter(set,c_factor).

otter(set,unit_deletion).
otter(set,process_input). */

/* Otter parameters which should be forwarded */

set(Flag)   :- assert(otter(set,Flag)).
clear(Flag) :- assert(otter(clear,Flag)).

set(Parameter,Value) :- 
	(retract(otter(assign,Parameter,_));true),
	assert(otter(assign,Parameter,Value)).



/* The quote symbol '  */
quote(X) :- name(X,[39]).


/* Symbols which are not read as atoms by Prolog.
   If the flag 'sy_parse_as_atoms.'   is set, 
   all names starting with capital letters are also read as atoms. */

:- dynamic(sy_parse_as_atoms/0).

sy_dangerous('|=').
sy_dangerous('!=').
sy_dangerous('|').
sy_dangerous(X) :- var(X),!,fail.
sy_dangerous(X) :- 
	sy_parse_as_atoms,
	atom(X),name(X,[H|_]),name(Y,[H]),
	my_member(Y,['A','B','C','D','E','F','G','H','I','J','K','L','M','N','O',
	'P','Q','R','S','T','U','V','W','X','Y','Z']).


/* an expression H is evaluated under the parse_as_atoms assumption */ 

as_constants(H) :- 
	assert(sy_parse_as_atoms),
	call(H),
	retract(sy_parse_as_atoms).


/**************************************************************************
*
*		         OPERATORS
*
* We distinguish two kinds of operators and quantifiers
* - the object logic connectives, defined by the user
* - the predicate logic connectives and quantifiers.
*   We use the Otter symbols for this. 
*   In principle they can be redefined, in the fol_connective and fol_quantifier
*   predicate, but then the SCAN output file becomes wrong. 
*   Everything else should work. 
* 
* The user can use the same symbols for object logic connectives as for the
* predicate logic connectives. 
*
**************************************************************************/

:- op(800, xfy, '->').      /* Otter uses the same precedences */
:- op(850, xfy, '<->').     
:- op(790, xfy, '|').       
:- op(780, xfy, '&').       
:- op(500, xfx, '-').   
:- op(700, xfx, '=').      
:- op(700, xfx, '!=').     
:- op(750,xfx,'|=').

fol_connective('&',conjunction).
fol_connective('|',disjunction).
fol_connective(->,implication).
fol_connective(<->,equivalence).
fol_connective(-,negation).
fol_connective(=,equality).
fol_connective('!=',inequality).
fol_connective('|=',satisfies).

fol_quantifier(all,universal).
fol_quantifier(exists,existential).

/* fol_operator allows us to distinguish  connectives from predicates like = etc. */

fol_operator(conjunction).
fol_operator(disjunction).
fol_operator(negation).
fol_operator(implication).
fol_operator(equivalence).
fol_operator(negation).

/* The connective predicate collects all predicate logic and all user defined
   connectives. This is necessary for proper tokenizing and for example 
   distinguishing - (negation) and -> (implication) */

:-dynamic(connective/1).

connective(=).
connective(X) :- fol_connective(X,_). 




/***************************************************************************
****************************************************************************
*
*           TRANSLATION AND CORRESPONDENCE THEORY PART
*
* A typical correspondence theory computation job which can be specified 
* and processed using the functions in this file might look as follows:
*
*    [scan].
*    [operators].
*
*    scan_input_file('/tmp/scan_corr.in').
*    set(max_seconds,2).
*    clear(print_kept).
*
*    truth_condition(all).
*
*    operator(unary(-,-)).
*    operator(binary(&,&),780).         
*    operator(binary('|','|'),790).     
*    operator(binary(->,->),800).       
*    operator(binary(<->,<->),850).     
*    operator(box(b,r)).
*    operator(diamond(d,r)).
*
*    scan([p,q],'b(p) -> b(b(p))').
*
* 
* [scan].      is this file. 
* [operators]. is a library file containing various definitions. 
* 
* All other predicates are explained below. 
* 
* Such a file is for example automatically generated from the 
* corresponding WWW form with the corr_scan.pl  Perl script.
*
****************************************************************************
***************************************************************************/


/**************************************************************************
*
*                THE GENERAL DEFINITION MECHANISM
* 
* The translation of formulae of a user defined logic is determined by 
* various parameters, for example the semantics of the connectives. 
* These parameters are provided by a general definition mechanism.
* For this purpose there is a predicate 
*
*            define(type,name,body1,...)
*
* The first argument specifies the type of the parameter.
* The second argument is a name of the parameter. 
* In general this is a Prolog term f(a1,...an) where the ai are some
* Prolog atoms used in the body of the definition. 
* These ai can be exchanged by the actual values when the definition is 
* instantiated. 
*
* If the body contains logical formulae, in particular those with 
* quantifiers, it is possible to use the more convenient Otter syntax 
* instead of the Prolog term syntax convention. To this end 
* the formula must be enclosed in quotes, for example 
*                             'all x p(x)' 
*
* The define(...) declarations are in general not in this file, 
* but in some extra library files. 

* The def predicate below allows the user to define things in an 
* interactive mode. This is usually not necessary. 
*
***************************************************************************/


def(X,Y,Z)     :- assert(define(X,Y,Z)).
def(X,Y,Z,U)   :- assert(define(X,Y,Z,U)).
def(X,Y,Z,U,V) :- assert(define(X,Y,Z,U,V)).


/**************************************************************************
*
*                          OPERATOR DEFINITIONS
* 
*
* Operator definitions have either the form
*
*           define(operator,        or         define(operator,
*                  Name,                              Name,
*                  Semantics).                        Rewrite_rule).
*
* The prolog atom 'operator' as a fixed keyword determines this as an
* operator definition. Name is a Prolog GROUND term f(a1,...,an)
* where the ai are atoms which can occur in the third argument. 
*
* Examples:  define(operator
*	           box(b,r),
*	          'w |= b(Phi) <-> (all v (r(w,v) -> v |= Phi))',
*                 op(500,fy,[b]).
*
*            define(operator,
*                  back('<=',->),
*                  '(P <= Q) -> (Q -> P)'
*                  op(800,yfx,'<=').
*
* The first version defines an operator via its semantics and the 
* second version defines it via a rewrite rule.
*
* The Semantics argument must always be an equivalence Left <-> Right 
* whose left hand side is of the form w |= Pattern and 
* whose right hand side is an arbitrary formula
* containing instances of v |= Formula (here is the recursion).
* If Prolog syntax conventions are not used, the formula must be quoted. 
*
* This is a prototypic definition of an operator semantics which can be instantiated and
* turned into a translation rule. 
*
* Conventions:  The formula variables must be Prolog variables (with capital letters)
* ***********   The precedence declarations work, unless the Semantics argument
*               is not quoted. In this case, write the precedence declaration for 
*               the symbol used in the Semantics argument before the define predicate. 
*
* The Rewrite_rule argument is a formula Left -> Right and gives a definition of the
* operator in terms of a rewrite rule. 
* 
* Conventions:  The formula variables must be Prolog variables. 
* ***********   For the precedence declarations the same holds as above. 
*
* Operators get instantiated by the operator(Name) predicate.
* In the above example, we can call operator(box(bx,'R')). 
* and we get an operator definition for a modal operator bx and an 
* accessibility relation 'R'. In this case the definition is instantiated by replacing 
* the b with the bx and the r with the 'R' symbol,
* 
* The operator predicate has a second argument, which takes an integer that 
* overwrites the precedence in the corresponding 'define' declaration. 
* Thus, you can instantiate the same scheme with different operators and
* different precedences. 
* 
* The 'operator' predicate actually instantiates the operator declaration with 
* a semantics declaration by
* generating a new clause for the tr_formula translation predicate: 
*         tr_formula(Worldvar,Pattern,Variables,Translated) :- ...
*
* In the above case it is 
*
*         tr_formula(W, bx(Phi), Variables, all(V, 'R'(W, V) -> Rec)) :-
*                    new_symbol(wv, V), tr_formula(V, Phi, Variables, Rec).
*
* The recursive parts v |= Formula are turned into recursive calls of the 
* translation function, and the variables are replaced by fresh variables. 
* The Variables argument collects the domain variables which should not 
* obtain world arguments during the translation of terms. 
*
* An operator declaration with a rewrite rule definition is instantiated by 
* generating a new clause for the 'rewrite(Old,New,N)' predicate. 
*
**************************************************************************/

:-dynamic(tr_formula/4).

operator(Name,Precedence) :-
	get_definition(operator,Name,Definition,Precedence,[Newprecedence],Error),!,
	(var(Error) ->
	 (op_connective(Name), 
	  (var(Newprecedence);call(Newprecedence)),
	  (functor(Definition,Functor,_),
	  (fol_connective(Functor,equivalence) -> 
	   op_defsemantics(Name,Definition);
	      (fol_connective(Functor,implication) ->
	       op_defrewrite(Definition);
		  er_op_def(Name,Definition)))));
	true).


operator(Name) :-
	operator(Name,_Precedence).


/* ops and opr are shortcuts for a define(operator,...). operator(...). sequence. 
   They allow you to define operators directly without   
   using and instantiating a schema.

   ops defines an operator with a semantics definition and 
   opr defines an with a rewrite rule declaration. */
   

ops(Operator,Semantics) :-
	parse(Semantics,Definition,Error),
	er_parse_report(('semantics of', Operator),Error),
	(var(Error) ->
	 (op_defsemantics(Operator,Definition),
	  assert(connective(Operator)));
	true).

opr(Operator,Rewrite) :-
	parse(Rewrite,Definition,Error),
	er_parse_report(('rewrite rule for', Operator),Error),
	(var(Error) ->
	 ((functor(Definition,F,_),fol_connective(F,implication)) -> 
	   (op_defrewrite(Definition),
	    assert(connective(Operator)));
	     	er_op_def1(Operator,Definition));
	true).


/*                 INTERNAL PREDICATES                */

/* This is the predicate called by gd_more. 
   It deals with the precedence declarations.*/

operator_extra(_Name,Precedence,Prec,_,_,_) :- 
	var(Prec),
	var(Precedence),!.

operator_extra(Name,Precedence,Prec,_,_,_) :- 
	var(Prec),!,
	er_op_precnumber(Name,Precedence).

operator_extra(Name,Precedence,op(Number,Parenthesis,Op),Newprec,_,_) :- 
	integer(Number),!,
	(op(Number,Parenthesis,Op) -> true;
	    er_op_prec(Name,op(Number,Parenthesis,Op))),
	(var(Precedence) -> 
	 (Newprec = op(Number,Parenthesis,Op));
	    (Newprec = op(Precedence,Parenthesis,Op))).

operator_extra(Name,_,Prec,_,_,_) :- 
	er_op_prec(Name,Prec).
	


op_defsemantics(Name,Definition) :-
	(arg(1,Definition,Left),
	 arg(2,Definition,Right),
	 functor(Left,Sat,_),
	 fol_connective(Sat,satisfies),
	 arg(1,Left,World),
	 arg(2,Left,Pattern)) ->
	 (subst(Right,World,Worldvar,Right1),
	  op_collect(Right1,Pattern,Variables,Translated,Recursive),
	  op_clean(Recursive,Recursives),
	  asserta((tr_formula(Worldvar,Pattern,Variables,Translated) :- !,Recursives)));
	er_op_def(Name,Definition).

op_defrewrite(Definition) :-
	arg(1,Definition,Left),
	arg(2,Definition,Right),
	asserta((rewrite(Left,Result,N) :- !,rr_check(N,M),rewrite(Right,Result,M))).

op_connective(Name) :-
	arg(1,Name,Connective),
	assert(connective(Connective)).


/* This function collects the recursive parts of the operator semantics and 
   turns them into recursive translation calls. 
   Furthermore it collects the bound variables, replaces them by Prolog variables 
   and generates a new_symbol call that binds the Prolog variables by fresh 
   symbols when applied for translating a particular formula. 

   The output variable Translated gets bound to the new skeleton with 
   Prolog variables at the corresponding places.
   The Recusive arguments gets bound to a conjunction of the Prolog predicates 
   to be called for binding the Prolog variables to the corresponding values. */

op_collect([],_,_,[],true) :-!.
op_collect([H|T],Left,Variables,[Hc|Tc],(Rh,Rt)) :- !,
	op_collect(H,Left,Variables,Hc,Rh),
	op_collect(T,Left,Variables,Tc,Rt).


op_collect(Formula,Left,Variables,Translated,Recursive) :- 
	functor(Formula,Operator,N),
	fol_connective(Operator,Type),
	fol_operator(Type),!,
	arguments(Formula,N,Args), 
	op_collect(Args,Left,Variables,Trans,Recursive),
	Translated =.. [Operator|Trans].

/* This clause deals with the bound variables. */


op_collect(Formula,Left,Variables,Translated,Recursive) :-
	functor(Formula,Quantifier,_), 
	fol_quantifier(Quantifier,_),
	arg(1,Formula,Variable),
	in(Variable,Left),!,	
	arg(2,Formula,Subformula),
	op_collect(Subformula,Left,[Variable|Variables],Subtrans,Recursive),
	Translated =.. [Quantifier,Variable,Subtrans].

op_collect(Formula,Left,Variables,Translated,(new_symbol('wv',V),Recursive)) :-
	functor(Formula,Quantifier,_), 
	fol_quantifier(Quantifier,_),!, 
	arg(1,Formula,Variable),
	arg(2,Formula,Subformula), 
	op_collect(Subformula,Left,Variables,Subtrans,Subrec),
	subst(Subtrans,Variable,V,Subtrans1),
	Translated =.. [Quantifier,V,Subtrans1], 
        subst(Subrec,Variable,V,Recursive),!.

/* This clause generates the recursive translation calls. */

op_collect(Formula,_,Variables,Translated,tr_formula(V,Phi,Variables,Translated)) :- 
	functor(Formula,F,_), 
	fol_connective(F,satisfies),!, 
	arg(1,Formula,V),
	arg(2,Formula,Phi).


op_collect(Formula,_,_,Formula,true) :- !.


/* Elimination of superfluous 'true' predicates in the conjunction generated 
   by op_collect */

op_clean(X,Z) :- op_cleann(X,Y),op_cleann(Y,Z).

op_cleann((true,X),Y)  :- op_cleann(X,Y).
op_cleann((X,true),Y)  :- op_cleann(X,Y).
op_cleann((X,Y),(U,V)) :- op_cleann(X,U),op_cleann(Y,V).
op_cleann(X,X).



/*******************************************************************
*
*                       THE KERNEL OF THE  TRANSLATION FUNCTION
*
* tr_formula(World,Formula,Variables,Translated)
* computes the translated Formula with respect to the world term World.
* The Variables argument collects the bound variables. 
* It prevents that variables get a world as argument. 
*
* The translated formula is a Prolog term (not yet Otter syntax).
*
*******************************************************************/


/* The clauses below realize the translation of terms. 
   Variables and rigid symbols don't get a world argument,
   all other terms f(t1...tn) get an argument f(World,t1...tn) 
   and this recursively, of course.
   
   The translation of formulae is done by the clauses generated from the 
   operator declarations. */

tr_formula(_,Variable,Variables,Variable) :-
	my_member(Variable,Variables),!.

tr_formula(World,Constant,_,Translated) :-
	atom(Constant),
	((rigid(Constant),Translated = Constant);
	    Translated =.. [Constant,World]),!.

tr_formula(World,Term,Variables,Translated) :- 
	functor(Term,Function,N),
        arguments(Term,N,Arguments),
	tr_termlist(World,Arguments,Variables,Trans),
	((rigid(Function),Translated =.. [Function|Trans]);
	                  Translated =.. [Function,World|Trans]),!.


/* Translation of a termlist. Nothing special */

tr_termlist(_,[],_,[]).
tr_termlist(World,[H|T],Variables,[Htr|Ttr]) :-
	tr_formula(World,H,Variables,Htr),
	tr_termlist(World,T,Variables,Ttr),!.



/**************************************************************************
*
*                           TRUTH CONDITIONS
*
* Truth conditions specify when a formula of a nonclassical logic is to be 
* considered as a theorem. 
* A typical specification is 
*
*      define(truth_condition,
*          all,
*          'all w (w |= Phi)'.
*
* It specifies that a formula must be true in all worlds. 
* A truth condition can be an arbitrary formula with  literals Term |= X
* in them. The X which may be an arbitrary symbol stands for the formula. 
* 
* The predicate truth_condition(Name) instantiates the truth condition by 
* generating a predicate 'translate(Formula,Result)', which translates
* a formula according to the truth condition, using the tr_formula predicate.
* For example the above truth conditions yields a translation predicate
*   translate(Formula, all(w,F)) :- tr_formula(w,Formula,[],F).
* 
* Only one truth condition can be instantiated at a time!
* Later instantiations overwrite previous ones. 
*
* As all define .. predicates, the name of the truth condition may be a 
* Prolog GROUND term, whose constants serve as formal parameters 
* replaced by the actual parameters as given in truth_condition(Name). 
*
**************************************************************************/

:-dynamic(translate/2).

truth_condition(Name) :-
	get_definition(truth_condition,Name,Formula,_,[],Error),!,
	tc_activate(Formula,Error).

/* trc is a shortcut for a define(truth_condition,...). truth_condition(...).
   sequence. It activates a truth condition directly. */

trc(Trc) :-
	parse(Trc,Formula,Error),
	er_parse_report('truth condition',Error),
	tc_activate(Formula,Error).


/*         INTERNAL PREDICATES       */

tc_activate(Formula,Error) :-
	var(Error) ->
	(tc_collect(Formula,Phi1,Abstracted,Recursives),
	 my_retractall(translate(_,_)),
	 assert((translate(Phi,Abstracted) :- !,fix_rewrite(Phi,Phi1),Recursives)));
	true.

/* tc_collect collects the necessary calls to the tr_formula predicate. 
   Similar to op_collect */

tc_collect([],_,[],true) :-!.
tc_collect([H|T],Phi,[Hc|Tc],(Rh,Rt)) :- !,
	tc_collect(H,Phi,Hc,Rh),
	tc_collect(T,Phi,Tc,Rt).


tc_collect(Formula,Phi,Translated,Recursive) :- 
	functor(Formula,Operator,N),
	fol_connective(Operator,Type),
	fol_operator(Type),!,
	arguments(Formula,N,Args),
	tc_collect(Args,Phi,Trans,Recursive),
	Translated =.. [Operator|Trans].


/* This clause deals with the bound variables. */

tc_collect(Formula,Phi,Translated,Recursive) :-
	functor(Formula,Quantifier,_), 
	fol_quantifier(Quantifier,_),
	arg(1,Formula,Variable),
	arg(2,Formula,Subformula),
	tc_collect(Subformula,Phi,Subtrans,Recursive),
	Translated =.. [Quantifier,Variable,Subtrans].

/* This clause generates the recursive translation calls. */

tc_collect(Formula,Phi,Translated,tr_formula(V,Phi,[],Translated)) :- 
	functor(Formula,F,_), 
	fol_connective(F,satisfies),!,
	arg(1,Formula,V).

tc_collect(Formula,_,Formula,[]) :- !.


/* This is the translation function for translating lists of formula */

translate_list([],[]).
translate_list([H|T],[Ht|Tt]) :-
	translate(H,Ht),
	translate_list(T,Tt),!.


/**************************************************************************
*
*                         ASSUMPTIONS AND QUALIFICATIONS
* 
* The assumption facility provides a means to pass certain formulae to the 
* SCAN algorithm. 
* Typically these are assignment restrictions as in the intuitionistic logic case,
* or properties of the accessibility relation etc. which might help simplify the
* SCAN generated formula set. 
* 
* We distinguish 'assumptions' and 'qualifications'. 
* Assumptions are not part of the scanned formulae, and they are not negated. 
* qualifications specify properties of the predicates to be eliminated. 
* They are part of the formulae to be scanned and they are part of the 
* negated and unskolemized result. 
* From a logical point of view we have the following correspondences:
* assumptions -> (all p qualification(p) -> formula(p) 
*                 <-> scan((all p qualification(p) -> formula(p))))
*
* Assumptions are defined as in the example
* 
*   define(assumption,transitivity(r),
*            'all x y z (r(x,y) & r(y,z) -> r(x,z)').
* 
* Qualifications are defined as in the example
*
*   define(qualification,assignment_restriction(p,r),
*	'all w (p(w) -> all v (r(w,v) -> p(v)))').
*
* Both are instantiated with the corresponding instantiation predicates below. 
* This instantiation translates the formula into Otter syntax and 
* stores the result in the assumptions and qualifications predicates. 
*
**************************************************************************/

:-dynamic(assumptions/1).
:-dynamic(qualifications/1).

assumption(Name) :-
	get_definition(assumption,Name,Assumption,_,[],Error),
	ass_activate(Assumption,Error).


/* A shortcut for a define. assumption. sequence.  */

ass(Assumption) :-
	parse(Assumption,Formula,Error),
	er_parse_report(Assumption,Error),
	ass_activate(Formula,Error).

ass_activate(Assumption,Error) :-
	(var(Error) -> 
	 (sy_otter(Assumption,Otterformula),
	  assert(assumptions(Otterformula)));
	true).


qualification(Name) :-
	get_definition(qualification,Name,Qualification,_,[],Error),
	qual_activate(Qualification,Error).

/* A shortcut for a define. qualification. sequence.  */

qual(Qualification) :-
	parse(Qualification,Formula,Error),
	er_parse_report(Qualification,Error),
	qual_activate(Formula,Error).

qual_activate(Qualification,Error) :-
	(var(Error) -> 
	 (sy_otter(Qualification,Otterformula),
	  assert(qualifications(Otterformula)));
	true).




/**************************************************************************
*
*                              REWRITE RULES
*
* We provide a general rewrite mechanism for the user defined logic. 
* It is primarily intended for computing a negation normal form, 
* but it may also be used to do other transformations. 
* 
* A rewrite system is defined in several stages. 
* The lowest level is the definition rewrite rules.
* Typical definitions could be 
* 
*           define(rr_rule,implication(-,->,&,'|'),
*  	           [ '(P -> Q) -> (-P | Q)',
*	            '-(P -> Q) -> (P & -Q)']).
* or 
*           define(rr_rule,box(b,d),
*	            '-b(P) -> d(-P)').
*
* The first argument of the define predicate must be the atom rr_rule. 
* The second argument is the rule name, which can be an atom or a 
* GROUND term. The parameters are formal parameters, which can be instantiated 
* with the actual parameters later on.
* The last argument consists of a single rewrite rule or a list of rewrite rules. 
* Each rewrite rule must be an implication left -> right,
* and both sides can be in Otter syntax, but the formula variables must be 
* Prolog variables (i.e. starting with a capital letter).
* 
*
* The second level is the definition of a rewrite rule system. 
* for example
*
*           define(rr_system,pl0_nnf(-,&,'|',->,<->),   
* 	           [cancel(-),
*	            neg_in(-,&,'|'),neg_in(-,'|',&),
*	            implication(-,->,&,'|'),
*	            equivalence(-,<->,&,'|')]).
*
* The first argument of define is the atom rr_sytem. 
* The second argument is the name of the rewrite system with its parameters.
* The third argument is a list of rewrite rule or other rewrite system names
* with the formal parameters replaced by the actual parameters. 
* 
* By using other rewrite system names you can incrementally build rewrite systems
* on top of other systems. 
*
* A rewrite rule can be activated with the rr_rule predicate and a 
* rewrite system can be activated with the rr_system predicate.
* Both generate the corresponding clauses for the rewrite(Old,New,N) predicate. 
*
* The third argument in the rewrite predicate counts the number of 
* recursive rewrite calls and stops it if the rr_max limit is exceeded. 
* Since we can't stop the user from defining divergent rewrite systems,
* this is a way for keeping the rewriting under control. 
*
* The rewrite clauses down provide only the skeleton. 
* They do the recursive descent without changing anything. 
*
***************************************************************************/

:-dynamic(rewrite/3).

rr_rule(Name) :-
	get_definition(rr_rule,Name,Rule,_,[],Error),
	(var(Error) -> 
	 rr_activate_rule(Name,Rule);
	    true).

/* A shortcut  for a define - rr_rule  sequence */

rr(Rule) :-	
	parse(Rule,Formula,Error),
	er_parse_report(('rewrite rule',Rule),Error),
	(var(Error) -> 
	 rr_activate_rule(Rule,Formula);
	    true).

rr_activate_rule(_,[]) :-!.

rr_activate_rule(Name,[Formula|_T]) :-  
	var(Formula),!,
	er_rr_noimp(Name,Formula).

rr_activate_rule(Name,[Formula|T]) :- !, 
	functor(Formula,Imp,_),
	(fol_connective(Imp,implication) ->
	 (arg(1,Formula,Left),
	  arg(2,Formula,Right),
	  asserta((rewrite(Left,Result,N) :- !,rr_check(N,M),rewrite(Right,Result,M))),
	  rr_activate_rule(Name,T));	
	    er_rr_noimp(Name,Formula)).


rr_activate_rule(Name,X) :-
	rr_activate_rule(Name,[X]).

/* The activation functions for rewrite systems */

rr_system(Name) :-
	is_defined(rr_system,Name,[]) ->
	(get_definition(rr_system,Name,System,_,[],Error),
	 (var(Error) -> rr_activate_system(System);true));
	rr_rule(Name).


rr_activate_system([]) :- !.
rr_activate_system([H|T]) :-!,
	rr_system(H),!,
	rr_activate_system(T),!.

rr_activate_system(X) :-
	er_rr_activate(X).


/* This is the skeleton of the rewrite predicate. 
   These clauses do nothing, but the recursive descent. */

rewrite(Formula,Result,N) :-
	rr_check(N,M),
	functor(Formula,Connective,I),
	I > 0,
	arguments(Formula,I,Args),
	rewrite_list(Args,Nargs,M),
	Result =.. [Connective|Nargs],!.


rewrite(Formula,Formula,_).

rewrite_list([],[],_).
rewrite_list([H|T],[Hn|Tn],N) :-
	rewrite(H,Hn,N),
	rewrite_list(T,Tn,N),!.


/* This predicate calls the rewrite predicate as long as the rewriting 
   changes something at the term structure. */

fix_rewrite(Formula,Result) :-
	rewrite(Formula,Result1,0),
	((Formula == Result1) -> 
	 (Result = Result1);
	fix_rewrite(Result1,Result)).

rr_check(N,M) :-
	rr_max(K), 
	(N > K -> (er_rr_max(K),fail);M is N+1).

/***************************************************************************
*
*           FURTHER PARAMETERS FOR THE TRANSLATION FUNCTION
*
*
* The 'rigid' declaration influences the translation of symbols. 
* Rigid symbols do not depend on the actual world. 
* They don not get a world argument. 
*
****************************************************************************/

:-dynamic(rigid/1).   


rigid(Term) :-
	functor(Term,F,N),
	N>0,
	rigid(F).
rigid(=).


/* The negate first declaration cause the original formula to be negated 
   before it is translated. This is usually not necessary, but might be 
   useful. */

:-dynamic(negate/1).
	 
negate_first(Negation) :-
	assert(negate(Negation)).




/***************************************************************************
*
*                        SCAN INPUT FILE GENERATION
*
* The predicate scan/2 takes either a single predicate symbol or a list of 
* predicate symbols (Prolog atoms) and a formula of some nonclassical logic 
* (a Prolog atom in Otter syntax) and prepares an input file for the SCAN algorithm
* such that SCAN can compute the corresponding frame axiom. 
* In particular the following actions are performed:
* - the formula is turned into a Prolog term
* - If a rewrite system is active, it is used to rewrite the formula.
* - The operator semantics is used as rewrite rule to 
*   translate the formula into predicate logic. 
* - The translated formula is embedded in the truth condition. 
* - Interpreting the 'Predicates' as universally quantified predicate variables,
*   the translated formula is negated and a SCAN input file is generated for 
*   eliminating these predicates. The SCAN flags are set such that after 
*   elimination of the predicates the formula is unskolemized and negated again. 
* 
* A typical call is: scan(p,'box(p) -> p').
* If box is defined as the standard modal box operator then 
* generated input file for SCAN should allow it compute
* the reflexivity of the accessibility relation. 
*
* The  scan/3 predicate is intended for translating Hilbert rules. 
* A typical call might be: translate(p,[p,'p => q'],q).
* It translates the modus ponens rule according to the semantics of =>.
*
* The translation is influenced by the following parameters:
* - the operator semantics    (see define(operator))
* - the truth condition       (see define(truth_condition))
* - the active rewrite system (see define(rewrite))
* - the 'rigid' declarations for function and predicate symbols.
*   rigid symbols do not depend on the world. 
*
*****************************************************************************/


scan(Predicates,Formula) :-                 /* Single Predicate, Single Formula */
        atom(Predicates),!,
	scan([Predicates],Formula).

scan(Predicates,Formula) :-                 /* Predicate List, Single Formula */
	er_no_truth_condition,!,            /* Check if a truth condition is defined, */
	as_constants(parse(Formula,Trans,Error)),  /*otherwise abort*/
	er_parse_report(formula,Error), 
	var(Error),                  /* Abort */
        sc_neg1(Trans,Trans0),          
        translate(Trans0,Trans1), 
	sc_neg2(Trans1,Trans2),
	sy_otter(Trans2,Trans3),
	scan_file(File),
	open(File,write,Stream),
	sc_scan_header(Stream,Predicates),
	sc_header(Stream),
	write(Stream,'formula_list(usable).'),nl(Stream),
	my_not(sc_assumptions(Stream)),nl(Stream),
	write(Stream,'end_of_list.'),nl(Stream),
	write(Stream,'formula_list(sos).'),nl(Stream),
	my_not(sc_qualifications(Stream)),nl(Stream),
	ot_print(Stream,Trans3),write(Stream,'.'),nl(Stream),
	write(Stream,'end_of_list.'),
	close(Stream),!.


scan(Predicates,Premisses,Conclusion) :-    /* Single Predicate, Implication */
	atom(Predicates),!,
	scan([Predicates],Premisses,Conclusion).

scan(Predicates,Premisses,Conclusion) :-   /* Predicate List, Implication */
	er_no_truth_condition,!,           /* Check if a truth condition is defined,*/
        as_constants(parse_list(Premisses,Prem0,Errprem)),  /* otherwise abort*/
	er_parse_report(premisses,Errprem),
	as_constants(parse(Conclusion,Conc,Errconc)),
	er_parse_report(conclusion,Errconc),
	var(Errprem),var(Errconc),                /* Abort */
	translate_list(Prem0,Prem1),
	sy_otter_list(Prem1,Prem2),
	sc_neg1(Conc,Conc0),
	translate(Conc0,Conc1),
	sc_neg2(Conc1,Conc2),
	sy_otter(Conc2,Conc3),
	scan_file(File),
	open(File,write,Stream),
	sc_scan_header(Stream,Predicates),
	sc_header(Stream),
	write(Stream,'formula_list(usable).'),nl(Stream),
	my_not(sc_assumptions(Stream)),nl(Stream),
	write(Stream,'end_of_list.'),nl(Stream),
	write(Stream,'formula_list(sos).'),nl(Stream),
	my_not(sc_qualifications(Stream)),
	ot_print_list(Stream,Prem2),
	ot_print(Stream,Conc3),write(Stream,'.'),nl(Stream),
	write(Stream,'end_of_list.'),
	close(Stream),!.


sc_neg1(Formula,Negated) :-
	negate(Negation),!,
	Negated =.. [Negation,Formula].

sc_neg1(Formula,Formula).

sc_neg2(Formula,Formula) :-
	negate(_),!.

sc_neg2(Formula,Negated) :-
	fol_connective(Neg,negation),
	Negated =.. [Neg,Formula].


/*****************************************************************************
*
*      SCAN AND OTTER PARAMETER SETTING AND PRINTING COMMANDS
*
*****************************************************************************/

/* Parameter printing */

sc_scan_header(Stream,Predicates) :-
	write(Stream,pred_list),write(Stream,Predicates),write(Stream,'.'),nl(Stream),
	write(Stream,'set(unskolemize).'),nl(Stream),
	write(Stream,'set(negate).'),     nl(Stream),
	write(Stream,';.'),nl(Stream).

sc_header(Stream) :-
	my_not(sc_set(Stream)),
	my_not(sc_clear(Stream)),
	my_not(sc_assign(Stream)).


sc_set(Stream) :-
	otter(set,Flag),
	write(Stream,set(Flag)),
	write(Stream,'.'),nl(Stream),fail.

sc_clear(Stream) :-
	otter(clear,Flag),
	write(Stream,clear(Flag)),
	write(Stream,'.'),nl(Stream),fail.

sc_assign(Stream) :-
	otter(assign,Parameter,Value),
	write(Stream,assign(Parameter,Value)),write(Stream,'.'),nl(Stream),fail.

sc_assumptions(Stream) :-
	assumptions(A),
	ot_print(Stream,A),
	write(Stream,'.'),nl(Stream),fail.


sc_qualifications(Stream) :-
	qualifications(A),
	ot_print(Stream,A),
	write(Stream,'.'),nl(Stream),fail.




/**************************************************************************
*
*         GENERAL PREDICATE FOR ACCESSING DEFINITIONS 
*
**************************************************************************/

is_defined(Type,Name,More) :-
	atom(Name),!,
	new_vars(More,More1),
	Pattern =..[define,Type,Name,_Def1|More1],
	call(Pattern).

is_defined(Type,Name,More) :-
	var_abstract(Name,Aname,_Consts,_Vars),
	new_vars(More,More1), 
	Pattern =..[define,Type,Aname,_Def1|More1], 
	call(Pattern).

get_definition(Type,Name,_Definition,_Extra,_More,1) :-
	var(Type),!,
	er_gd_var(Type,Name).

get_definition(Type,Name,_Definition,_Extra,_More,1) :-
	var(Name),!,
	er_gd_var(Type,Name).

get_definition(Type,Name,Definition,Extra,More,Error) :-
	var_abstract(Name,Aname,Consts,Vars),
	new_vars(More,More1), 
	Pattern =..[define,Type,Aname,Def1|More1], 
	(call(Pattern) ->
	 (gd_more(Type,Name,Extra,More1,Vars,Consts,More), 
	  gd_parse(Type,Name,Def1,Definition,Vars,Consts,Error));
	    (er_definition(Type,Name),Error = 1)).


gd_more(_,_,_,[],_,_,[]) :-!.

gd_more(Type,Name,Extra,More,Old,New,Nmore) :-
	my_concat(Type,'_extra',Predicate),
	new_vars(More,More1),
	my_append(More,More1,Par),
	my_append(Par,[Old,New],Par1),
	Function =.. [Predicate,Name,Extra|Par1],
	(call(Function) -> substs(More1,Old,New,Nmore);
	    er_gd_more((Type,Name),More)).


gd_parse(_,_,[],[],_,_,_).
gd_parse(Type,Name,[H|T],[Hp|Tp],Old,New,Error) :-!,
	gd_parse(Type,Name,H,Hp,Old,New,Error),
	gd_parse(Type,Name,T,Tp,Old,New,Error),!.

gd_parse(Type,Name,Atom,Formula,Old,New,Error) :-
	atom(Atom),!,
	parse(Atom,Parsed,Error),
	er_parse_report((Type,Name),Error),
	(var(Error) -> 
	 substs(Parsed,Old,New,Formula);
	    true).


gd_parse(_Type,_Name,Term,Formula,Old,New,_Error) :-
	substs(Term,Old,New,Formula).


/**************************************************************************
* 
*            PARSING OTTER FORMULAE
*
* This is a primitive parser for the Otter syntax. 
* The Otter formulae are read as a Prolog atom.
* The main difference between Otter formulae and Prolog terms is
* - quantifications may be written as 'all x y exists z v ..'
* Therefore the parsing process is done as follows:
* - The atom is converted into a character list. 
* - The character list is tokenized. 
* - Quantifications like all x y .. are changed into 
*                        all ( x , all ( y , ..  ))
*    This facility recognizes only the two predicate logic quantifiers all and exists.
*    All other quantifiers must be written in Prolog syntax, for example ex(x,phi(x)).
* The result is a list of tokens which should represent linearized Prolog terms.
* Since there is no 'read form string' possibility in standard Prolog,
* we write this list to a temporary file /tmp/lazy-parse.pl and then read it back.
* Thus, the Prolog parser does the main job. 
*
**************************************************************************/


parse(Atom,Term,Error) :-
	atom(Atom),!,
	tokenize(Atom,List,Err),!, 
	(Err == 1 -> 
	 (Error = List,er_parentheses(Atom,List));
	    (prolog_parse(List,Term);Error = 1)).

parse(X,X,_).

	
parse_list([],[],_) :-!.
parse_list([H|T],[Hp|Tp],Error) :- !,
	parse(H,Hp,Error),!,
	parse_list(T,Tp,Error).

parse_list(X,[Term],Error) :- 
	parse(X,Term,Error).


prolog_parse(List,Term) :-
	my_append([lazy_parse,'('|List],').',L1),
	lazy_parse_file(File),
	open(File,write,Stream),
	sy_print(Stream,L1),
	close(Stream),
	open(File,read,Stream1),
	(read(Stream1,lazy_parse(Term0)) -> 
	 (close(Stream1),
	  normalize_inequalities(Term0,Term));
	    close(Stream1),!,fail).


tokenize(Atom,List,Error) :-
	name(Atom,Symbols),
	tk_tokenize(Symbols,Token,Restlist,Error),
	tk_close_token(Token,Restlist,List,Error).

tk_tokenize([],[],[],_).
tk_tokenize([H|T],Token,Tokens,Error) :-
	tk_tokenize(T,Current,List,Error),!,
	tk_analyse(H,Current,List,Token,Tokens,Error).

tk_analyse(Character,Currenttoken,Currenttokens,[],Tokens,Error) :-
	name(' ',[Character]),!,
	tk_close_token(Currenttoken,Currenttokens,Tokens,Error).

tk_analyse(Character,Currenttoken,Currenttokens,[],[Name|Tokens],Error) :-
	tk_separator(Character,Name),!,
	tk_close_token(Currenttoken,Currenttokens,Tokens,Error).

tk_analyse(Character,Currenttoken,Currenttokens,[Character|Currenttoken],Currenttokens,_).


tk_close_token([],Currenttokens,Currenttokens,_) :- !.

tk_close_token(Currenttoken,Currenttokens,Tokens,_) :-
	name(Atom,Currenttoken),
	Currenttoken = [Character|Tail],
	name(Single,[Character]), 
	(connective(Single) -> 
	 (connective(Atom) ->
	  (Tokens = [Atom|Currenttokens]);
	     (name(Tatom,Tail),Tokens = [Single,Tatom|Currenttokens]));
	 tk_quantifier(Atom,Currenttokens,Tokens)),!.
	
tk_close_token(Symbol,Tokens,[Name,'**HERE**'|Tokens],1) :- 
	name(Name,Symbol).


/* Here we treat the all x y z ... case */
tk_quantifier(Symbol,['('|T],[Symbol,'('|T]) :-
    fol_quantifier(Symbol,_),!.

tk_quantifier(Symbol,List,[Symbol,'(',Variable,','|Newlist]) :-
    fol_quantifier(Symbol,_),
    List = [Variable|T],!,
    tk_qu_fill(Symbol,T,1,Newlist).

tk_quantifier(Symbol,List,[Symbol|List]).

/* Finding the end of a variable list and adding the left out quantifiers */

tk_qu_fill(_,['('|T],N,['('|Tnew]) :-
    !,tk_qu_par(T,N,0,0,Tnew).



tk_qu_fill(_,[X,'('|T],N,[X,'('|Tnew]) :-
	(T=[Term,')'|_];T=[Term,','|_]),!,
	 tk_qu_par(T,N,0,0,Tnew).

tk_qu_fill(Quantifier,[X,'('|T],N,[Quantifier,'(',X,','|Tnew]):-
	 tk_qu_par(T,N,0,0,Tnew),!.

tk_qu_fill(Quantifier,[X |T],N,[Quantifier,'(',X,','|Tnew]) :-
    N1 is N+1,!,
    tk_qu_fill(Quantifier,T,N1,Tnew).



tk_qu_par([')'|T],N,0,1,Tokens) :-
        tk_parentheses(N,Parentheses),
	my_append([')'|Parentheses],T,Tokens),!.

tk_qu_par([')'|T],N,0,0,Tokens) :-
        tk_parentheses(N,Parentheses),
	my_append([')'|Parentheses],T,Tokens),!.


tk_qu_par(['('|T],N,M,_,['('|Tnew]) :-
	M1 is M+1,!,
	tk_qu_par(T,N,M1,1,Tnew).

tk_qu_par([')'|T],N,M,Flag,[')'|Tnew]) :-
	M1 is M-1,!,
	tk_qu_par(T,N,M1,Flag,Tnew).
  
tk_qu_par([H|T],N,M,Flag,[H|Tnew]) :-
	!,tk_qu_par(T,N,M,Flag,Tnew).
  
tk_parentheses(0,[]) :- !.
tk_parentheses(N,[')'|Pars]) :-
    N1 is N-1,
    tk_parentheses(N1,Pars).



tk_separator(Character,'(') :- name('(',[Character]).
tk_separator(Character,')') :- name(')',[Character]).
tk_separator(Character,'[') :- name('[',[Character]).
tk_separator(Character,']') :- name(']',[Character]).
tk_separator(Character,',') :- name(',',[Character]).
tk_negation(Character,'-')  :- name('-',[Character]).

/* a neq b  -> ~(a = b). */

normalize_inequalities(Interm,Interm) :-
	(atomic(Interm);var(Interm)),!.

normalize_inequalities(Interm,Outterm) :-
	functor(Interm,F,_),
	fol_connective(F,inequality),!,
	arguments(Interm,2,Args),
	fol_connective(Eq,equality),
	fol_connective(Neg,negation),
	Out     =.. [Eq|Args],
	Outterm =.. [Neg,Out].

normalize_inequalities(Interm,Outterm) :-
	functor(Interm,F,N),
	arguments(Interm,N,Args),
	normalize_inequalities_list(Args,Arguments),
	Outterm =.. [F|Arguments].

normalize_inequalities_list([],[]).
normalize_inequalities_list([H|T],[Hn|Tn]) :-
	normalize_inequalities(H,Hn),
	normalize_inequalities_list(T,Tn).


/***************************************************************************
* 
*               TRANSLATION TO OTTER SYNTAX
*
* sy_otter translates the Prolog terms which represent predicate logic formulae
* into the syntax of Otter. 
* Certain optimizations which make the Otter formulae more readable are performed. 
* The result is a list which when printed to a file, hopefully is parseble by Otter. 
*
***************************************************************************/


sy_otter(Formula,['(',Formula,')']) :-
	functor(Formula,Connective,_),
	fol_connective(Connective,equality),!.

sy_otter(Formula,[Formula]) :-
	atom(Formula),!.


sy_otter(Formula,Result) :-
	functor(Formula,Connective,1),
	fol_connective(Connective,negation),
	arg(1,Formula,Subformula),
	functor(Subformula,Connective,1),!,
	fol_connective(Connective,negation),
	arg(1,Subformula,Subsubformula),
	sy_otter(Subsubformula,Result).

sy_otter(Formula,['(',Result,')']) :-
	functor(Formula,Connective,_),
	fol_connective(Connective,negation),
	arg(1,Formula,Subformula),
	functor(Subformula,Equality,_),
	fol_connective(Equality,equality),!,
	arg(1,Subformula,Left),
	arg(2,Subformula,Right),
	fol_connective(Neq,inequality),
	Result =..[Neq,Left,Right].

sy_otter(Formula,['(',Connective|Result]) :-
	functor(Formula,Connective,1),
	fol_connective(Connective,negation),!,
	arg(1,Formula,Subformula),
	sy_otter(Subformula,Sub),
	my_append(Sub,[')'],Result).

sy_otter(Formula,['('|Result]) :-
	functor(Formula,Connective,_), 
	fol_connective(Connective,Type),
	(Type = conjunction; Type=disjunction),
	sy_flatten(Formula,Connective,Flattened),
	my_append(Flattened,[')'],Result),!.

sy_otter(Formula,Result) :-
	functor(Formula,Connective,_), 
	fol_connective(Connective,Type),
	(Type = implication; Type=equivalence),
	arg(1,Formula,Left),
	arg(2,Formula,Right),
	sy_otter(Left,L),
	sy_otter(Right,R),
	my_append(R,[')'],R1),
	my_append(['('|L],[Connective|R1],Result),!.

sy_otter(Quantified,Result) :-
	functor(Quantified,Quantifier,_), 
	fol_quantifier(Quantifier,Type),
	sy_quantifiers(Quantified,Type,Variables,Matrix),
	sy_otter(Matrix,Subformula),
	my_append(Subformula,[')'],Subformula1),
	my_append(['(',Quantifier|Variables],Subformula1,Result),!.


sy_otter(Formula,[Formula]).

/* Flattening of nested 'and' and 'or' trees */

sy_flatten(Formula,Connective,Flattened) :-
	functor(Formula,Connective,_), 
	arg(1,Formula,A),
	arg(2,Formula,B),
	sy_flatten(A,Connective,Afl),
	sy_flatten(B,Connective,Bfl),	
	my_append(Afl,[Connective|Bfl],Flattened),!.

sy_flatten(Formula,_,Flattend) :-
	sy_otter(Formula,Flattend),!.

/* Collection of nested quantified variables of the same type */

sy_quantifiers(Formula,Type,Variables,Matrix) :-
	functor(Formula,Quantifier,_), 
	fol_quantifier(Quantifier,Type),
	arg(1,Formula,Variable),
	arg(2,Formula,Subformula),
	sy_quantifiers(Subformula,Type,Vars,Matrix),
	((Vars=[],Variables = [Variable]);Variables = [Variable|Vars]).
	
sy_quantifiers(Formula,_,[],Formula).



sy_otter_list([],[]).
sy_otter_list([H|T],[Ht|Tt]) :-
	sy_otter(H,Ht),
	sy_otter_list(T,Tt),!.


/* Print functions for lists */

sy_print(_,[]).
sy_print(Stream,[X|Tail]) :- 
	quote(Quote),
	(sy_dangerous(X) -> 
	 (write(Stream,Quote),write(Stream,X),write(Stream,Quote));
	    write(Stream,X)),
	(tk_separator(_,X);
	    (Tail = [Char|_], tk_separator(_,Char));
	    write(Stream,' ')),
	sy_print(Stream,Tail),!.
sy_print(Stream,X) :- write(Stream,X).



ot_print_list(_,[]).
ot_print_list(Stream,[H|T]) :-
	ot_print(Stream,H),write(Stream,'.'),nl(Stream),
	ot_print_list(Stream,T),!.



ot_print(_,[]).
ot_print(Stream,[H|T]) :-
	write(Stream,H),
	ot_print(Stream,H,T).

ot_print(_,_,[]).
ot_print(Stream,'(',[H|T]) :-
	!,write(Stream,H),
	ot_print(Stream,H,T).

ot_print(Stream,_,[H|T]) :-
	write(Stream,' '),
	write(Stream,H),
	ot_print(Stream,H,T).


ot_write(Stream,Type,Formulae) :-
	sy_otter_list(Formulae,List),
	write(Stream,'formula_list('),write(Stream,Type),write(Stream,').'),nl(Stream),
	ot_print_list(Stream,List), 
	write(Stream,'end_of_list.'),
	nl(Stream),nl(Stream). 


/************************************************************
*
*		VARIOUS USEFUL FUNCTIONS
*
************************************************************/

my_retractall(X) :- retract(X),fail.
my_retractall(X) :- retract((X :- _)),fail.
my_retractall(_).



/* Example: new_symbol(v,v1)*/

:-dynamic(new_symbol_counter/2).

new_symbol(Prefix,Symbol) :-
		( retract(new_symbol_counter(Prefix,Value)) ; Value = 0 ),
		NewValue is Value+1,
		asserta(new_symbol_counter(Prefix,NewValue)),
		name(Prefix,P),
		name(NewValue,N),
		my_append(P,N,SymbolList),
		name(Symbol,SymbolList), !.

/* my_append also appends elements which are not lists as singleton list */

my_append([],A,A).
my_append(A,[],A).
my_append([A|B],[C|D],[A|E]) :- my_append(B,[C|D],E),!.
my_append(A,[H|T],[A,H|T]) :- !.
my_append([H|T],A,E) :- my_append([H|T],[A],E),!.
my_append(A,B,[A,B]).


my_member(X,[Y|_]) :- 
	X == Y,!.
my_member(X,[_|Y]) :- !,my_member(X,Y).

my_not(X) :- call(X),!,fail.
my_not(_).


/* Checking whether one term occurs inside another */

in(X,Y)     :-  X == Y,!.
in(_,Y)     :- (atomic(Y);var(Y)),!,fail.
in(_,[])    :- !,fail. 
in(X,[H|T]) :- !,(in(X,H);in(X,T)).
in(X,Term) :- 
	functor(Term,_,N),
	arguments(Term,N,Args),
	in(X,Args).

/* Concatenation of two atoms */

my_concat(Atom1,Atom2,Atom) :-
	name(Atom1,List1),
	name(Atom2,List2),
	my_append(List1,List2,List),
	name(Atom,List).


/* arguments(Term,N,Arg) computes the list of N arguments of the term Term.
   The Term must have at least N arguments. 
   If Term has more than N arguments, the first N ones are extracted as a list. */
   

arguments(_,0,[]).
arguments(Term,N,Arguments) :-
	get_arguments(Term,N,1,Arguments),!.

get_arguments(Term,N,N,[Argument]) :-
	arg(N,Term,Argument).

get_arguments(Term,N,M,[Arg|Args]) :-
	arg(M,Term,Arg),
	M1 is M+1,
	get_arguments(Term,N,M1,Args).


/* Substitution of symbols (incl. functions) inside terms. 
   subst replaces an Old symbol by a New symbol in the Term. */

subst(Term,Old,New,Result) :-
	substs(Term,[Old],[New],Result).


/* This function substitutes the terms in a list of Old terms by the 
   corresponding New term in the list of new terms. */


substs(Term,Old,New,Result):-
	su_member(Term,Old,New,Result),!.

substs(Term,_,_,Term) :- 
	(atomic(Term);var(Term)),!.

substs(Term,Old,New,Result) :-
	functor(Term,Operator,N),
	arguments(Term,N,Arguments),
	substs_list(Arguments,Old,New,Sarguments),
	(su_member(Operator,Old,New,Noperator) ->
	 (Newoperator = Noperator);
	    (Newoperator = Operator)),
	Result =.. [Newoperator|Sarguments].



/* Substitution in a list of terms */

substs_list([],_,_,[]).
substs_list([H|T],Old,New,[Hs|Ts]) :-
	substs(H,Old,New,Hs),
	substs_list(T,Old,New,Ts).

su_member(X,[Y|_],[Z|_],Z) :- 
	X == Y,!.
su_member(X,[_|Y],[_|Z],U) :- !,su_member(X,Y,Z,U).


/* Generation of a list of different unbounded variables */


new_vars([],[]) :- !.
new_vars([_|T],[_|List]) :-
	new_vars(T,List).


/* Replacing arguments of a term by fresh variables */

var_abstract(Term,Term,[],[]) :-
	atom(Term).

var_abstract(Term,Aterm,Constants,Variables) :-
	functor(Term,F,N),
	arguments(Term,N,Constants),
	new_vars(Constants,Variables),
	Aterm =.. [F|Variables].


/************************************************************
*
*                  ERROR MESSAGES 
*
************************************************************/


er_parentheses(Atom,List) :-
	write('Parenthesis mismatch while parsing '),
	write(Atom),nl,
	write(List),nl.
    
er_parse_list(X) :-
	write(X),write(' is not a list'),nl.

er_parse_report(Name,Error) :-
	(var(Error),!);
	(write('error while parsing '), write(Name),nl,
	write('processing continues, but this information will be ignored!'),nl).

er_definition(Type,Name) :-
	write('no '),write(Type),write(' '),write(Name),write(' found'),nl.



er_rr_activate(Type,X) :-
	write('rewrite system '),write(Type),
	write(': '), write(X),
	write(' is not a LIST of rewrite rule names'),nl.

er_rr_noimp(Name,X) :-
	write('rewrite rule component '),
	write(Name),write(': '),write(X),
	write(' is not an implication'),nl.

er_rr_max(K) :-
	write('the number of recursive rewrite calls exceeds the limit '),write(K),nl,
	write('rewriting is stopped. Are you sure your rewrite system is terminating?'),nl.


er_op_prec(Name,Prec) :-
	write('operator '), write(Name),
	write(' has a precedence declaration '), write(Prec),nl,
	write('which is neither undefined (a variable) nor of the form op(Number,Parenthesis, Operator'),nl,
	write('precedence declaration ignored!'),nl.

er_op_def(Name,Definition) :-
	write('operator '),write(Name),
	write(' has a definition '),write(Definition),nl,
	write('which is neither a rewrite rule of the form Left -> Right'),nl,
	write('nor a semantics definition of the form w |= Phi <-> ...'),nl.

er_op_def1(Name,Definition) :-
	write('operator '),write(Name),
	write(' is supposed to have a rewrite rule, but the definition'),nl,
	write(Definition),write(' is not an implication'),nl.


er_op_precnumber(Name,Precedence) :-
	write('operator '),write(Name),
	write(' is supposed to get a new precedence number: '),write(Precedence),nl,
	write('but there is no op(..,..,..) declaration in define(operator,..).'),nl,
	write('new precedence ignored'),nl.

er_gd_more(Name,More) :-
	write('operator '),write(Name),
	write(': '),write(More),write(' part ignored!'),nl.

er_gd_var(Type,Name) :-
	write('sorry, but both '),write(Type),write(' and '),write(Name),
	write(' must not be variables.'),nl.

er_no_truth_condition :-
	clause(translate(_,_),_);
	(write('no truth condition defined!'),nl,fail).


er_ci_pred(Formulae,P) :-
	write('predicates '),write(P),
	write(' do not occur in the formulae '),
	write(Formulae),nl.



/***************************************************************************
****************************************************************************
*
*                          CIRCUMSCRIPTION  PART
*
****************************************************************************
***************************************************************************/

/***************************************************************************
* The circ predicate below computes the original second order circumscription 
* formula and generates an input file for the SCAN program. 
* 
* Circumscription has two parameters, the predicates to be minimized and 
* the predicates to be varied. 
* The original circumscription definition is 

* circ(F(P,Z),P,Z) = F & (all P*,Z* (F(P*,Z*) & (P* -> P)) -> (P -> P*))
*  
* where P are the predicates to be minimized and Z are the predicates to 
* be varied. (P* -> P) is short for all x1,...,xn P*(x1,...,xn) -> P(x1,...,xn). 
* 
* The SCAN input file gets F(P*,Z*) & (P* -> P) positive and (P -> P*)
* negative, and the original F(P,Z) in the usable list for simplification 
* purposes. 
*
***************************************************************************/

circ(Formulae,P) :-
	circ(Formulae,P,[]).

circ(Formulae,P,Z) :-
	ci_circ(Formulae,P,Z,Pformulae,Circumscribed,Predicates),!,
	scan_file(File), 
	open(File,write,Stream), 
	sc_scan_header(Stream,Predicates), 
	sc_header(Stream),
	ot_write(Stream,usable,Pformulae),
	ot_write(Stream,sos,Circumscribed),
	close(Stream).


/* Generation of the circumscription formulae */

ci_circ(Formulae,P,Z,Pformulae,Circumscribed,Predicates) :-
	atom(P),P \== [],!,
	ci_circ(Formulae,[P],Z,Pformulae,Circumscribed,Predicates).

ci_circ(Formulae,P,Z,Pformulae,Circumscribed,Predicates) :-
	atom(Z),Z \== [],!,
	ci_circ(Formulae,P,[Z],Pformulae,Circumscribed,Predicates).


ci_circ(Formulae,P,Z,Pformulae,Circumscribed,Predicates) :-	
	as_constants(parse_list(Formulae,Pformulae,Error)),	
	er_parse_report(Pformulae,Error),
	var(Error),              /* Abort */
	ci_arities(P,Pa,Pformulae),
	ci_cleanup(P,Pa,Pc,Pac),
	(Pc = [] ->
	 (er_ci_pred(Formulae,P),fail);
	    (ci_arities(Z,Za,Pformulae),
	     ci_cleanup(Z,Za,Zc,_),
	     ci_new_symbols(Pc,Ps),
	     ci_new_symbols(Zc,Zs),
	     my_append(Pc,Zc,PZ),
	     my_append(Ps,Zs,PZs),
	     substs(Pformulae,PZ,PZs,Fnew),
	     ci_imp(Ps,Pc,Pac,Psp),
	     ci_imp(Pc,Ps,Pac,Pps),
	     ci_conjunct(Pps,Conjunct),
	     fol_connective(Neg,negation),
	     Ppsn =.. [Neg,Conjunct],
	     my_append(Ps,Zs,Predicates),
	     my_append(Fnew,Psp,Circ1),
	     my_append(Circ1,[Ppsn],Circumscribed))).


ci_imp([],[],_,[]).

ci_imp([Fh|Ft],[Th|Tt],[Ah|At],[Resh|Rest]) :-
	ci_vars(Ah,Vars),
	From =.. [Fh|Vars],
	To   =.. [Th|Vars],
	fol_connective(Imp,implication),
	Formula =.. [Imp,From,To],
	ci_quantifiers(Formula,Vars,Resh),
	ci_imp(Ft,Tt,At,Rest).


ci_quantifiers(Formula,[],Formula).
ci_quantifiers(Formula,[H|T],Quantified) :-
	fol_quantifier(Q,universal),
	Quantif =.. [Q,H,Formula],
	ci_quantifiers(Quantif,T,Quantified).


ci_conjunct([H],H).
ci_conjunct([H|T],Conj) :-
	ci_conjunct(T,Tc),
	fol_connective(And,conjunction),
	Conj =.. [And,H,Tc].




ci_vars(0,[]) :- !.
ci_vars(N,[Var|Vars]) :-
	new_symbol(x,Var),
	M is N-1,
	ci_vars(M,Vars).


/* Determining the arities of the predicate symbols */

ci_arities([],[],_).
	
ci_arities([H|T],[Ha|Ta],Formulae) :-
	(ci_arity(H,Ha,Formulae);true),
	ci_arities(T,Ta,Formulae).
	

ci_arity(_,_,[]) :- !,fail.

ci_arity(Predicate,Arity,[H|T]) :-
	!,
	(ci_arity(Predicate,Arity,H);
	ci_arity(Predicate,Arity,T)).

ci_arity(Predicate,0,Formula) :-
	(atom(Formula);var(Formula)),!,
	 Predicate == Formula.

ci_arity(Predicate,Arity,Formula) :-
	functor(Formula,F,Arity),
	Predicate == F,!.

ci_arity(Predicate,Arity,Formula) :-
	functor(Formula,_,N),
	arguments(Formula,N,Subformulae),
	ci_arity(Predicate,Arity,Subformulae).

/* Eliminating predicates not occurring at all */

ci_cleanup([],[],[],[]).

ci_cleanup([_|Tp],[Ha|Ta],Tpc,Tac) :-
	var(Ha),!,
	ci_cleanup(Tp,Ta,Tpc,Tac).

ci_cleanup([Hp|Tp],[Ha|Ta],[Hp|Tpc],[Ha|Tac]) :-
	ci_cleanup(Tp,Ta,Tpc,Tac).

/* Generation of the P* predicates */
	
ci_new_symbols([],[]).
ci_new_symbols([H|T],[Hn|Tn]) :-
	my_concat(H,'_circ',Hn),
	ci_new_symbols(T,Tn).
