#!/bin/sh # This is a shell archive, meaning: # 1. Remove everything above the #!/bin/sh line. # 2. Save the resulting text in a file. # 3. Execute the file with /bin/sh (not csh) to create the files: # README # morgan.five.desc # morgan.five.ver1.clauses # morgan.five.ver1.in # morgan.five.ver1.out # morgan.five.ver2.clauses # morgan.five.ver2.in # morgan.five.ver2.out # morgan.four.desc # morgan.four.ver1.clauses # morgan.four.ver1.in # morgan.four.ver1.out # morgan.one.desc # morgan.one.ver1.clauses # morgan.one.ver1.in # morgan.one.ver1.out # morgan.six.desc # morgan.six.ver1.clauses # morgan.six.ver1.in # morgan.six.ver1.out # morgan.three.desc # morgan.three.ver1.clauses # morgan.three.ver1.in # morgan.three.ver1.out # morgan.three.ver2.clauses # morgan.three.ver2.in # morgan.three.ver2.out # morgan.two.desc # morgan.two.ver1.clauses # morgan.two.ver1.in # morgan.two.ver1.out # This archive created: Tue Aug 16 11:19:43 1988 export PATH; PATH=/bin:$PATH if test -f 'README' then echo shar: over-writing existing file "'README'" fi cat << \SHAR_EOF > 'README' problem-set/logic.problems/morgan/README created : 07/15/86 revised : 07/15/88 Contents of 'morgan': -------------------- Main File Headings ------------------------------------------------------------------------ The following axioms apply to all problems in this directory: * 1. x => (y => x) * 2. [x => (y => z)] => [(x => y) => (x => z)] * 3. (-x => -y) => (y => x) * 4. -(x => y) | -x | y README : You are currently in this file. morgan_one : Can transitivity be deduced from the four axioms listed? morgan_two : Can (not(not(a)) implies a) be deduced from the four axioms and transitiviy? morgan_three : Can (a implies not(not(a))) be deduced from the four axioms and the statement proven by morgan_two (not(not(a)) implies a)? morgan_four : Can (a implies not(not(a))) be deduced from the four axioms and transitiviy? morgan_five.ver1 : Can (not(not(a)) implies a) be deduced from the four axioms given. morgan_five.ver2 : The same problem as morgan_five.ver1 except that the third axiom is changed from [(-x => -y) => (y => x)] to [(y => x) => (-x => -y)]. morgan_six : Can (a => b) => [(b => c) => (a => c)] be deduced from just axioms 1,2, and 4. ------------------------------------------------------------------------ For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#.in, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, credits for problem formulation, and complete details on each formulation and each version. probname.ver#.in : contains the problem specification, input clauses, and strategy for OTTER; this file is ready to run. probname.ver#.clauses : contains the description, commentary, and the actual clauses (including the denial of the conclusion) used for probname.ver#.in, without any strategy; note that comments always are on lines beginning with a %, preceding the clauses to which they refer, and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver#.in with OTTER, with proof if one is found, and with statistics on the clauses generated and CPU time used. HOW TO RUN : ---------------------------------------------------------------------- Invoke OTTER by using the following command : otter < probname.ver#.in [ > outfile ] [ & ] NOTE : '> outfile' may be used to send all output to a file named outfile; '&' may be used to run the program in the background. SHAR_EOF if test -f 'morgan.five.desc' then echo shar: over-writing existing file "'morgan.five.desc'" fi cat << \SHAR_EOF > 'morgan.five.desc' problem-set/logic.problems/morgan/morgan.five.ver1.desc created : 07/15/86 revised : 07/15/88 Natural Language Description: The files that begin with morgan.five concern problem five sent by Charles Morgan of Victoria University. The problem asks if (not(not(a)) implies a) can be deduced from the four axioms given. The axioms are as follows: 1. x => (y => x) 2. [x => (y => z)] => [(x => y) => (x => z)] 3a. (-x => -y) => (y => x) OR 3b. (x => y) => (-y => -x) 4. -(x => y) | -x | y => means "implies", and - means "not". Thus axiom 4 represents the inference rule of modus ponens. Versions: morgan.five.ver1.in- Only axiom 3 and the negation of the hypothesis are in the set of support. Axiom 3a is used as the third axiom. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER by: SLM verified for OTTER: 07/15/88 morgan.five.ver1.in- Only axiom 3 and the negation of the hypothesis are in the set of support. Axiom 3b is used as the third axiom. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER by: SLM verified for OTTER: no proof SHAR_EOF if test -f 'morgan.five.ver1.clauses' then echo shar: over-writing existing file "'morgan.five.ver1.clauses'" fi cat << \SHAR_EOF > 'morgan.five.ver1.clauses' % problem-set/logic.problems/morgan/morgan.five.ver1.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem five sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms alone that % not(not(a)) implies a? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % negation of hypothesis -P(i(n(n(a)),a)). SHAR_EOF if test -f 'morgan.five.ver1.in' then echo shar: over-writing existing file "'morgan.five.ver1.in'" fi cat << \SHAR_EOF > 'morgan.five.ver1.in' % problem-set/logic.problems/morgan/morgan.five.ver1.in % created : 07/15/86 % revised : 07/15/88 % description: % % Problem five sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms alone that % not(not(a)) implies a? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(UR_res). list(axioms). % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % negation of hypothesis -P(i(n(n(a)),a)). end_of_list. SHAR_EOF if test -f 'morgan.five.ver1.out' then echo shar: over-writing existing file "'morgan.five.ver1.out'" fi cat << \SHAR_EOF > 'morgan.five.ver1.out' problem-set/logic.problems/morgan/morgan.five.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.91, 14 June 1988. set(UR_res). list(axioms). 1 P(i(x1,i(x2,x1))). 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). 4 P(i(i(n(x1),n(x2)),i(x2,x1))). 5 -P(i(n(n(a)),a)). end_of_list. ----> UNIT CONFLICT at 16.35 sec ----> 249 (246,248) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 P(i(x1,i(x2,x1))). 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). 4 P(i(i(n(x1),n(x2)),i(x2,x1))). 5 -P(i(n(n(a)),a)). 7 (5,3,1) -P(i(i(x,i(y,x)),i(n(n(a)),a))). 17 (4,3,1) P(i(x,i(i(n(y),n(z)),i(z,y)))). 56 (7,3,2) -P(i(n(n(a)),i(i(x,n(n(a))),a))). 74 (17,3,2) P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))). 246 (74,3,56) -P(i(n(n(a)),i(n(a),n(i(x,n(n(a))))))). 248 (74,3,1) P(i(n(x),i(x,y))). 249 (246,248) . --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 5 clauses given 41 clauses generated 273 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 29 (clauses subsumed by sos) 2 unit deletions 0 clauses kept 244 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 45 ----------- times (seconds) ----------- run time 16.57 input time 0.17 binary_res time 0.00 hyper_res time 0.00 UR_res time 1.83 para_into time 0.00 para_from time 0.00 pre_process time 7.89 demod time 0.00 weigh time 0.37 for_sub time 1.61 unit_del time 0.00 post_process time 5.91 back_sub time 3.94 conflict time 1.83 factor time 0.00 FPA build time 0.64 IS build time 0.38 print_cl time 3.43 cl integrate time 1.30 window time 0.00 SHAR_EOF if test -f 'morgan.five.ver2.clauses' then echo shar: over-writing existing file "'morgan.five.ver2.clauses'" fi cat << \SHAR_EOF > 'morgan.five.ver2.clauses' % problem-set/logic.problems/morgan/morgan.five.ver2.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem five sent by Charles Morgan of Victoria University: % Using the same four axioms, with the exception that the third % is reversed, can we deduce that not(not(a)) implies a? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(y,x),i(n(x),n(y)))). (the reverse of the usual axiom 3) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % axiom 3 P(i(i(x2,x1),i(n(x1),n(x2)))). % negation of hypothesis -P(i(n(n(a)),a)). SHAR_EOF if test -f 'morgan.five.ver2.in' then echo shar: over-writing existing file "'morgan.five.ver2.in'" fi cat << \SHAR_EOF > 'morgan.five.ver2.in' % problem-set/logic.problems/morgan/morgan.five.ver2.in % created : 07/15/86 % revised : 07/15/88 % description: % % Problem five sent by Charles Morgan of Victoria University: % Using the same four axioms, with the exception that the third % is reversed, can we deduce that not(not(a)) implies a? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(y,x),i(n(x),n(y)))). (the reverse of the usual axiom 3) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(UR_res). list(axioms). % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). % axiom 3 P(i(i(x2,x1),i(n(x1),n(x2)))). % negation of hypothesis -P(i(n(n(a)),a)). end_of_list. SHAR_EOF if test -f 'morgan.five.ver2.out' then echo shar: over-writing existing file "'morgan.five.ver2.out'" fi cat << \SHAR_EOF > 'morgan.five.ver2.out' problem-set/logic.problems/morgan/morgan.five.ver2.out created : 07/15/88 revised : 07/15/88 This version has no output file, because no proof was found. SHAR_EOF if test -f 'morgan.four.desc' then echo shar: over-writing existing file "'morgan.four.desc'" fi cat << \SHAR_EOF > 'morgan.four.desc' problem-set/logic.problems/morgan/morgan.four.ver1.desc created : 07/15/86 revised : 07/15/88 Natural Language Description: The files that begin with morgan.four concern problem four sent by Charles Morgan of Victoria University. The problem asks if (a implies not(not(a))) can be deduced from the four axioms given and transitivity. The axioms are as follows: 1. x => (y => x) 2. [x => (y => z)] => [(x => y) => (x => z)] 3. (-x => -y) => (y => x) 4. -(x => y) | -x | y => means "implies", and - means "not". Thus axiom 4 represents the inference rule of modus ponens. Versions: morgan.four.ver1.in - Only axiom 1 and the negation of the hypothesis are in the set of support. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER by: SLM verified for OTTER: 07/15/88 SHAR_EOF if test -f 'morgan.four.ver1.clauses' then echo shar: over-writing existing file "'morgan.four.ver1.clauses'" fi cat << \SHAR_EOF > 'morgan.four.ver1.clauses' % problem-set/logic.problems/morgan/morgan.four.ver1.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem two sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and transitivity that % a implies not(not(a))? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % transitivity -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). % axiom 1 P(i(x1,i(x2,x1))). % negation of hypothesis -P(i(n(n(a)),a)). SHAR_EOF if test -f 'morgan.four.ver1.in' then echo shar: over-writing existing file "'morgan.four.ver1.in'" fi cat << \SHAR_EOF > 'morgan.four.ver1.in' % problem-set/logic.problems/morgan/morgan.four.ver1.in % created : 07/15/86 % revised : 07/15/88 % description: % % Problem two sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and transitivity that % a implies not(not(a))? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(UR_res). list(axioms). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % transitivity -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). end_of_list. list(sos). % axiom 1 P(i(x1,i(x2,x1))). % negation of hypothesis -P(i(n(n(a)),a)). end_of_list. SHAR_EOF if test -f 'morgan.four.ver1.out' then echo shar: over-writing existing file "'morgan.four.ver1.out'" fi cat << \SHAR_EOF > 'morgan.four.ver1.out' problem-set/logic.problems/morgan/morgan.four.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.91, 14 June 1988. set(UR_res). list(axioms). 1 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 2 P(i(i(n(x1),n(x2)),i(x2,x1))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). 4 -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). end_of_list. list(sos). 5 P(i(x1,i(x2,x1))). 6 -P(i(n(n(a)),a)). end_of_list. ----> UNIT CONFLICT at 5.93 sec ----> 114 (113,85) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 2 P(i(i(n(x1),n(x2)),i(x2,x1))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). 4 -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). 5 P(i(x1,i(x2,x1))). 6 -P(i(n(n(a)),a)). 10 (5,4,2) P(i(n(x),i(x,y))). 12 (5,3,5) P(i(x,i(y,i(z,y)))). 13 (5,3,1) P(i(i(x,y),i(x,x))). 25 (10,4,6) -P(i(i(n(a),x),a)). 38 (25,4,2) -P(i(i(x,a),a)). 85 (12,3,38) -P(i(i(x,i(y,i(z,y))),i(i(u,a),a))). 105 (13,3,12) P(i(x,x)). 113 (105,3,1) P(i(i(i(x,y),x),i(i(x,y),y))). 114 (113,85) . --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 6 clauses given 13 clauses generated 197 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 89 (clauses subsumed by sos) 32 unit deletions 0 clauses kept 108 empty clauses 1 factors generated 0 clauses back subsumed 4 clauses not processed 9 ----------- times (seconds) ----------- run time 6.17 input time 0.27 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.95 para_into time 0.00 para_from time 0.00 pre_process time 2.74 demod time 0.00 weigh time 0.06 for_sub time 0.89 unit_del time 0.00 post_process time 1.79 back_sub time 0.82 conflict time 0.82 factor time 0.00 FPA build time 0.20 IS build time 0.12 print_cl time 1.13 cl integrate time 0.32 window time 0.00 SHAR_EOF if test -f 'morgan.one.desc' then echo shar: over-writing existing file "'morgan.one.desc'" fi cat << \SHAR_EOF > 'morgan.one.desc' problem-set/logic.problems/morgan/morgan.one.ver1.desc created : 07/15/86 revised : 07/15/88 Natural Language Description: The files that begin with morgan.one concern problem one sent by Charles Morgan of Victoria University. The problem asks if transitivity can be deduced from the following axioms. The axioms are as follows: 1. x => (y => x) 2. [x => (y => z)] => [(x => y) => (x => z)] 3. (-x => -y) => (y => x) 4. -(x => y) | -x | y => means "implies", and - means "not". Thus axiom 4 represents the inference rule of modus ponens. Versions: morgan.one.ver1.in- Only the negation of transitivity is in the set of support. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER by: SLM verified for OTTER: 07/15/88 SHAR_EOF if test -f 'morgan.one.ver1.clauses' then echo shar: over-writing existing file "'morgan.one.ver1.clauses'" fi cat << \SHAR_EOF > 'morgan.one.ver1.clauses' % problem-set/logic.problems/morgan/morgan.one.ver1.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem one sent by Charles Morgan of Victoria University: % Can transitivity be deduced from the four axioms given. % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % negation of transitivity P(i(a,b)). P(i(b,c)). -P(i(a,c)). SHAR_EOF if test -f 'morgan.one.ver1.in' then echo shar: over-writing existing file "'morgan.one.ver1.in'" fi cat << \SHAR_EOF > 'morgan.one.ver1.in' % problem-set/logic.problems/morgan/morgan.one.ver1.in % created : 07/15/86 % revised : 07/15/88 % description: % % Problem one sent by Charles Morgan of Victoria University: % Can transitivity be deduced from the four axioms given. % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(UR_res). list(axioms). % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). % negation of transitivity P(i(a,b)). P(i(b,c)). -P(i(a,c)). end_of_list. SHAR_EOF if test -f 'morgan.one.ver1.out' then echo shar: over-writing existing file "'morgan.one.ver1.out'" fi cat << \SHAR_EOF > 'morgan.one.ver1.out' problem-set/logic.problems/morgan/morgan.one.ver1.out created : 07/15/86 revised : 07/15/88 OTTER version 0.9, 19 May 1988. set(UR_res). list(axioms). 1 P(i(x1,i(x2,x1))). 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 3 P(i(i(n(x1),n(x2)),i(x2,x1))). 4 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). 5 P(i(a,b)). 6 P(i(b,c)). 7 -P(i(a,c)). end_of_list. ----> UNIT CONFLICT at 1.65 sec ----> 46 (44,11) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 P(i(x1,i(x2,x1))). 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 4 -P(i(x1,x2)) | -P(x1) | P(x2). 5 P(i(a,b)). 6 P(i(b,c)). 7 -P(i(a,c)). 9 (6,4,1) P(i(x,i(b,c))). 11 (7,4,5) -P(i(i(a,b),i(a,c))). 44 (9,4,2) P(i(i(x,b),i(x,c))). 46 (44,11) . --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 7 clauses given 8 clauses generated 55 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 16 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 39 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 7 ----------- times (seconds) ----------- run time 1.82 input time 0.21 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.21 para_into time 0.00 para_from time 0.00 pre_process time 0.74 demod time 0.00 weigh time 0.05 for_sub time 0.17 unit_del time 0.00 post_process time 0.39 back_sub time 0.12 conflict time 0.25 factor time 0.00 FPA build time 0.07 IS build time 0.08 print_cl time 0.42 cl integrate time 0.08 window time 0.00 SHAR_EOF if test -f 'morgan.six.desc' then echo shar: over-writing existing file "'morgan.six.desc'" fi cat << \SHAR_EOF > 'morgan.six.desc' problem-set/logic.problems/morgan/morgan.six.ver1.desc created : 07/15/86 revised : 07/15/88 Natural Language Description: The files that begin with morgan.six concern problem six sent by Charles Morgan of Victoria University. The problem asks if ((a => b) => [(b => c) => (a => c)]) can be deduced from the three axioms given. The axioms are as follows: 1. x => (y => x) 2. [x => (y => z)] => [(x => y) => (x => z)] 4. -(x => y) | -x | y => means "implies", and - means "not". Thus axiom 4 represents the inference rule of modus ponens. Versions: morgan.six.ver1.in- Only axiom 1 and the negation of the hypothesis are in the set of support. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER: SLM verified for OTTER: no proof SHAR_EOF if test -f 'morgan.six.ver1.clauses' then echo shar: over-writing existing file "'morgan.six.ver1.clauses'" fi cat << \SHAR_EOF > 'morgan.six.ver1.clauses' % problem-set/logic.problems/morgan/morgan.six.ver1.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem six sent by Charles Morgan of Victoria University: % Can we deduce from these three axioms alone that % (a => b) => [(b => c) => (a => c)], where => means "implies"? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % axiom 1 P(i(x1,i(x2,x1))). % negation of hypothesis -P(i(i(a,b),i(i(b,c),i(a,c)))). SHAR_EOF if test -f 'morgan.six.ver1.in' then echo shar: over-writing existing file "'morgan.six.ver1.in'" fi cat << \SHAR_EOF > 'morgan.six.ver1.in' % problem-set/logic.problems/morgan/morgan % created : 07/15/86 % revised : 07/15/88 % description: % % Problem six sent by Charles Morgan of Victoria University: % Can we deduce from these three axioms alone that % (a => b) => [(b => c) => (a => c)], where => means "implies"? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(UR_res). list(axioms). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). % axiom 1 P(i(x1,i(x2,x1))). % negation of hypothesis -P(i(i(a,b),i(i(b,c),i(a,c)))). end_of_list. SHAR_EOF if test -f 'morgan.six.ver1.out' then echo shar: over-writing existing file "'morgan.six.ver1.out'" fi cat << \SHAR_EOF > 'morgan.six.ver1.out' problem-set/logic.problems/morgan/morgan.six.ver1.out created : 07/15/88 revised : 07/15/88 This version has no output file, because no proof was found. SHAR_EOF if test -f 'morgan.three.desc' then echo shar: over-writing existing file "'morgan.three.desc'" fi cat << \SHAR_EOF > 'morgan.three.desc' problem-set/logic.problems/morgan/morgan.three.ver1.desc created : 07/15/86 revised : 07/15/88 Natural Language Description: The files that begin with morgan.three concern problem three sent by Charles Morgan of Victoria University. The problem asks if (a implies not(not(a))) can be deduced from the four axioms given and the statement proven by morgan_two.ver1. The axioms are as follows: 1. x => (y => x) 2. [x => (y => z)] => [(x => y) => (x => z)] 3. (-x => -y) => (y => x) 4. -(x => y) | -x | y => means "implies", and - means "not". Thus axiom 4 represents the inference rule of modus ponens. Versions: morgan.three.ver1.in- Both the statement proven by morgan.three.ver1.in and the negation of the hypothesis are in the set of support. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER by: SLM verified for OTTER: 07/15/88 morgan.three.ver2.in- Only the statement proven by morgan.three.ver2.in is in the set of support. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER by: SLM verified for OTTER: 07/15/88 SHAR_EOF if test -f 'morgan.three.ver1.clauses' then echo shar: over-writing existing file "'morgan.three.ver1.clauses'" fi cat << \SHAR_EOF > 'morgan.three.ver1.clauses' % problem-set/logic.problems/morgan/morgan.three.ver1.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem three sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and the statement proven % by morgan_two.ver1, that a implies not(not(a)), this time with % both the negation of the hypothesis and the proven statement in % the set of support? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % negation of hypothesis -P(i(a,n(n(a)))). % statement proven by morgan_two.ver1 P(i(n(n(x1)),x1)). SHAR_EOF if test -f 'morgan.three.ver1.in' then echo shar: over-writing existing file "'morgan.three.ver1.in'" fi cat << \SHAR_EOF > 'morgan.three.ver1.in' % problem-set/logic.problems/morgan/morgan.three.ver1.in % created : 07/15/86 % revised : 07/15/88 % description: % % Problem three sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and the statement proven % by morgan_two.ver1, that a implies not(not(a)), this time with % both the negation of the hypothesis and the proven statement in % the set of support? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(hyper_res). list(axioms). % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). % negation of hypothesis -P(i(a,n(n(a)))). % statement proven by morgan_two.ver1.in P(i(n(n(x1)),x1)). end_of_list. SHAR_EOF if test -f 'morgan.three.ver1.out' then echo shar: over-writing existing file "'morgan.three.ver1.out'" fi cat << \SHAR_EOF > 'morgan.three.ver1.out' problem-set/logic.problems/morgan/morgan.three.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.91, 14 June 1988. set(hyper_res). list(axioms). 1 P(i(x1,i(x2,x1))). 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 3 P(i(i(n(x1),n(x2)),i(x2,x1))). 4 -P(i(x1,x2)) | -P(x1) | P(x2). end_of_list. list(sos). 5 -P(i(a,n(n(a)))). 6 P(i(n(n(x1)),x1)). end_of_list. ----> UNIT CONFLICT at 0.31 sec ----> 10 (7,5) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 3 P(i(i(n(x1),n(x2)),i(x2,x1))). 4 -P(i(x1,x2)) | -P(x1) | P(x2). 5 -P(i(a,n(n(a)))). 6 P(i(n(n(x1)),x1)). 7 (6,4,3) P(i(x,n(n(x)))). 10 (7,5) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 6 clauses given 2 clauses generated 4 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 0 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 4 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.48 input time 0.20 binary_res time 0.00 hyper_res time 0.03 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.05 demod time 0.00 weigh time 0.00 for_sub time 0.01 unit_del time 0.00 post_process time 0.00 back_sub time 0.00 conflict time 0.00 factor time 0.00 FPA build time 0.05 IS build time 0.01 print_cl time 0.10 cl integrate time 0.01 window time 0.00 SHAR_EOF if test -f 'morgan.three.ver2.clauses' then echo shar: over-writing existing file "'morgan.three.ver2.clauses'" fi cat << \SHAR_EOF > 'morgan.three.ver2.clauses' % problem-set/logic.problems/morgan/morgan.three.ver2.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem three sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and the statement proven % by morgan_two.ver1, that a implies not(not(a)), this time with % only the proven statement in the set of support? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % negation of hypothesis -P(i(a,n(n(a)))). % statement proven by morgan_two.ver1 P(i(n(n(x1)),x1)). SHAR_EOF if test -f 'morgan.three.ver2.in' then echo shar: over-writing existing file "'morgan.three.ver2.in'" fi cat << \SHAR_EOF > 'morgan.three.ver2.in' % problem-set/logic.problems/morgan/morgan.three.ver2.in % created : 07/15/86 % revised : 07/15/88 % description: % % Problem three sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and the statement proven % by morgan_two.ver1, that a implies not(not(a)), this time with % only the proven statement in the set of support? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(hyper_res). list(axioms). % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % negation of hypothesis -P(i(a,n(n(a)))). end_of_list. list(sos). % statement proven by morgan_two.ver1.in P(i(n(n(x1)),x1)). end_of_list. SHAR_EOF if test -f 'morgan.three.ver2.out' then echo shar: over-writing existing file "'morgan.three.ver2.out'" fi cat << \SHAR_EOF > 'morgan.three.ver2.out' problem-set/logic.problems/morgan/morgan.three.ver2.out created : 07/15/88 revised : 07/15/88 OTTER version 0.91, 14 June 1988. set(hyper_res). list(axioms). 1 P(i(x1,i(x2,x1))). 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 3 P(i(i(n(x1),n(x2)),i(x2,x1))). 4 -P(i(x1,x2)) | -P(x1) | P(x2). 5 -P(i(a,n(n(a)))). end_of_list. list(sos). 6 P(i(n(n(x1)),x1)). end_of_list. ----> UNIT CONFLICT at 0.31 sec ----> 10 (7,5) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 3 P(i(i(n(x1),n(x2)),i(x2,x1))). 4 -P(i(x1,x2)) | -P(x1) | P(x2). 5 -P(i(a,n(n(a)))). 6 P(i(n(n(x1)),x1)). 7 (6,4,3) P(i(x,n(n(x)))). 10 (7,5) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 6 clauses given 1 clauses generated 4 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 0 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 4 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.47 input time 0.24 binary_res time 0.00 hyper_res time 0.01 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.06 demod time 0.00 weigh time 0.00 for_sub time 0.00 unit_del time 0.00 post_process time 0.01 back_sub time 0.00 conflict time 0.00 factor time 0.00 FPA build time 0.05 IS build time 0.04 print_cl time 0.07 cl integrate time 0.02 window time 0.00 SHAR_EOF if test -f 'morgan.two.desc' then echo shar: over-writing existing file "'morgan.two.desc'" fi cat << \SHAR_EOF > 'morgan.two.desc' problem-set/logic.problems/morgan/morgan.two.ver1.desc created : 07/15/86 revised : 07/15/88 Natural Language Description: The files that begin with morgan.two concern problem two sent by Charles Morgan of Victoria University. The problem asks if (not(not(a)) implies a) can be deduced from the four axioms given and transitivity. The axioms are as follows: 1. x => (y => x) 2. [x => (y => z)] => [(x => y) => (x => z)] 3. (-x => -y) => (y => x) 4. -(x => y) | -x | y => means "implies", and - means "not". Thus axiom 4 represents the inference rule of modus ponens. Versions: morgan.two.ver1.in- Only axiom 1 and the negation of the hypothesis are in the set of support. Nonequality based axioms are used, UR resolution is the inference rule, and demodulators are not included. created by: E. Lusk verified for ITP: 07/15/86 translated for OTTER by: SLM verified for OTTER: 07/15/88 SHAR_EOF if test -f 'morgan.two.ver1.clauses' then echo shar: over-writing existing file "'morgan.two.ver1.clauses'" fi cat << \SHAR_EOF > 'morgan.two.ver1.clauses' % problem-set/logic.problems/morgan/morgan.two.ver1.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem two sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and transitivity that % not(not(a)) implies a? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % transitivity -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). % axiom 1 P(i(x1,i(x2,x1))). % negation of hypothesis -P(i(n(n(a)),a)). SHAR_EOF if test -f 'morgan.two.ver1.in' then echo shar: over-writing existing file "'morgan.two.ver1.in'" fi cat << \SHAR_EOF > 'morgan.two.ver1.in' % problem-set/logic.problems/morgan/morgan.two.ver1.in % created : 07/15/86 % revised : 07/15/88 % description: % % Problem two sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and transitivity that % not(not(a)) implies a? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. set(UR_res). list(axioms). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % transitivity -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). end_of_list. list(sos). % axiom 1 P(i(x1,i(x2,x1))). % negation of hypothesis -P(i(n(n(a)),a)). end_of_list. SHAR_EOF if test -f 'morgan.two.ver1.out' then echo shar: over-writing existing file "'morgan.two.ver1.out'" fi cat << \SHAR_EOF > 'morgan.two.ver1.out' problem-set/logic.problems/morgan/morgan.two.ver1.out created : 07/15/86 revised : 07/15/88 OTTER version 0.91, 14 June 1988. set(UR_res). list(axioms). 1 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 2 P(i(i(n(x1),n(x2)),i(x2,x1))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). 4 -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). end_of_list. list(sos). 5 P(i(x1,i(x2,x1))). 6 -P(i(n(n(a)),a)). end_of_list. ----> UNIT CONFLICT at 6.06 sec ----> 114 (113,85) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 2 P(i(i(n(x1),n(x2)),i(x2,x1))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). 4 -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). 5 P(i(x1,i(x2,x1))). 6 -P(i(n(n(a)),a)). 10 (5,4,2) P(i(n(x),i(x,y))). 12 (5,3,5) P(i(x,i(y,i(z,y)))). 13 (5,3,1) P(i(i(x,y),i(x,x))). 25 (10,4,6) -P(i(i(n(a),x),a)). 38 (25,4,2) -P(i(i(x,a),a)). 85 (12,3,38) -P(i(i(x,i(y,i(z,y))),i(i(u,a),a))). 105 (13,3,12) P(i(x,x)). 113 (105,3,1) P(i(i(i(x,y),x),i(i(x,y),y))). 114 (113,85) . --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 6 clauses given 13 clauses generated 197 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 89 (clauses subsumed by sos) 32 unit deletions 0 clauses kept 108 empty clauses 1 factors generated 0 clauses back subsumed 4 clauses not processed 9 ----------- times (seconds) ----------- run time 6.28 input time 0.23 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.97 para_into time 0.00 para_from time 0.00 pre_process time 3.02 demod time 0.00 weigh time 0.09 for_sub time 0.94 unit_del time 0.00 post_process time 1.67 back_sub time 0.76 conflict time 0.83 factor time 0.00 FPA build time 0.28 IS build time 0.19 print_cl time 1.11 cl integrate time 0.33 window time 0.00 SHAR_EOF # End of shell archive exit 0