1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2% 3% Copyright 2003-2010, Renate Schmidt, University of Manchester 4% 2009-2010, Ullrich Hustadt, University of Liverpool 5% 6%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 7 8prove(Fml, Result) :- 9 provable([], Fml, Result). 10 11provable(Fml, Result) :- 12 provable([], Fml, Result). 13 14provable(Axioms, FmlInput, unprovable) :- 15 retractall(consistent(_,_,_)), 16 retractall(inconsistent(_)), 17 retractall(reduced(_,_,_)), 18 % Axioms is a set of non-logical axioms, i.e. a background theory 19 create_search_output_file, 20 21 negated_formula(FmlInput, Fml), 22 23 nl, 24 pdl_write('** Input: '), pdl_write(Fml), pdl_nl, 25 26 % Transform Axioms and Fml into negation normal form 27 pdl_write('** NFAxioms: '), pdl_nl, 28 normalise(Axioms, NFAxioms), 29 normalise(Fml, [], NFFml, Paths), 30 31 pdl_write('** NFFml: '), pdl_write(NFFml), pdl_nl, 32 pdl_write('Paths = '), pdl_write(Paths), pdl_nl, 33 34 (get_output_format(latex) -> 35 latex_output(begin) 36 ; 37 true), 38 39 % Search for a proof or a model 40 search(NFAxioms, NFFml), !, 41 42 (get_output_format(latex) -> 43 latex_output(end) 44 ; 45 true). 46 47provable(_, _, provable) :- 48 print_result('Refutation proof found'), 49 (get_output_format(latex) -> 50 latex_output(end) 51 ; 52 true). 53 54%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 55 56satisfiable(Fml, Result) :- 57 satisfiable([], Fml, Result). 58 59satisfiable(Axioms, FmlInput, satisfiable) :- 60 retractall(consistent(_,_,_)), 61 retractall(inconsistent(_)), 62 % Axioms is a set of non-logical axioms, i.e. a background theory 63 create_search_output_file, 64 65 FmlInput = Fml, 66 67 nl, 68 pdl_write('** Input: '), pdl_write(Fml), pdl_nl, 69 70 % Transform Axioms and Fml into negation normal form 71 pdl_write('** NFAxioms: '), pdl_nl, 72 normalise(Axioms, NFAxioms), 73 normalise(Fml, [], NFFml, Paths), 74 75 pdl_write('** NFFml: '), pdl_write(NFFml), pdl_nl, 76 pdl_write('Paths = '), pdl_write(Paths), pdl_nl, 77 78 (get_output_format(latex) -> 79 latex_output(begin) 80 ; 81 true), 82 83 % Search for a proof or a model 84 search(NFAxioms, NFFml), !, 85 86 (get_output_format(latex) -> 87 latex_output(end) 88 ; 89 true). 90 91satisfiable(_, _, unsatisfiable) :- 92 print_result('Refutation found'), 93 (get_output_format(latex) -> 94 latex_output(end) 95 ; 96 true). 97 98%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 99 100negated_formula(Fml, not(Fml)) :- 101 get_negate_first(yes), !. 102 103negated_formula(Fml, Fml). 104 105%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 106% 107% search(+Axioms, +Formula) 108% 109% Formula is a term including the formula to be tested for 110% satisfiability and encodings of the positions of all subformulae 111% The formula is in negation normal form. 112 113search(Axioms, Fml) :- 114 set_satisfiable_flag(-1), 115 set_states_counter(0), 116 set_proof_steps_counter(-1), 117 set_branch_point_counter(0), 118 set_sat_reuse_counter(0), 119 set_unsat_reuse_counter(0), 120 121 print_proof_step(0, Axioms, '[theory]'), 122 print_proof_step(0, Fml, '[given]'), 123 124 search_state(Axioms, [Fml], 0, [], NewBranch, [], NewEventualities, [], _), 125 pdl_write('In search, State : '), pdl_write(0), pdl_nl, 126 pdl_write(' Axioms : '), pdl_write(Axioms), pdl_nl, 127 pdl_write(' NewBranch : '), pdl_write(NewBranch), pdl_nl, 128 pdl_write(' NewEventualities : '), pdl_write(NewEventualities), pdl_nl, 129 test_ignorability(NewBranch, NewEventualities), 130% write('Remembering consistent set - state shown consistent'), write(FmlList), nl, 131% print_proof_step(State, consistent_set(FmlList), '[consistent set]'), 132% store_consistent(FmlList,Branch,NewBranch,Eventualities,NewEventualities) 133 print_result('Satisfiable branch found'). 134 135%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 136% 137% search_state(+Axioms, +Unexpanded, +State, +Branch, -NewBranch, 138% +Eventualities, -NewEventualities) 139% 140% Test whether a model for < State : Unexpanded > can be constructed. 141% The formulae in Unexpanded are assumed to be in negation normal form. 142% * +Branch is the branch constructed so far (i.e. the segment from the 143% root state/world to the parent state/world of +State) 144% * -NewBranch will be a \pi-completed branch extending +Branch 145% * +Eventualities will be the eventualities fulfilled so far on +Branch 146% * -NewEventualities will be eventualities fulfilled on -NewBranch 147% Note: The predicate search_state is also used in reduce_existentials. 148 149search_state(Axioms, Unexpanded, State, Branch, NewBranch, 150 Eventualities, NewEventualities, IDT, ODT) :- 151 pdl_write('In search_state, State : '), pdl_write(State), pdl_nl, 152 pdl_write(' Unexpanded : '), pdl_write(Branch), pdl_nl, 153 154 print_proof_step(State, Axioms, '[theory-inst]'), 155 append(Unexpanded, Axioms, UnexpandedPlusAxioms), 156 % Remember: +LocalEventualities in the following call to reduce_local are 157 % the eventualities fulfilled in the current state +State 158 reduce_local(UnexpandedPlusAxioms, State, [], Workedoff, 159 Universal, Existential, LocalEventualities, IDT, ODT_RL), 160 161 eliminate_duplicates(Workedoff, SimplifiedWorkedoff), 162 eliminate_duplicates(Universal, SimplifiedUniversal), 163 eliminate_duplicates(Existential, SimplifiedExistential), 164 165 pdl_write(' Branch : '), pdl_write(Branch), pdl_nl, 166 pdl_write(' SimplifiedWorkedoff : '), pdl_write(SimplifiedWorkedoff), pdl_nl, 167 pdl_write(' SimplifiedUniversal : '), pdl_write(SimplifiedUniversal), pdl_nl, 168 pdl_write(' SimplifiedExistential : '), pdl_write(SimplifiedExistential), pdl_nl, 169 pdl_write(' LocalEventualities : '), pdl_write(LocalEventualities), pdl_nl, 170 171 test_unsatisfiability(State, SimplifiedWorkedoff, SimplifiedWorkedoff), 172 173 merge_set(SimplifiedWorkedoff, SimplifiedExistential, Aux), 174 merge_set(Aux, SimplifiedUniversal, FmlList), 175 176 pdl_write(' FmlList : '), pdl_write(FmlList), pdl_nl, 177 178 prefix_to_list(State,StateList), 179 assert(reduced(ODT_RL, StateList, FmlList)), 180 (known_consistent(FmlList,BranchForFmlList,EventualitiesForFmlList) -> 181 pdl_write(' is known to be consistent'), pdl_nl, 182 append(BranchForFmlList,Branch,NewBranch), 183 append(EventualitiesForFmlList,Eventualities,NewEventualities) 184 ; 185 extend_branch(State, FmlList, Branch, ExtendedBranch), 186 pdl_write(' ExtendedBranch : '), pdl_write(ExtendedBranch), pdl_nl, 187 188 merge_set(Eventualities, LocalEventualities, ExtendedEventualities), 189 pdl_write(' ExtendedEventualities : '), pdl_write(ExtendedEventualities), pdl_nl, 190 191 search_state_aux(Axioms, SimplifiedExistential, 192 SimplifiedUniversal, Unexpanded, State, ExtendedBranch, NewBranch, 193 ExtendedEventualities, NewEventualities, ODT_RL, ODT) 194 ). 195 196%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 197 198% 4th argument not used. 199search_state_aux(_, _, _, _, State, 200 [pr(State,FmlList)|Branch], [EqualStates,pr(State,FmlList)|Branch], 201 ExtendedEventualities, ExtendedEventualities, IDT, IDT) :- 202 pdl_write_ln('In search_state_aux (1)....'), 203 pdl_write(' State : '), pdl_write(State), pdl_nl, 204 pdl_write(' FmlList : '), pdl_write(FmlList), pdl_nl, 205 pdl_write(' Branch : '), pdl_write(Branch), pdl_nl, 206 is_copy(FmlList, State, Branch, EqualStates), !. 207 208search_state_aux(Axioms, SimplifiedExistential, SimplifiedUniversal, 209 _, State, ExtendedBranch, NewBranch, 210 ExtendedEventualities, NewEventualities, IDT, ODT) :- 211% pdl_write_ln('In search_state_aux (2)....'), 212 reduce_existentials(Axioms, SimplifiedExistential, State, 213 SimplifiedUniversal, ExtendedBranch, NewBranch, 214 ExtendedEventualities, NewEventualities, IDT, ODT). 215 216%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 217% 218% extend_branch(+State, +FmlList, +Branch, -ExtendedBranch) 219 220extend_branch(State, FmlList, Branch, [pr(State, FmlList)|Branch]). 221 222%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 223% 224% The key proof_steps_counter counts the proof steps 225 226set_proof_steps_counter(Number) :- !, 227 pdl_write('set_proof_steps_counter to '), pdl_write(Number), pdl_nl, 228 flag(proof_steps_counter, _, Number). 229 230increment_proof_steps_counter(Increment) :- !, 231 flag(proof_steps_counter, Old, Old + Increment). 232 233get_proof_steps_counter(Number) :- !, 234 flag(proof_steps_counter, Number, Number). 235 236%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 237% 238% The key states_counter counts the states created 239 240set_states_counter(Number) :- !, 241 pdl_write('set_states_counter to '), pdl_write(Number), pdl_nl, 242 flag(states_counter, _, Number). 243 244increment_states_counter(Increment) :- !, 245 flag(states_counter, Old, Old + Increment). 246 247get_states_counter(Number) :- !, 248 flag(states_counter, Number, Number). 249 250%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 251% 252% The key branch_point_counter counts the branch_points 253 254set_branch_point_counter(Number) :- !, 255 pdl_write('set_branch_point_counter to '), pdl_write(Number), pdl_nl, 256 flag(branch_point_counter, _, Number). 257 258increment_branch_point_counter(Increment) :- !, 259 flag(branch_point_counter, Old, Old + Increment). 260 261get_branch_point_counter(Number) :- !, 262 flag(branch_point_counter, Number, Number). 263 264%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 265% 266% The key sat_reuse_counter counts the number of times a stored 267% satisfiable set is re-used 268 269set_sat_reuse_counter(Number) :- !, 270 pdl_write('set_sat_reuse_counter to '), pdl_write(Number), pdl_nl, 271 flag(sat_reuse_counter, _, Number). 272 273increment_sat_reuse_counter(Increment) :- !, 274 flag(sat_reuse_counter, Old, Old + Increment). 275 276get_sat_reuse_counter(Number) :- !, 277 flag(sat_reuse_counter, Number, Number). 278 279%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 280% 281% The key unsat_reuse_counter counts the number of times a stored 282% unsatisfiable set is re-used 283 284set_unsat_reuse_counter(Number) :- !, 285 pdl_write('set_unsat_reuse_counter to '), pdl_write(Number), pdl_nl, 286 flag(unsat_reuse_counter, _, Number). 287 288increment_unsat_reuse_counter(Increment) :- !, 289 flag(unsat_reuse_counter, Old, Old + Increment). 290 291get_unsat_reuse_counter(Number) :- !, 292 flag(unsat_reuse_counter, Number, Number). 293 294 295%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 296% 297% The key satisfiable is used to track satisfiability on the current 298% branch. 299% -1 means undefined, 0 means unsatisfiable, 1 means satisfiable 300 301set_satisfiable_flag(Value) :- 302 flag(satisfiable, _, Value). 303 304get_satisfiability_status(Value) :- 305 flag(satisfiable, Value, Value). 306 307is_satisfiable(_) :- 308 get_satisfiability_status(1). 309 310is_unsatisfiable(_) :- 311 get_satisfiability_status(0). 312 313%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 314% 315% test_ignorability(+Branch,+FulfilledEventualities) 316% According to Definition 7 in (De Giacomo and Massacci, 2001), 317% a \pi-completed branch B is ignorable iff there is an eventuality X which 318% is not fulfilled. A branch is \pi-completed if (i) all prefixes are 319% reduced, i.e. all rules except <A>-rules have been applied, and 320% (ii) for every s1 which is not fully reduced there is a pair (s0,S0) 321% shorter than (s1,B) s.t. s0 is fully reduced in the segment S0 and s1 is 322% a copy of s0 in B. 323% The procedure only uses +Branch to determine all the eventualities 324% present on the branch. Whether these are fulfilled is then checked against 325% +FulfilledEventualities, a list of all eventualities currently fulfilled 326% on the branch. 327% Note that since distinct X_i and X_j can represent the 328% same eventuality, this check requires more than just comparing, say, the 329% number of syntactically distinct X_i present on the branch with the number 330% of syntactically distinct X_i in +FulfilledEventualities. 331% Note also, that we obtain +FulfilledEventualities from reduce_local. 332% +FulfilledEventualities will only be correct, as long complement splitting 333% is used to deal with X_i = <A*>F and as long rules are applied even if one 334% of the consequents is present (i.e. the formula F should not subsume <A*>F). 335 336test_ignorability(Branch, FulfilledEventualities) :- 337 eventualities(Branch, Eventualities), 338 collectCopies(Branch,Copies), 339 pdl_write_ln('In test_ignorability... '), 340 pdl_write(' Branch : '), pdl_write(Branch), pdl_nl, 341 pdl_write(' FulfilledEventualities : '), pdl_write(FulfilledEventualities), pdl_nl, 342 pdl_write(' Eventualities : '), pdl_write(Eventualities), pdl_nl, 343 test_ignorability_loop(Eventualities, FulfilledEventualities, Copies, Branch, _NewEventualities, _NewFulfilledEventualities). 344 345 346test_ignorability_loop(Eventualities, FulfilledEventualities, Copies, Branch, NewEventualities, NewFulfilledEventualities) :- 347 test_ignorability_aux(Eventualities, FulfilledEventualities, Copies, 348 NewEventualities1, NewFulfilledEventualities1), 349 (NewEventualities1 == [] -> 350 NewEventualities = NewEventualities1, 351 NewFulfilledEventualities = NewFulfilledEventualities1 352 ; 353 (NewFulfilledEventualities1 == FulfilledEventualities -> 354 print_unfulfilled_eventualities(NewEventualities1), 355 compute_inconsistent_sets(Eventualities,Branch,Copies), 356 !, 357 fail 358 ; 359 test_ignorability_loop(NewEventualities1, NewFulfilledEventualities1, Copies, Branch, NewEventualities, NewFulfilledEventualities) 360 ) 361 ). 362 363 364%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 365% 366% print_unfulfilled_eventualities(+Eventualities) 367% 368% print a list of eventualities that are not fulfilled on the current branch 369 370print_unfulfilled_eventualities([]) :- 371 !. 372print_unfulfilled_eventualities([ev(State,x(Y,Fml))|Eventualities]) :- 373 pdl_write('** Ignorable ** - '), pdl_write(ev(State,x(Y,Fml))), pdl_write(' unfulfilled'), pdl_nl, 374 print_proof_step('post', '** Ignorable **', ['unfulfilled',ev(State,x(Y,Fml))]), 375% print_proof_step('post', '** Ignorable/Unsatisfiable **', ['unfulfilled',x(Y,Fml)]), 376 !, 377 print_unfulfilled_eventualities(Eventualities). 378 379%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 380% 381% compute_inconsistent_sets(+Eventualities, +Branch, +Copies) 382% 383 384compute_inconsistent_sets([], _, _) :- 385 !. 386 387compute_inconsistent_sets([ev(State,x(_Y,_Fml))|Eventualities], Branch, Copies) :- 388 get_formulae_for_state(State,Branch,FmlList), 389 memberchk(isCopyOf(State,_),Copies), 390 store_inconsistent(FmlList), 391 !, 392 compute_inconsistent_sets(Eventualities, Branch, Copies). 393 394get_formulae_for_state(State1,[isCopyOf(_,_)|Branch],FmlList) :- 395 get_formulae_for_state(State1,Branch,FmlList), 396 !. 397get_formulae_for_state(State1,[pr(State1,FmlList)|_Branch],FmlList) :- 398 !. 399get_formulae_for_state(State1,[pr(State2,_FmlList)|Branch],FmlList) :- 400 State1 \= State2, 401 get_formulae_for_state(State1,Branch,FmlList), 402 !. 403 404%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 405% 406% test_ignorability_aux(+Eventualities, +FulfilledEventualities, +Copies, 407% -NewEventualities, -NewFulfilledEventualities) 408% computes -NewEventualities and -NewFulfilledEventualities from 409% +Eventualities and +FulfilledEventualities as follows: 410% -NewFulfilledEventualities contains all eventualities in +FulfilledEventualities 411% plus any eventuality in +Eventualities that can be shown to be fulfilled with 412% respect to +FulfilledEventualities and +Copies; 413% -NewEventualities contains all eventualities in +Eventualities that cannot be 414% shown to be fulfilled with respect to +FulfilledEventualties and +Copies. 415 416test_ignorability_aux([], FulfilledEventualities, _Copies, [], FulfilledEventualities). 417 418test_ignorability_aux([ev(State,Eventuality)|Eventualities], FulfilledEventualities, Copies, NewEventualities, NewFulfilledEventualities) :- 419 (test_ignorability_aux_fml(ev(State,Eventuality), FulfilledEventualities, Copies) -> 420 append(FulfilledEventualities,[fulfilled(State,Eventuality)],NewFulfilledEventualities1), 421 test_ignorability_aux(Eventualities, NewFulfilledEventualities1, Copies, NewEventualities, NewFulfilledEventualities) 422 ; 423 test_ignorability_aux(Eventualities, FulfilledEventualities, Copies, NewEventualities1, NewFulfilledEventualities), 424 NewEventualities = [ev(State,Eventuality)|NewEventualities1] 425 ). 426 427%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 428% 429% test_ignorability_aux_fml(+Eventuality, +FulfilledEventualities, +Copies) 430% 431% succeeds if +Eventuality is a fulfilled eventuality. This in turn is the case 432% if (a) among +FulfilledEventualities is a syntactically identical eventuality 433% which is already recorded as being fulfilled on the current branch, or 434% (b) among +FulfilledEventualities is an eventuality Eventuality2, recorded to 435% be fulfilled at a state State2 such that the state State1 at which +Eventuality 436% occurs collapsed to State2. 437 438test_ignorability_aux_fml(_, [], _) :- 439 fail. 440 441test_ignorability_aux_fml(ev(State1,x(Y,Fml)), [fulfilled(State2, x(X,Fml))|_], Copies) :- 442 (X = Y -> 443 print_proof_step('post', fulfilled_by(ev(State1,x(Y,Fml)), ev(State2,x(X,Fml))), '[fulfilled]') 444 ; 445 collapses(State1,State2,Copies), 446 print_proof_step('post', fulfilled_by(ev(State1,x(Y,Fml)), ev(State2,x(X,Fml))), '[fulfilled]') 447 ). 448 449test_ignorability_aux_fml(Event, [_|FulfilledEventualities], Copies) :- 450 test_ignorability_aux_fml(Event, FulfilledEventualities, Copies). 451 452 453%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 454% 455% collectCopies(+Branch, -Copies) 456% 457% whenever a state State1 is identified as a copy of a State2, we record that 458% fact by adding `isCopyOf(State1,State2)' on a branch. The predice collectCopies 459% retrieves all such facts from +Branch and returns it as a list -Copies. 460 461collectCopies([isCopyOf(State1,State2)|Branch],[isCopyOf(State1,State2)|Copies]) :- 462 !, 463 collectCopies(Branch,Copies). 464collectCopies([_|Branch],Copies) :- 465 collectCopies(Branch,Copies), 466 !. 467collectCopies([],[]). 468 469%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 470% 471% collapses(+State1, +State2, +Copies) 472% 473% succeeds if +State1 is a copy of +State2 with respect to the information on 474% which states are copies of each other contained in +Copies. 475 476collapses(X, Y, Copies) :- 477 memberchk(isCopyOf(X,Y),Copies). 478 479 480%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 481% 482% test_unsatisfiability(+State, +FmlList, +CompleteFmlList) 483% 484% test for inconsistency of the list of formulae FmlList; 485% - The first rule states that the empty set/list of formulae is not 486% inconsistent 487% - The second rule covers conditions 1 and 2 of Definition 23 in % 488% (De Giacomo and Massacci, 2000) via a inf_closure 489% - The third rule covers condition 3 of Definition 23 in 490% (De Giacomo and Massacci, 2000) 491 492test_unsatisfiability(_, [], _) :- !. 493% The following rule uses condition 3 of Definition 23 in 494% (De Giacomo and Massacci, 2000): 495% A superset of a \bot-set is a \bot-set. 496test_unsatisfiability(State, Fml, _) :- 497 list_to_ord_set(Fml,OrdFml1), 498 inconsistent(OrdFml2), 499 ord_subset(OrdFml2,OrdFml1), 500 pdl_write('Reused unsatisfiable set '), pdl_write(OrdFml2), pdl_nl, 501 print_proof_step(State, inconsistent_subset_of(OrdFml2,OrdFml1), '[inconsistent subset]'), 502 increment_unsat_reuse_counter(1), 503 !, 504 fail. 505test_unsatisfiability(State, Set, CompleteFmlList) :- 506 select_fml(Given, Set, SetWithoutGiven), 507 inf_closure(State, Given, SetWithoutGiven, CompleteFmlList), 508 test_unsatisfiability(State, SetWithoutGiven, CompleteFmlList). 509 510%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 511 512select_fml(Fml, [Fml|FmlList], FmlList). 513 514%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 515% 516% is_copy(+FmlList, +CurrentState, +Branch). 517% 518% test if pr(CurrentState, FmlList) is a copy of an earlier state in 519% Branch. 520 521is_copy(_,_,[],_) :- 522 fail. 523is_copy(FmlList, State, [isCopyOf(_,_)|Branch], EqualStates) :- 524 !, 525 is_copy(FmlList, State, Branch, EqualStates). 526is_copy(FmlList, State, [pr(X,FmlListInX)|_],isCopyOf(State,X)) :- 527 is_prefix(X, State), 528 % Ignore the first argument in the introduce literals x(_,Fml) 529 simplify_X(FmlList, SimplifiedFmlList), 530 simplify_X(FmlListInX, SimplifiedFmlListInX), 531% pdl_write_ln('In is_copy... '), 532% pdl_write(' SimplifiedFmlList : '), pdl_write(SimplifiedFmlList), pdl_nl, 533% pdl_write(' SimplifiedFmlListInX : '), pdl_write(SimplifiedFmlListInX), pdl_nl, 534 equal_set(SimplifiedFmlList, State, SimplifiedFmlListInX, X), !. 535is_copy(FmlList, State, [pr(_,_)|Branch], EqualStates) :- 536 is_copy(FmlList, State, Branch, EqualStates). 537 538%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 539 540is_prefix(X, X). 541is_prefix(X, ((Y), _)) :- 542 is_prefix(X,Y). 543 544prefix_to_list(0,[0]) :- !. 545prefix_to_list(((X), L, N),List) :- 546 prefix_to_list(X,List1), 547 append(List1,[L,N],List), 548 !. 549 550list_to_prefix([0],(0)) :- !. 551list_to_prefix([A,B|List],(Prefix1,L,N)) :- 552 append(PrefixList,[L,N],[A,B|List]), 553 list_to_prefix(PrefixList,Prefix1), 554 !. 555 556%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 557 558equal_set([], State, [], X) :- !, 559 % X is a copy of State 560 print_copies(State, X). 561 562equal_set([Elem|Set1], State, Set2, X) :- 563 delete(Set2, Elem, Set3), 564 equal_set(Set1, State, Set3, X). 565 566%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 567 568eliminate_duplicates(List, SimplifiedList) :- !, 569 sort(List, SimplifiedList). 570 571%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 572% 573% complement(+Fml,-NotFml) 574% 575% Returns the complement of Fml. 576 577complement(not(A),A) :- !. 578 579complement(A,not(A)) :- !. 580 581%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 582% 583% reduce_existentials(+Axioms, +Existential, +State, 584% +Universal, +Branch, -NewBranch, 585% +Eventualities, -NewEventualities) 586% 587% - Applies existential, universal and theory rules 588% 589 590reduce_existentials(_, [], _, _, Branch, Branch, 591 Eventualities, Eventualities, IDT, IDT). 592 593reduce_existentials(Axioms, Existential, X, Universal, Branch, NewBranch, 594 Eventualities, NewEventualities, IDT, ODT) :- !, 595% pdl_write('In reduce_existentials, X : '), pdl_write(X), pdl_nl, 596% pdl_write(' Existential : '), pdl_write(Existential), pdl_nl, 597 select(Fml, Existential, ExistentialWithoutFml), 598 Fml = dia(R,A), 599 pdl_write('* R = '), pdl_write(R), 600% atom(R), 601 pdl_write_ln('* '), 602 increment_states_counter(1), 603 get_states_counter(N), 604 Y = (X,R,N), 605 print_proof_step(Y, A, ['dia',Fml]), 606% pdl_write('In reduce_existentials, Y : '), pdl_write(Y), pdl_nl, 607 608 reduce_universal(Universal, Y, [], Unexpanded), 609 610 extend_unexpanded([A], [], Unexpanded, NewUnexpanded), 611 reduce_existential(Axioms, NewUnexpanded, Y, Branch, NewBranch1, 612 Eventualities, NewEventualities1, IDT, ODT_RE), 613 reduce_existentials(Axioms, ExistentialWithoutFml, X, Universal, 614 NewBranch1, NewBranch, NewEventualities1, NewEventualities, ODT_RE, ODT). 615 616 617reduce_existential(Axioms, NewUnexpanded, Y, Branch, NewBranch, 618 Eventualities, NewEventualities, IDT, ODT) :- 619 search_state(Axioms, NewUnexpanded, Y, Branch, NewBranch, 620 Eventualities, NewEventualities, IDT, ODT). 621 622 623%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 624 625reduce_universal([], _, Unexpanded, Unexpanded). 626 627reduce_universal([not(dia(R,A))|Universal], Y, Unexpanded, NewUnexpanded) :- 628 % check if Y is an R-successor 629 Y = (_,R,_), !, 630 complement(A, NotA), 631 extend_unexpanded([NotA], [], Unexpanded, NewUnexpanded1, 632 Y, ['box',not(dia(R,A))]), 633 reduce_universal(Universal, Y, NewUnexpanded1, NewUnexpanded). 634 635reduce_universal([_|Universal], Y, Unexpanded, NewUnexpanded) :- 636 reduce_universal(Universal, Y, Unexpanded, NewUnexpanded). 637 638%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 639% 640% extend_unexpanded(+FmlList, +Workedoff, +Unexpanded, -NewUnexpanded, 641% +X, +Justification) 642% - Adds all non-redundant formulae in FmlList to Unexpanded; 643% redundancy is evaluated against Workedoff 644% - Keeping all expanded formulae in Workedoff has the disadvantage that 645% the performance decreases and proofs are longer. 646% 647% TO DO: Consider ways of reducing this bookkeeping while preserving 648% soundness and completeness. 649% 650 651extend_unexpanded([], _, Unexpanded, Unexpanded, _, _). 652 653extend_unexpanded([Fml|Rest], Workedoff, Unexpanded, NewUnexpanded, X, Justification) :- 654 extend_unexpanded_aux(Fml, Workedoff, Unexpanded, Unexpanded1, 655 X, Justification), !, 656 extend_unexpanded(Rest, Workedoff, Unexpanded1, NewUnexpanded, X, Justification). 657 658extend_unexpanded_aux(true, _, Unexpanded, Unexpanded, 659 X, Justification) :- 660 print_proof_step(X, '-', Justification). 661 662extend_unexpanded_aux(Fml, Workedoff, Unexpanded, [Fml|Unexpanded], 663 X, Justification) :- 664 not_redundant(Fml, Workedoff, Unexpanded), 665 print_proof_step(X, Fml, Justification). 666 667extend_unexpanded_aux(Fml, _, Unexpanded, Unexpanded, X, Justification) :- 668 print_redundant_step(X, Fml, Justification). 669 670%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 671% 672% extend_unexpanded(+FmlList, +Workedoff, +Unexpanded, -NewUnexpanded) 673% 674% Same as above, but derivation step is not documented 675% 676 677extend_unexpanded([], _, Unexpanded, Unexpanded). 678 679extend_unexpanded([Fml|Rest], Workedoff, Unexpanded, NewUnexpanded) :- 680 extend_unexpanded_aux(Fml, Workedoff, Unexpanded, Unexpanded1), !, 681 extend_unexpanded(Rest, Workedoff, Unexpanded1, NewUnexpanded). 682 683extend_unexpanded_aux(Fml, Workedoff, Unexpanded, [Fml|Unexpanded]) :- 684 not_in_set(Fml, Workedoff), 685 not_in_set(Fml, Unexpanded). 686 687extend_unexpanded_aux(_, _, Unexpanded, Unexpanded) :- 688 true. 689 690%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 691% not_in_set(+Fml, +FmlList) 692% 693 694not_redundant(Fml, FmlList1, FmlList2) :- 695 not_in_set(Fml, FmlList1), 696 not_in_set(Fml, FmlList2). 697 698%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 699% not_in_set(+Fml, +FmlList) 700% 701 702not_in_set(Fml, FmlList) :- 703 \+ member(Fml, FmlList). 704 705%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 706% known_consistent(Fmls) 707% If Fmls is a subset of a set of formulae which is already known to be 708% consistent, then Fmls is also consistent 709% 710 711known_consistent(Fmls,BranchForFmls,EventualitiesForFmls) :- 712 list_to_ord_set(Fmls,OrdFmls1), 713 consistent(OrdFmls2,BranchForFmls,EventualitiesForFmls), 714 ord_subset(OrdFmls1,OrdFmls2), 715% write('Reused satisfiable set '), print(OrdFmls2), nl, 716% write('Reused a satisfiable set '), nl, 717 print_proof_step(g, consistent_superset_of(OrdFmls2,OrdFmls1), '[consistent superset]'), 718 increment_sat_reuse_counter(1), 719 !. 720 721%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 722% print_copies(+State, +CopyState) 723% 724 725print_copies(State, CopyState) :- 726 print_proof_step(State, copy_of(State, CopyState), '[loop checking]'). 727 728%%print_copies(State, CopyState) :- 729%% sprintf_state(StateString, State), 730%% string_to_atom(StateString, State1), 731%% sprintf_state(CopyStateString, CopyState), 732%% swritef(String, 'copy of %w', [CopyStateString]), 733%% string_to_atom(String, StringAtom), 734%% print_proof_step(State1, StringAtom, 'loop checking'). 735 736%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 737 738print_result(Result) :- 739 write('** '), write(Result), write_ln(' **'), 740 get_search_output_filename(Filename), 741 append(Filename), 742 (get_output_format(latex) -> 743 write('& \\text{** '), write(Result), write_ln(' **}') 744 ; 745 write('** '), write(Result), write_ln(' **') 746 ), 747 told. 748 749%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 750 751print_proof_step(_, [], _) :- !. 752 753print_proof_step(State, [Fml|FmlList], Justification) :- !, 754 print_proof_step(State, Fml, Justification), 755 print_proof_step(State, FmlList, Justification). 756 757print_proof_step(State, Conclusion, Justification) :- 758 increment_proof_steps_counter(1), 759 get_proof_steps_counter(N), 760% print_proof_step_aux(N, State, Conclusion, Justification), 761 get_search_output_filename(Filename), 762 append(Filename), 763 (get_output_format(latex) -> 764 print_proof_step_latex(N, State, Conclusion, Justification) 765 ; 766 print_proof_step_aux(N, State, Conclusion, Justification) 767 ), 768 told. 769 770print_proof_step_aux(N, State, Conclusion, Justification) :- 771 pdl_writef('%4r. ', [N]), 772 get_branch_point_counter(Count), 773 pdl_tab(Count * 4), 774 print_state(State), pdl_write(' : '), 775 print_conclusion(Conclusion), pdl_nl, 776 pdl_write(' '), 777% pdl_write(' '), 778 pdl_write(Justification), pdl_nl. 779 780 781print_proof_step_latex(N, State, Conclusion, Justification) :- 782 pdl_write(N), pdl_write('.\\ & '), 783 get_branch_point_counter(Count), 784 print_quad(Count), 785 print_state_latex(State), pdl_write(' {:} '), 786 print_conclusion_latex(Conclusion), pdl_nl, 787 pdl_write('\\tag*{$'), 788 print_justification_latex(Justification), !, 789 pdl_write('$}'), pdl_nl, 790 pdl_write('\\\\'), pdl_nl. 791 792print_quad(0). 793 794print_quad(Count) :- 795 pdl_write('\\quad\\qquad '), 796 CountDecr is Count - 1, 797 print_quad(CountDecr). 798 799 800%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 801 802print_redundant_step(_, [], _) :- !. 803 804print_redundant_step(State, [Fml|FmlList], Justification) :- !, 805 print_redundant_step(State, Fml, Justification), 806 print_redundant_step(State, FmlList, Justification). 807 808print_redundant_step(State, Conclusion, Justification) :- 809 print_proof_step_aux('-', State, Conclusion, Justification), 810 get_search_output_filename(Filename), 811 append(Filename), 812 (get_output_format(latex) -> 813 print_proof_step_latex('-', State, Conclusion, Justification) 814 ; 815 print_proof_step_aux('-', State, Conclusion, Justification) 816 ), 817 told. 818 819%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 820 821print_justification_latex(String) :- 822 atom(String), !, 823 rule_name_latex(String, LatexString), 824 pdl_write(LatexString). 825 826print_justification_latex([String|FmlList]) :- 827 atom(String), !, 828 rule_name_latex(String, LatexString), 829 pdl_write(LatexString), pdl_write('{}: '), 830 print_formula_list_latex(FmlList). 831 832print_justification_latex(Justification) :- !, 833 pdl_write(Justification). 834 835%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 836 837rule_name_latex(true, '\\mltop'). 838rule_name_latex('or-LEFT', '\\text{${\\mlor}$-left}'). 839rule_name_latex('or-RIGHT', '\\text{${\\mlor}$-right}'). 840rule_name_latex('or-RIGHT1', '\\text{${\\mlor}$-right1}'). 841rule_name_latex('or-RIGHT2', '\\text{${\\mlor}$-right2}'). 842rule_name_latex('and', '\\neg{\\mlor}'). 843%rule_name_latex('and', '{\\mland}'). 844rule_name_latex('dia-or-LEFT', '\\text{$\\mldia{\\mlor}{}$-left}'). 845rule_name_latex('dia-or-RIGHT', '\\text{$\\mldia{\\mlor}{}$-right}'). 846rule_name_latex('dia-or-RIGHT1', '\\text{$\\mldia{\\mlor}{}$-right1}'). 847rule_name_latex('dia-or-RIGHT2', '\\text{$\\mldia{\\mlor}{}$-right2}'). 848rule_name_latex('dia-comp', '\\mldia{\\comp{}{}}{}'). 849rule_name_latex('dia-star', '\\mldia{\\ast}{}'). 850rule_name_latex('dia-test', '\\mldia{?}{}'). 851rule_name_latex('dia', '\\mldia{\\cdot}{}'). 852rule_name_latex('X-LEFT', '\\text{$X$-left}'). 853rule_name_latex('X-RIGHT', '\\text{$X$-right}'). 854rule_name_latex('X-RIGHT1', '\\text{$X$-right1}'). 855rule_name_latex('X-RIGHT2', '\\text{$X$-right2}'). 856rule_name_latex('box-or', '\\neg\\mldia{\\mlor}{}'). 857rule_name_latex('box-comp', '\\neg\\mldia{\\comp{}{}}{}'). 858rule_name_latex('box-star', '\\neg\\mldia{\\ast}{}'). 859rule_name_latex('box-test-LEFT', '\\text{$\\neg\\mldia{?}{}$-left}'). 860rule_name_latex('box-test-RIGHT', '\\text{$\\neg\\mldia{?}{}$-right}'). 861rule_name_latex('box-test-RIGHT1', '\\text{$\\neg\\mldia{?}{}$-right1}'). 862rule_name_latex('box-test-RIGHT2', '\\text{$\\neg\\mldia{?}{}$-right2}'). 863rule_name_latex('box', '\\neg\\mldia{\\cdot}{}'). 864%rule_name_latex('box-or', '\\mlbox{\\mlor}{}'). 865%rule_name_latex('box-comp', '\\mlbox{\\comp}{}'). 866%rule_name_latex('box-star', '\\mlbox{\\ast}{}'). 867%rule_name_latex('box', '\\mlbox{\\cdot}{}'). 868rule_name_latex('[theory]', '\\text{theory}'). 869rule_name_latex('[theory-inst]', '\\text{theory-inst}'). 870rule_name_latex('[given]', '\\text{given}'). 871rule_name_latex('[fulfilled]', '\\text{fulfilled}'). 872rule_name_latex('[loop checking]', '\\text{loop checking}'). 873rule_name_latex(String, LatexString) :- 874 swritef(LatexString, '\\\\text{%w}', [String]). 875 876%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 877 878justification_latex('[given]', 'given'). 879justification_latex('[fulfilled]', 'fulfilled'). 880justification_latex('[loop checking]', 'loop checking'). 881 882%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 883 884print_formula_list_latex([]). 885 886print_formula_list_latex([Fml]) :- 887 print_formula_latex(Fml). 888 889print_formula_list_latex([Fml|List]) :- 890 print_formula_latex(Fml), 891 pdl_write(', '), 892 print_formula_list_latex(List). 893 894%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 895 896print_formula_latex(true) :- !, 897 pdl_write('\\mltop'). 898 899print_formula_latex(false) :- !, 900 pdl_write('\\mlbot'). 901 902print_formula_latex(x(Y,Fml)) :- !, 903 pdl_write('X^{'), print_state(Y), pdl_write('}_{'), 904 print_formula_latex(Fml), pdl_write('}'). 905 906print_formula_latex(ev(State,x(Y,Fml))) :- !, 907 print_state(State), pdl_write(' {:} '), 908 pdl_write('X^{'), print_state(Y), pdl_write('}_{'), 909 print_formula_latex(Fml), pdl_write('}'). 910print_formula_latex(at(State,Fml)) :- !, 911 print_state(State), pdl_write(' {:} '), 912 print_formula_latex(Fml). 913 914print_formula_latex(and(A,B)) :- !, 915 pdl_write('('), 916 print_formula_latex(A), 917 pdl_write(' \\mland '), 918 print_formula_latex(B), 919 pdl_write(')'). 920 921print_formula_latex(or(A,B)) :- !, 922 pdl_write('('), 923 print_formula_latex(A), 924 pdl_write(' \\mlor '), 925 print_formula_latex(B), 926 pdl_write(')'). 927 928print_formula_latex(not(A)) :- !, 929 pdl_write('\\neg '), 930 print_formula_latex(A). 931 932print_formula_latex(test(A)) :- !, 933 pdl_write('\\test{'), 934 print_formula_latex(A), 935 pdl_write('}'). 936 937print_formula_latex(comp(A,B)) :- !, 938 pdl_write('(\\comp{'), 939 print_formula_latex(A), 940 pdl_write('}{'), 941 print_formula_latex(B), 942 pdl_write('})'). 943 944print_formula_latex(star(A)) :- !, 945 print_formula_latex(A), 946 pdl_write('{}^*'). 947 948print_formula_latex(dia(R,A)) :- !, 949 pdl_write('\\mldia{'), 950 print_formula_latex(R), 951 pdl_write('}{'), 952 print_formula_latex(A), 953 pdl_write('}'). 954 955print_formula_latex(box(R,A)) :- !, 956 pdl_write('\\mlbox{'), 957 print_formula_latex(R), 958 pdl_write('}{'), 959 print_formula_latex(A), 960 pdl_write('}'). 961 962print_formula_latex(A) :- !, 963 pdl_write('\\textit{'), pdl_write(A), pdl_write('}'). 964 965%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 966 967latex_output(begin) :- !, 968 get_search_output_filename(Filename), 969 append(Filename), 970 pdl_write_ln('\\begin{align*}'), 971 told. 972 973latex_output(end) :- !, 974 get_search_output_filename(Filename), 975 append(Filename), 976 pdl_write_ln('\\end{align*}'), 977 told. 978 979%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 980 981sprintf_state(String, (X,Y)) :- !, 982 sprintf_state(XString, X), 983 sprintf_state(YString, Y), 984 swritef(String, '%w.%w', [XString, YString]). 985 986sprintf_state(XString,X) :- 987 string_to_atom(XString, X). 988 989%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 990 991print_state((X,Y)) :- !, 992 print_state(X), pdl_write('.'), print_state(Y). 993 994print_state(X) :- 995 pdl_write(X). 996 997%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 998 999print_state_latex((X,Y)) :- !, 1000 print_state_latex(X), pdl_write('.'), print_state_latex(Y). 1001 1002print_state_latex(X) :- 1003 number(X), !, 1004 pdl_write(X). 1005 1006print_state_latex(X) :- !, 1007 pdl_write('\\textit{'), pdl_write(X), pdl_write('}'). 1008 1009%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1010 1011print_conclusion(fulfilled_by(Fml1,Fml2)) :- !, 1012 pdl_write('\\ '), pdl_write(Fml1), pdl_write(' fulfilled by '), pdl_write(Fml2). 1013 1014print_conclusion(copy_of(X,Y)) :- !, 1015 print_state(X), pdl_write(' copy of '), print_state(Y). 1016 1017print_conclusion(inconsistent_subset_of(X,Y)) :- !, 1018 print_state(X), pdl_write(' is an inconsistent subset of '), print_state(Y). 1019 1020print_conclusion(consistent_superset_of(X,Y)) :- !, 1021 print_state(X), pdl_write(' is a consistent superset of '), print_state(Y). 1022 1023print_conclusion(inconsistent_set(X)) :- !, 1024 print_state(X), pdl_write(' is an inconsistent set'). 1025 1026print_conclusion(consistent_set(X)) :- !, 1027 print_state(X), pdl_write(' is an consistent set'). 1028 1029print_conclusion(X) :- 1030 pdl_write(X). 1031 1032%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1033 1034print_conclusion_latex(fulfilled_by(Fml1,Fml2)) :- !, 1035 pdl_write(' '), 1036 print_formula_latex(Fml1), 1037 pdl_write('\\textit{ fulfilled by }'), 1038 print_formula_latex(Fml2). 1039 1040print_conclusion_latex(copy_of(X,Y)) :- !, 1041 print_state_latex(X), 1042 pdl_write('\\textit{ copy of }'), 1043 print_state_latex(Y). 1044 1045print_conclusion_latex(consistent_set(X)) :- !, 1046 pdl_write('\\begin{array}[t]{l}'), pdl_nl, 1047 print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl, 1048 pdl_write('\\textit{ is a consistent set }'), pdl_nl, 1049 pdl_write('\\end{array}'). 1050 1051print_conclusion_latex(inconsistent_set(X)) :- !, 1052 pdl_write('\\begin{array}[t]{l}'), pdl_nl, 1053 print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl, 1054 pdl_write('\\textit{ is an inconsistent set }'), pdl_nl, 1055 pdl_write('\\end{array}'). 1056 1057print_conclusion_latex(consistent_superset_of(X,Y)) :- !, 1058 pdl_write('\\begin{array}[t]{l}'), pdl_nl, 1059 print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl, 1060 pdl_write('\\textit{ is a consistent superset of }\\\\ '), pdl_nl, 1061 print_formula_list_latex(Y), pdl_write('\\\\ '), pdl_nl, 1062 pdl_write(' \\end{array}'). 1063 1064print_conclusion_latex(inconsistent_subset_of(X,Y)) :- !, 1065 pdl_write('\\begin{array}[t]{l}'), pdl_nl, 1066 print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl, 1067 pdl_write('\\textit{ is an inconsistent subset of }\\\\ '), pdl_nl, 1068 print_formula_list_latex(Y), pdl_write('\\\\ '), pdl_nl, 1069 pdl_write(' \\end{array}'). 1070 1071print_conclusion_latex(X) :- 1072 print_formula_latex(X). 1073 1074%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1075 1076print_list([]). 1077 1078print_list([Head|List]) :- 1079 pdl_write(Head), 1080 pdl_write(' '), 1081 print_list(List)