|
PENG Processable ENGlish |
|
Prove it with OTTER
Dreadsbury Mansion Mystery in PENG
A text written in PENG can be checked for consistency and used for question answering. For this purpose, we are using the theorem prover OTTER (and a model builder in parallel). Our example text below is first translated into a discourse representation structure and then via first-order logic notation into OTTER syntax.- A person who lives in Dreadsbury Mansion kills Agatha.
- Agatha lives in Dreadsbury Mansion.
- The butler lives in Dreadsbury Mansion.
- Charles lives in Dreadsbury Mansion.
- If a person lives in Dreadsbury Mansion then the person is Agatha or is the butler or is Charles.
- If a person X kills a person Y then the person X hates the person Y.
- If a person X kills a person Y then the person X is not richer then the person Y.
- If Agatha hates a person then Charles does not hate that person.
- If a person is not the butler then Agatha hates the person.
- If a person is not richer than Agatha then the butler hates the person.
- If Agatha hates a person then the butler hates the person.
- No person hates every person.
- Agatha is not the butler.
Does Agatha kill Agatha?Since OTTER is a refutation based theorem prover, we have to feed it the negation of the question Does Agatha kill Agatha?. If we were interested in finding the answer to the question Who kills Agatha? we would have to add an answer literal of the form $ans(Variable) to the denial. The answer literal records instantiations of variables in input clauses during the search for a refutation. In our example below we would use the expression (-((exists K (event(K) & kill(K,G,agatha)))) & $ans(G) instead of (-((exists K (event(K) & kill(K,G,agatha)))).
If OTTER finds a poof, it will produce the empty clause $F. However, the result of the proof is displayed in the editor in controlled language and the user never has to worry about the details of the proof.
OTTER Output File
The original output produced by OTTER has been slightly edited for better readability.----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Thu Feb 20 23:01:12 2003 The command was "otter". set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). assign(max_seconds,30). set(prolog_style_variables). formula_list(usable). exists A B C D E F G H I J K L M N (-(exists O (event(O) & kill(O,J,J))) & -eq(J,F) & (all P (person(P) -> -(all Q (person(Q) -> (exists R (event(R) & hate(R,P,Q))))))) & (all S T (event(S) & hate(S,J,T) & person(T) -> (exists U (event(U) & hate(U,F,T))))) & (all V (-(exists W (state(W) & richer(W,V,J))) & person(V) -> (exists X (event(X) & hate(X,F,V))))) & (all Y (-eq(Y,F) & person(Y) -> (exists Z (event(Z) & hate(Z,J,Y))))) & (all A1 B1 (event(A1) & hate(A1,J,B1) & person(B1) -> -(exists C1 (event(C1) & hate(C1,C,B1))))) & (all D1 E1 F1 (event(D1) & kill(D1,F1,E1) & person(E1) & person(F1) -> -(exists G1 (state(G1) & richer(G1,F1,E1))))) & (all H1 I1 J1 (event(H1) & kill(H1,J1,I1) & person(I1) & person(J1) -> (exists K1 (event(K1) & hate(K1,J1,I1))))) & (all L1 M1 N1 (location(L1) & in(L1,M1,L) & event(M1) & live(M1,N1) & person(N1) -> eq(C,N1))) & (all O1 P1 Q1 (location(O1) & in(O1,P1,L) & event(P1) & live(P1,Q1) & person(Q1) -> eq(F,Q1))) & (all R1 S1 T1 (location(R1) & in(R1,S1,L) & event(S1) & live(S1,T1) & person(T1) -> eq(J,T1))) & location(A) & in(A,B,L) & event(B) & live(B,C) & eq(C,charles) & location(D) & in(D,E,L) & event(E) & live(E,F) & butler(F) & location(G) & in(G,H,L) & event(H) & live(H,J) & event(I) & kill(I,N,J) & eq(J,agatha) & location(K) & in(K,M,L) & eq(L,dreadsbury_mansion) & event(M) & live(M,N) & person(N)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -event(O)| -kill(O,$c5,$c5). 0 [] -eq($c5,$c9). 0 [] -person(P)|person($f1(P)). 0 [] -person(P)| -event(R)| -hate(R,P,$f1(P)). 0 [] -event(S)| -hate(S,$c5,T)| -person(T)|event($f2(S,T)). 0 [] -event(S)| -hate(S,$c5,T)| -person(T)|hate($f2(S,T),$c9,T). 0 [] state($f3(V))| -person(V)|event($f4(V)). 0 [] state($f3(V))| -person(V)|hate($f4(V),$c9,V). 0 [] richer($f3(V),V,$c5)| -person(V)|event($f4(V)). 0 [] richer($f3(V),V,$c5)| -person(V)|hate($f4(V),$c9,V). 0 [] eq(Y,$c9)| -person(Y)|event($f5(Y)). 0 [] eq(Y,$c9)| -person(Y)|hate($f5(Y),$c5,Y). 0 [] -event(A1)| -hate(A1,$c5,B1)| -person(B1)| -event(C1)| -hate(C1,$c12,B1). 0 [] -event(D1)| -kill(D1,F1,E1)| -person(E1)| -person(F1)| -state(G1)| -richer(G1,F1,E1). 0 [] -event(H1)| -kill(H1,J1,I1)| -person(I1)| -person(J1)|event($f6(H1,I1,J1)). 0 [] -event(H1)| -kill(H1,J1,I1)| -person(I1)| -person(J1)|hate($f6(H1,I1,J1),J1,I1). 0 [] -location(L1)| -in(L1,M1,$c3)| -event(M1)| -live(M1,N1)| -person(N1)|eq($c12,N1). 0 [] -location(O1)| -in(O1,P1,$c3)| -event(P1)| -live(P1,Q1)| -person(Q1)|eq($c9,Q1). 0 [] -location(R1)| -in(R1,S1,$c3)| -event(S1)| -live(S1,T1)| -person(T1)|eq($c5,T1). 0 [] location($c14). 0 [] in($c14,$c13,$c3). 0 [] event($c13). 0 [] live($c13,$c12). 0 [] eq($c12,charles). 0 [] location($c11). 0 [] in($c11,$c10,$c3). 0 [] event($c10). 0 [] live($c10,$c9). 0 [] butler($c9). 0 [] location($c8). 0 [] in($c8,$c7,$c3). 0 [] event($c7). 0 [] live($c7,$c5). 0 [] event($c6). 0 [] kill($c6,$c1,$c5). 0 [] eq($c5,agatha). 0 [] location($c4). 0 [] in($c4,$c2,$c3). 0 [] eq($c3,dreadsbury_mansion). 0 [] event($c2). 0 [] live($c2,$c1). 0 [] person($c1). end_of_list. SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deletion, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: set(unit_deletion). dependent: set(factor). ------------> process usable: ** KEPT (pick-wt=6): 1 [] -event(A)| -kill(A,$c5,$c5). ** KEPT (pick-wt=3): 3 [copy,2,flip.1] -eq($c9,$c5). ** KEPT (pick-wt=5): 4 [] -person(A)|person($f1(A)). ** KEPT (pick-wt=9): 5 [] -person(A)| -event(B)| -hate(B,A,$f1(A)). ** KEPT (pick-wt=12): 6 [] -event(A)| -hate(A,$c5,B)| -person(B)|event($f2(A,B)). ** KEPT (pick-wt=14): 7 [] -event(A)| -hate(A,$c5,B)| -person(B)|hate($f2(A,B),$c9,B). ** KEPT (pick-wt=8): 8 [] state($f3(A))| -person(A)|event($f4(A)). ** KEPT (pick-wt=10): 9 [] state($f3(A))| -person(A)|hate($f4(A),$c9,A). ** KEPT (pick-wt=10): 10 [] richer($f3(A),A,$c5)| -person(A)|event($f4(A)). ** KEPT (pick-wt=12): 11 [] richer($f3(A),A,$c5)| -person(A)|hate($f4(A),$c9,A). ** KEPT (pick-wt=8): 12 [] eq(A,$c9)| -person(A)|event($f5(A)). ** KEPT (pick-wt=10): 13 [] eq(A,$c9)| -person(A)|hate($f5(A),$c5,A). ** KEPT (pick-wt=14): 14 [] -event(A)| -hate(A,$c5,B)| -person(B)| -event(C)| -hate(C,$c12,B). ** KEPT (pick-wt=16): 15 [] -event(A)| -kill(A,B,C)| -person(C)| -person(B)| -state(D)| -richer(D,B,C). ** KEPT (pick-wt=15): 16 [] -event(A)| -kill(A,B,C)| -person(C)| -person(B)|event($f6(A,C,B)). ** KEPT (pick-wt=17): 17 [] -event(A)| -kill(A,B,C)| -person(C)| -person(B)|hate($f6(A,C,B),B,C). ** KEPT (pick-wt=16): 18 [] -location(A)| -in(A,B,$c3)| -event(B)| -live(B,C)| -person(C)|eq($c12,C). ** KEPT (pick-wt=16): 19 [] -location(A)| -in(A,B,$c3)| -event(B)| -live(B,C)| -person(C)|eq($c9,C). ** KEPT (pick-wt=16): 20 [] -location(A)| -in(A,B,$c3)| -event(B)| -live(B,C)| -person(C)|eq($c5,C). ------------> process sos: ** KEPT (pick-wt=2): 25 [] location($c14). ** KEPT (pick-wt=4): 26 [] in($c14,$c13,$c3). ** KEPT (pick-wt=2): 27 [] event($c13). ** KEPT (pick-wt=3): 28 [] live($c13,$c12). ** KEPT (pick-wt=3): 30 [copy,29,flip.1] eq(charles,$c12). ---> New Demodulator: 31 [new_demod,30] eq(charles,$c12). ** KEPT (pick-wt=2): 32 [] location($c11). ** KEPT (pick-wt=4): 33 [] in($c11,$c10,$c3). ** KEPT (pick-wt=2): 34 [] event($c10). ** KEPT (pick-wt=3): 35 [] live($c10,$c9). ** KEPT (pick-wt=2): 36 [] butler($c9). ** KEPT (pick-wt=2): 37 [] location($c8). ** KEPT (pick-wt=4): 38 [] in($c8,$c7,$c3). ** KEPT (pick-wt=2): 39 [] event($c7). ** KEPT (pick-wt=3): 40 [] live($c7,$c5). ** KEPT (pick-wt=2): 41 [] event($c6). ** KEPT (pick-wt=4): 42 [] kill($c6,$c1,$c5). ** KEPT (pick-wt=3): 44 [copy,43,flip.1] eq(agatha,$c5). ---> New Demodulator: 45 [new_demod,44] eq(agatha,$c5). ** KEPT (pick-wt=2): 46 [] location($c4). ** KEPT (pick-wt=4): 47 [] in($c4,$c2,$c3). ** KEPT (pick-wt=3): 49 [copy,48,flip.1] eq(dreadsbury_mansion,$c3). ---> New Demodulator: 50 [new_demod,49] eq(dreadsbury_mansion,$c3). ** KEPT (pick-wt=2): 51 [] event($c2). ** KEPT (pick-wt=3): 52 [] live($c2,$c1). ** KEPT (pick-wt=2): 53 [] person($c1). >>>> Starting back demodulation with 31. >>>> Starting back demodulation with 45. >>>> Starting back demodulation with 50. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=2) 25 [] location($c14). given clause #2: (wt=2) 27 [] event($c13). given clause #3: (wt=2) 32 [] location($c11). given clause #4: (wt=2) 34 [] event($c10). given clause #5: (wt=2) 36 [] butler($c9). given clause #6: (wt=4) 26 [] in($c14,$c13,$c3). given clause #7: (wt=2) 37 [] location($c8). given clause #8: (wt=2) 39 [] event($c7). given clause #9: (wt=2) 41 [] event($c6). given clause #10: (wt=2) 46 [] location($c4). given clause #11: (wt=3) 28 [] live($c13,$c12). given clause #12: (wt=2) 51 [] event($c2). given clause #13: (wt=2) 53 [] person($c1). given clause #14: (wt=3) 30 [copy,29,flip.1] eq(charles,$c12). given clause #15: (wt=3) 35 [] live($c10,$c9). given clause #16: (wt=4) 33 [] in($c11,$c10,$c3). given clause #17: (wt=3) 40 [] live($c7,$c5). given clause #18: (wt=3) 44 [copy,43,flip.1] eq(agatha,$c5). given clause #19: (wt=3) 49 [copy,48,flip.1] eq(dreadsbury_mansion,$c3). given clause #20: (wt=3) 52 [] live($c2,$c1). given clause #21: (wt=4) 38 [] in($c8,$c7,$c3). given clause #22: (wt=3) 90 [hyper,53,4] person($f1($c1)). given clause #23: (wt=3) 93 [para_into,30.1.1,30.1.1] eq($c12,$c12). given clause #24: (wt=3) 110 [para_into,44.1.1,44.1.1] eq($c5,$c5). given clause #25: (wt=3) 113 [para_into,49.1.1,49.1.1] eq($c3,$c3). given clause #26: (wt=4) 42 [] kill($c6,$c1,$c5). given clause #27: (wt=4) 47 [] in($c4,$c2,$c3). ----> UNIT CONFLICT at 0.02 sec ----> 194 [binary,193.1,162.1] $F. Length of proof is 7. Level of proof is 3. ---------------- PROOF ---------------- 2 [] -eq($c5,$c9). 3 [copy,2,flip.1] -eq($c9,$c5). 19 [] -location(A)| -in(A,B,$c3)| -event(B)| -live(B,C)| -person(C)|eq($c9,C). 20 [] -location(A)| -in(A,B,$c3)| -event(B)| -live(B,C)| -person(C)|eq($c5,C). 43 [] eq($c5,agatha). 44 [copy,43,flip.1] eq(agatha,$c5). 46 [] location($c4). 47 [] in($c4,$c2,$c3). 51 [] event($c2). 52 [] live($c2,$c1). 53 [] person($c1). 110 [para_into,44.1.1,44.1.1] eq($c5,$c5). 143,142 [hyper,47,20,46,51,52,53] eq($c5,$c1). 145,144 [hyper,47,19,46,51,52,53] eq($c9,$c1). 162 [back_demod,110,demod,143,143] eq($c1,$c1). 193 [back_demod,3,demod,145,143] -eq($c1,$c1). 194 [binary,193.1,162.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 27 clauses generated 104 clauses kept 182 clauses forward subsumed 22 clauses back subsumed 2 Kbytes malloced 191 ----------- times (seconds) ----------- user CPU time 0.22 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 0 finished Thu Feb 20 23:01:12 2003