/************************************************************************** * * 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).