1% MODULE g2_ops EXPORTS 2:- module( g2_ops, 3 [ intra_construct1/5, % ITOU-like 4 intra_construct1/6, % give name of new pred 5 intra_construct1/7, % give name & bound for common generalizations 6 intra_construct2/5, % CIGOL-like 7 intra_construct2/6, % give name of new pred 8 intra_construct2/7, % give name & bound for common generalizations 9 g2_op/5, 10 apply_g2/5, 11 apply_g2/3, 12 apply_g2/2 13 ]). 14 15% IMPORTS 16:- use_module(home(lgg), 17 [lgti/6,lgg/5,buildlgg/4, 18 gti/5,lgti/5]). %%%diese f"ur lgti/6 ersetzen (ohne Bound) 19:- use_module(home(kb), 20 [get_clause/5,store_clause/4,delete_clause/1,delete_all/1]). 21:- use_module(home(var_utils), 22 [relevant_vars2/6,relevant_vars3/6, 23 skolemize/3,deskolemize/3,replace/4,inv_replace/4, 24 exists_intersect/3,findargs/3,allarg/4,buildrelterms/6]). 25:- use_module(home(div_utils), 26 [effaceall/3,genterm_test/2]). 27:- use_module(home(g1_ops), 28 [g1_op/4]). 29:- use_module(home(environment), 30 [oracle/2,confirm/2,get_ci/2]). 31:- use_module(home(evaluation), 32 [complexity/2]). 33:- use_module_if_exists(library(strings), 34 [gensym/2]). 35:- use_module_if_exists(library(basics), 36 [member/2]). 37:- use_module_if_exists(library(sets), 38 [subtract/3]). 39:- use_module_if_exists(library(not), 40 [(once)/1]). 41 42 43% METAPREDICATES 44% none 45 46 47%*********************************************************************** 48%* 49%* module: g2_ops.pl 50%* 51%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend date:12/92 52%* 53%* changed: 54%* 55%* description: Intra-Construction, G2 56%* 57%* see also: 58%* 59%*********************************************************************** 60 61 62%*********************************************************************** 63%* 64%* predicate: intra_construct1/5/6/7 65%* 66%* syntax: intra_construct1(+C1,+C2,-A,-B1,-B2) 67%* intra_construct1(+C1,+C2,-A,-B1,-B2,PName) 68%* intra_construct1(+C1,+C2,-A,-B1,-B2,PName,Bound) 69%* 70%* args: C1,C2,A,B1,B2: references to clauses in kb 71%* PName: atom - name of invented predicate 72%* Bound: integer 73%* 74%* description: intra-construction where C1,C2 are at bottom of W, 75%* A at the center top, B1,B2 at outside top positions. 76%* S1(A) in C1, S2(A) in C2; the substitutions 77%* between Bi & Ci are empty. 78%* Uses an ITOU-like heursitics for determining relevant 79%* variables for the new predicate 80%* Our intra-construction will only work, if the two 81%* input clauses require the same number of arguments 82%* for the newly invented predicate. 83%* This restriction is not part of the original 84%* definition of intra-construction, but its at least 85%* a very useful heuristics. If the restriction does not 86%* fit your needs, change it in relevant_vars/3, 87%* module "var_utils.pl". 88%* 89%* example: 90%* 91%* peculiarities: backtracking over lgti/6 until the same number 92%* of arguments is reached. 93%* 94%* see also: 95%* 96%*********************************************************************** 97 98intra_construct1(IDC1,IDC2,IDA,IDB1,IDB2):- 99 gensym( new_pred, NewPred), 100 intra_construct1(IDC1,IDC2,IDA,IDB1,IDB2,NewPred). 101 102 103intra_construct1(IDC1,IDC2,IDA,IDB1,IDB2,NewPred):- 104 intra_construct1(IDC1,IDC2,IDA,IDB1,IDB2,NewPred,10). 105 106intra_construct1(IDC1,IDC2,IDA,IDB1,IDB2,NewPred,Bound):- 107 atom(NewPred), 108 get_clause( IDC1,_,_,C1,_), 109 get_clause( IDC2,_,_,C2,_), 110 !, 111 lgti(C1,C2,G,S1,S2,Bound), % G is common generalization 112 113 once(( 114 relevant_vars3(C1,C2,G,S1,S2,Vars), %%% ITOU - like 115 NewLit =.. [NewPred | Vars], 116 % build clause in center top 117 append(G,[NewLit:n],A), 118 119 120 % build clause at top left 121 copy_term( (C1,G,S1,NewLit), (C11,G11,S11,NewLit11) ), 122 skolemize( (C11,G11,S11,NewLit11), Phi1, (C12,G12,S12,NewLit12) ), 123 replace( G12,S12,G13,S12 ), 124 replace( [NewLit12],S12,[NewLit13],S12), 125 subtract( C12,G13,B1BodyS), % 126 B1S = [ NewLit13:p | B1BodyS ], 127 deskolemize(B1S,Phi1,B1), 128 129 130 % build clause at top right 131 copy_term( (C2,G,S2,NewLit), (C21,G21,S21,NewLit21) ), 132 skolemize( (C21,G21,S21,NewLit21), Phi2, (C22,G22,S22,NewLit22) ), 133 replace( G22,S22,G23,S22 ), 134 replace( [NewLit22],S22,[NewLit23],S22), 135 subtract( C22,G23,B2BodyS), 136 B2S = [ NewLit23:p | B2BodyS ], 137 deskolemize(B2S,Phi2,B2), 138 139 store_clause(_,A,ic,IDA), 140 store_clause(_,B1,ic,IDB1), 141 store_clause(_,B2,ic,IDB2) 142 )). 143 144 145 146%*********************************************************************** 147%* 148%* predicate: intra_construct2/5/6/7 149%* 150%* syntax: intra_construct2(+C1,+C2,-A,-B1,-B2) 151%* intra_construct2(+C1,+C2,-A,-B1,-B2,PName) 152%* intra_construct2(+C1,+C2,-A,-B1,-B2,PName,Bound) 153%* 154%* args: C1,C2,A,B1,B2: references to clauses in kb 155%* PName: atom - name of invented predicate 156%* Bound: integer 157%* 158%* description: intra-construction where C1,C2 are at bottom of W, 159%* A at the center top, B1,B2 at outside top positions. 160%* S1(A) in C1, S2(A) in C2; the substitutions 161%* between Bi & Ci are empty. 162%* Uses a CIGOL-like heursitics for determining relevant 163%* variables for the new predicate 164%* 165%* example: 166%* 167%* peculiarities: backtracking over lgti/6 until the same number 168%* of arguments is reached. 169%* 170%* see also: 171%* 172%*********************************************************************** 173 174intra_construct2(IDC1,IDC2,IDA,IDB1,IDB2):- 175 gensym( new_pred, NewPred), 176 intra_construct2(IDC1,IDC2,IDA,IDB1,IDB2,NewPred). 177 178 179intra_construct2(IDC1,IDC2,IDA,IDB1,IDB2,NewPred):- 180 intra_construct2(IDC1,IDC2,IDA,IDB1,IDB2,NewPred,10). 181 182intra_construct2(IDC1,IDC2,IDA,IDB1,IDB2,NewPred,Bound):- 183 atom(NewPred), 184 get_clause( IDC1,_,_,C1,_), 185 get_clause( IDC2,_,_,C2,_), 186 !, 187 lgti(C1,C2,G,S1,S2,Bound), % G is common generalization 188 189 once( ( 190 relevant_vars2(C1,C2,G,S1,S2,Vars), %%% CIGOL - like 191 NewLit =.. [NewPred | Vars], 192 % build clause in center top 193 append(G,[NewLit:n],A), 194 195 196 % build clause at top left 197 copy_term( (C1,G,S1,NewLit), (C11,G11,S11,NewLit11) ), 198 skolemize( (C11,G11,S11,NewLit11), Phi1, (C12,G12,S12,NewLit12) ), 199 replace( G12,S12,G13,S12 ), 200 replace( [NewLit12],S12,[NewLit13],S12), 201 subtract( C12,G13,B1BodyS), % 202 B1S = [ NewLit13:p | B1BodyS ], 203 deskolemize(B1S,Phi1,B1), 204 205 206 % build clause at top right 207 copy_term( (C2,G,S2,NewLit), (C21,G21,S21,NewLit21) ), 208 skolemize( (C21,G21,S21,NewLit21), Phi2, (C22,G22,S22,NewLit22) ), 209 replace( G22,S22,G23,S22 ), 210 replace( [NewLit22],S22,[NewLit23],S22), 211 subtract( C22,G23,B2BodyS), 212 B2S = [ NewLit23:p | B2BodyS ], 213 deskolemize(B2S,Phi2,B2), 214 215 store_clause(_,A,ic,IDA), 216 store_clause(_,B1,ic,IDB1), 217 store_clause(_,B2,ic,IDB2) 218 )). 219 220 221%******************************************************************************** 222%* 223%* predicate: g2_op/5 224%* 225%* syntax: g2_op ( + C1_ID, + C2_ID, - A_ID, - B1_ID, - B2_ID) 226%* 227%* args: Ci_ID ... IDs of resolvent clauses C1 and C2 to be generalized 228%* A_ID ... ID of common parent clause A 229%* Bi_ID ... IDs of corresponding parent clauses B1 and B2 230%* 231%* description: Implementation of Ruediger Wirth's G2-operator for inverse 232%* resolution corresponding to his 1989 PhD thesis. 233%* We generalize the Ci using Plotkin's LGG, then build a new 234%* predicate as resolution literal, find the argument terms for the 235%* new predicate (in a heuristic manner) and finally build the Bi 236%* using our well-known G1-operator. 237%* The compression achieved is evaluated thru a simple, though quite 238%* sophisticated complexity heuristic (cf. module 'complexity'). 239%* If the resulting clauses show some compression, the are passed 240%* to the oracle for confirmation and the user gets a chance to 241%* rename the new predicate. 242%* Clauses which become obsolete during the process will be deleted. 243%* 244%* example: 245%* 246%* peculiarities: The procedure 'inv_replace' might yield unsatisfying results, 247%* due to the possible ambiguity of inverse substitution. 248%* 249%* see also: 250%* 251%******************************************************************************** 252 253g2_op(C1, C2, A, B1, B2) :- 254 get_clause(C1,_,_,C1list,_), 255 get_clause(C2,_,_,C2list,_), 256 lgg(C1list,C2list,Clgg,S1,S2), % Clgg = A\{L} 257 not_unary(Clgg), % heuristic proc. 258 buildrelterms(C1list,C2list,Clgg,S1,S2,Terms), % Terms = List of Args for L 259 buildreslit(Terms,L), % L = resolution literal 260 buildparentA(Clgg,L,Alist), % Alist = parentclause A 261 store_clause(_,Alist,g2,A), 262 (g1_op(C1,A,B1,g2g1), % Bi = parentclauses 263 g1_op(C2,A,B2,g2g1) -> 264 ( compression_heuristic([A,B1,B2], [C1,C2]) -> 265 confirm([A,B1,B2], L), 266 delete_all([C1,C2]), 267 nl, write('Resolvent clauses deleted.'); 268 nl, write('G2: No compression achieved.'), nl, fail 269 ); 270 delete_clause(A) ). 271 272 273%******************************************************************************** 274%* 275%* predicate: apply_g2/3 - tries to apply the G2-operator to a set of clauses Ci. 276%* The output will be a kb reference of the common parent 277%* clause A and a list of id's for parent clauses Bi. 278%* 279%* Bi A Bj 280%* \ / \ / 281%* \ / \ / 282%* Ci Cj 283%* apply_g2/2 - ORACLE is asked to enter the Id's of resolvent clauses 284%* Ci one by one. This continues until oracle says 'stop'. 285%* Doubles and answers which are not a number are ignored. 286%* Finally apply_g2/3 is called. 287%* apply_g2/5 - simply calls g2_op/5 288%* 289%* syntax: apply_g2( + CC, - A, -BB), apply_g2( - A, -BB), 290%* apply_g2 ( + C1_ID, + C2_ID, - A_ID, - B1_ID, - B2_ID) 291%* 292%* args: CC ... Id-list of resolvent clauses Ci to be generalized 293%* A ... Id of common parent clause A 294%* BB ... Id-list of corresponding parent clauses Bi 295%* C_ID, A_ID, B_ID .. as for g2_op/5 296%* 297%* description: 298%* 299%* example: 300%* 301%* peculiarities: 302%* 303%* see also: 304%* 305%********************************************************************************% 306 307apply_g2(C1, C2, A, B1, B2) :- 308 g2_op(C1, C2, A, B1, B2), !. 309 310 311apply_g2(A, BB) :- 312 get_ci([],CC), 313 apply_g2(CC, A, BB), !. 314 315 316apply_g2(CC, A, BB) :- 317 sort(CC,CCsort), 318 gensym(new_p,N), 319 findall(Aij, ( member(Ci,CCsort), member(Cj,CCsort), 320 Ci < Cj, g2_op_A(Ci,Cj,N,Aij) ), AA), 321 AA = [A1|An], 322 buildlgg(An,A1,A,g2), 323 delete_all(AA), 324 findall(Bi, ( member(Ci,CC), 325 g1_op(Ci,A,Bi,g2g1) ), BB), 326 length(CC,NoC), 327 ( length(BB,NoC) -> 328 ( compression_heuristic([A|BB], CC) -> 329 confirm([A|BB], N), 330 delete_all(CC), 331 nl, write('Resolvent clauses deleted.'); 332 nl, write('G2: No compression achieved.'), nl, fail 333 ); 334 delete_all(BB), 335 delete_clause(A), 336 fail 337 ). 338 339 340g2_op_A(C1, C2, Name, A) :- 341 get_clause(C1,_,_,C1list,_), 342 get_clause(C2,_,_,C2list,_), 343 lgg(C1list,C2list,Clgg,S1,S2), % Clgg = A\{L} 344 buildrelterms(C1list,C2list,Clgg,S1,S2,T), % T = List of Args for L 345 not_unary(Clgg), % heuristic proc. 346 length(T,N), 347 functor(L,Name,N), % Name = common for all L's 348 setargs(N,T,L), % L = resolution literal 349 buildparentA(Clgg,L,Alist), % parentclause A 350 store_clause(_,Alist,g2,A). 351 352 353 354%************************************************************************ 355%* 356%* predicate: not_unary/1 357%* 358%* syntax: not_unary(+CL) 359%* 360%* args: CL .. clause in list representation 361%* 362%* description: fails, if CL is a unary clause or a unary goal 363%* 364%* example: 365%* 366%* peculiarities: 367%* 368%* see also: 369%* 370%************************************************************************ 371 372not_unary([_:p]) :- nl, write('No compression achievable.'), !,fail. 373not_unary([true:p,_]) :- nl, write('No compression achievable.'), !,fail. 374not_unary(_). 375 376 377%************************************************************************ 378%* 379%* predicate: buildreslit/2 380%* 381%* syntax: buildreslit(+TermList,-Lit) 382%* 383%* args: TermList is the list of relevant argument terms, Lit is the resolution 384%* literal (with a new predicate symbol) 385%* 386%* description: constructs the resolution literal 387%* 388%* example: 389%* 390%* peculiarities: 391%* 392%* see also: 393%* 394%************************************************************************ 395 396buildreslit(T,L) :- 397 length(T,N), 398 gensym(new_p,F), 399 functor(L,F,N), 400 setargs(N,T,L). 401 402setargs(0,[],_) :- !. 403setargs(N,[Arg1|Rest],L) :- 404 arg(N,L,Arg1), 405 M is N-1, 406 setargs(M,Rest,L). 407 408 409%************************************************************************ 410%* 411%* predicate: buildparentA/3 412%* 413%* syntax: buildparentA(+A_L,+Lit,-AL) 414%* 415%* args: A_L ... A\{Lit} the lgg of C1 and C2 416%* Lit ... the new predicate literal 417%* AL ... A\{Lit} + {Lit} 418%* 419%* description: adds the new predicate literal Lit either as head or 420%* as body literal to A_L 421%* 422%* example: 423%* 424%* peculiarities: 425%* 426%* see also: 427%* 428%************************************************************************ 429 430buildparentA([true:p|Rest],L,[L:p|Rest]) :- !. 431buildparentA(List,L,Alist) :- append(List,[L:n],Alist), !. 432 433 434%************************************************************************ 435%* 436%* predicate: compression_heuristic/2 437%* 438%* syntax: compression_heuristic(+NewIDs,+OldIDs) 439%* 440%* args: NewIDs, OldIDs ... clauseIDs 441%* 442%* description: succeeds if the size of the clauses NewIDs is smaller 443%* than that of the clauses OldIDs 444%* 445%* example: 446%* 447%* peculiarities: 448%* 449%* see also: 450%* 451%************************************************************************ 452 453compression_heuristic( New_cl, Old_cl) :- 454 complexity(Old_cl, Cold), 455 complexity(New_cl, Cnew), 456 ( Cnew < Cold -> 457 true; 458 delete_all(New_cl), fail 459 )