#!/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 # SAMslemma.desc # SAMslemma.ver1.clauses # SAMslemma.ver1.in # SAMslemma.ver1.out # This archive created: Tue Aug 16 11:17:09 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/algebra/lattices/README created : 07/15/86 revised : 07/20/88 Contents of 'lattices' : ------------------------ Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/algebra/lattices. SAMslemma : the problem is to prove SAM's lemma, a lemma in modular lattice theory. ---------------------------------------------------------------------- For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, as well as complete details on each formulation and each version. probname.ver# : 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#, without any strategy; note that comments always are on lines beginning with a % and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver# through 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# [ > 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 'SAMslemma.desc' then echo shar: over-writing existing file "'SAMslemma.desc'" fi cat << \SHAR_EOF > 'SAMslemma.desc' problem-set/algebra/lattices/SAMslemma.desc created : 07/09/86 revised : 07/11/88 Natural Language Description: NOTE : The clauses are described in the form of Algebraic formulae, where: "v" stands for union "^" stands for intersection "'" stands for complement Sam's Lemma may be stated as follows: Let L be a modular lattice with 0 and 1. Suppose that A and B are elements of L such that (A v B) and (A ^ B) both have not necessarily unique complements. Then, one can prove ((A v B)' v ((A ^ B)' ^ B)) ^ ((A v B)' v ((A ^ B)' ^ A)) = (A v B)' Axioms to define Sams Lemma Union of 1 and x is equal to 1 : (1 v X) = 1 Union of x with itself is equal to x : (X v X) = X Union of 0 and x is equal to x : (0 v X) = X Intersection of 0 and x is equal to 0 : (0 ^ X) = 0 Intersection of x and itself is equal to x : (X ^ X) = X Intersection of 1 and x is equal to itself : (1 ^ X) = X Intersection of x and y , is the same as intersection of y and x. (X ^ Y) = (Y ^ X) Union of x and y is the same as union of y and x. (X v Y) = (Y v X) Union of x with the intersection of x and y is the same as x. X v (X ^ Y) = X Intersection of x with the union of x and y is the same as x. X ^ (X v Y) = X The operation '^', intersection ,is associative X ^ (Y ^ Z) = (X ^ Y) ^ Z The operation 'v' is associative X v (Y v Z) = (X v Y) v Z (X ^ Z) = X implies that (Z ^ (X v Y)) = (X v (Y ^ Z)) (X ^ Z) = Z implies that (X ^ (Y v Z)) = (Z v (X ^ Y)) Negation of Sams Lemma The following can be obtained by using the fact that if x v y = 1 and x ^ y = 0 then x = y' a intersection b is equal to c : a ^ b = c The union of d and c is equal to 1 : d v c = c1 b union d is equal to e : b v d = e a union e is equal to 0 : a v e = c0 b union a2 is equal to b2 : b v a2 = b2 a union b2 is equal to c1 : (a v b2) = c1 a union b is equal to c2 : (a v b) = c2 a2 intersection c2 is equal to c0 : a2 ^ c2 = c0 d intersection a is equal to d2 : (d ^ a) = d2 a2 union d2 is equal to e2 : (a2 v d2) = e2 b intersection d is equal to a3 : (b ^ d) = a3 a2 union a3 is equal to b3 : (a2 v a3) = b3 the intersection of b3 and e2 is not equal to a2 : (b3 ^ e2) <> a2 Versions: SAMslemma.ver1.in: a clause formulation using hyperresolution with the p-formulation of the problem. created by : E. Lusk. verified for ITP : 07/15/86. translated for OTTER by : caw. verified for OTTER : 07/01/88. SHAR_EOF if test -f 'SAMslemma.ver1.clauses' then echo shar: over-writing existing file "'SAMslemma.ver1.clauses'" fi cat << \SHAR_EOF > 'SAMslemma.ver1.clauses' % problem-set/algebra/lattices/SAMslemma.ver1.clauses % created : 07/09/86 % revised : 07/08/88 % description: % % Sam's Lemma may be stated as follows: % % Let L be a modular lattice with 0 and 1. Suppose that % A and B are elements of L such that (A v B) and (A ^ B) % both have not necessarily unique complements. % % Then, one can prove % % ((A v B)' v ((A ^ B)' ^ B)) ^ % ((A v B)' v ((A ^ B)' ^ A)) = (A v B)' % representation: % % declare_predicates(3,[MAX,MIN]). % declare_constants([a,a2,a3,b,b2,b3,c,c2,c3,d,e,d2,e2,a3,b3,c1,c0]). % declare_variables([x,y,z,x1,y1,z1,xy,yz,xyz]). % % Meanings of predicates and functions used in the following clauses : % MAX(x,y,z) : means z as the union of x and y % MIN(x,y,z) : means z as the intersection of x and y % c0 : is the constant used to represent the number '0' % c1 : is the constant used to represent the number '1' % Union of 1 and x is equal to 1 : (1 v X) = 1 MAX(c1,x,c1). % Union of x with itself is equal to x : (X v X) = X MAX(x,x,x). % Union of 0 and x is equal to x : (0 v X) = X MAX(c0,x,x). % Intersection of 0 and x is equal to 0 : (0 ^ X) = 0 MIN(c0,x,c0). % Intersection of x and itself is equal to x : (X ^ X) = X MIN(x,x,x). % Intersection of 1 and x is equal to itself : (1 ^ X) = X MIN(c1,x,x). % Intersection of x and y , is the same as intersection of y and x. % % (X ^ Y) = (Y ^ X) -MIN(x,y,z) | MIN(y,x,z). % Union of x and y is the same as union of y and x. (X v Y) = (Y v X) -MAX(x,y,z) | MAX(y,x,z). % Union of x with the intersection of x and y is the same as x. % X v (X ^ Y) = X -MIN(x,y,z) | MAX(x,z,x). % Intersection of x with the union of x and y is the same as x. % X ^ (X v Y) = X -MAX(x,y,z) | MIN(x,z,x). % The operation '^', intersection ,is associative X ^ (Y ^ Z) = (X ^ Y) ^ Z -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz). -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz). % The operation 'v' is associative X v (Y v Z) = (X v Y) v Z -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(x,yz,xyz) | MAX(xy,z,xyz). -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(xy,z,xyz) | MAX(x,yz,xyz). % (X ^ Z) = X implies that (Z ^ (X v Y)) = (X v (Y ^ Z)) -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1). -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1). % (X ^ Z) = Z implies that (X ^ (Y v Z)) = (Z v (X ^ Y)) -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1). -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MAX(z,x1,z1) | MIN(x,y1,z1). % Negation of Sams Lemma : % The following can be obtained by using the fact that % if x v y = 1 and x ^ y = 0 then x = y' % a intersection b is equal to c : a ^ b = c MIN(a,b,c). % The union of d and c is equal to 1 : d v c = c1 MAX(d,c,c1). % b union d is equal to e : b v d = e MIN(b,d,e). % a union e is equal to 0 : a v e = c0 MIN(a,e,c0). % b union a2 is equal to b2 : b v a2 = b2 MAX(b,a2,b2). % a union b2 is equal to c1 : (a v b2) = c1 MAX(a,b2,c1). % a union b is equal to c2 : (a v b) = c2 MAX(a,b,c2). % a2 intersection c2 is equal to c0 : a2 ^ c2 = c0 MIN(a2,c2,c0). % d intersection a is equal to d2 : (d ^ a) = d2 MIN(d,a,d2). % a2 union d2 is equal to e2 : (a2 v d2) = e2 MAX(a2,d2,e2). % b intersection d is equal to a3 : (b ^ d) = a3 MIN(d,b,a3). % a2 union a3 is equal to b3 : (a2 v a3) = b3 MAX(a2,a3,b3). % the intersection of b3 and e2 is not equal to a2 : (b3 ^ e2) <> a2 -MIN(b3,e2,a2). SHAR_EOF if test -f 'SAMslemma.ver1.in' then echo shar: over-writing existing file "'SAMslemma.ver1.in'" fi cat << \SHAR_EOF > 'SAMslemma.ver1.in' % problem-set/algebra/lattices/SAMslemma.ver1.in % created : 07/09/86 % revised : 07/08/88 % description: % % Sam's Lemma may be stated as follows: % % Let L be a modular lattice with 0 and 1. Suppose that % A and B are elements of L such that (A v B) and (A ^ B) % both have not necessarily unique complements. % % Then, one can prove % % ((A v B)' v ((A ^ B)' ^ B)) ^ % ((A v B)' v ((A ^ B)' ^ A)) = (A v B)' % representation: % % declare_predicates(3,[MAX,MIN]). % declare_constants([a,a2,a3,b,b2,b3,c,c2,c3,d,e,d2,e2,a3,b3,c1,c0]). % declare_variables([x,y,z,x1,y1,z1,xy,yz,xyz]). % % Meanings of predicates and functions used in the following clauses : % MAX(x,y,z) : means z as the union of x and y % MIN(x,y,z) : means z as the intersection of x and y % c0 : is the constant used to represent the number '0' % c1 : is the constant used to represent the number '1' set(hyper_res). clear(back_sub). list(axioms). % Union of 1 and x is equal to 1 : (1 v X) = 1 MAX(c1,x,c1). % Union of x with itself is equal to x : (X v X) = X MAX(x,x,x). % Union of 0 and x is equal to x : (0 v X) = X MAX(c0,x,x). % Intersection of 0 and x is equal to 0 : (0 ^ X) = 0 MIN(c0,x,c0). % Intersection of x and itself is equal to x : (X ^ X) = X MIN(x,x,x). % Intersection of 1 and x is equal to itself : (1 ^ X) = X MIN(c1,x,x). % Intersection of x and y , is the same as intersection of y and x. % % (X ^ Y) = (Y ^ X) -MIN(x,y,z) | MIN(y,x,z). % Union of x and y is the same as union of y and x. (X v Y) = (Y v X) -MAX(x,y,z) | MAX(y,x,z). % Union of x with the intersection of x and y is the same as x. % X v (X ^ Y) = X -MIN(x,y,z) | MAX(x,z,x). % Intersection of x with the union of x and y is the same as x. % X ^ (X v Y) = X -MAX(x,y,z) | MIN(x,z,x). % The operation '^', intersection ,is associative X ^ (Y ^ Z) = (X ^ Y) ^ Z -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz). -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz). % The operation 'v' is associative X v (Y v Z) = (X v Y) v Z -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(x,yz,xyz) | MAX(xy,z,xyz). -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(xy,z,xyz) | MAX(x,yz,xyz). % (X ^ Z) = X implies that (Z ^ (X v Y)) = (X v (Y ^ Z)) -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1). -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1). % (X ^ Z) = Z implies that (X ^ (Y v Z)) = (Z v (X ^ Y)) -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1). -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MAX(z,x1,z1) | MIN(x,y1,z1). end_of_list. list(sos). % Negation of Sams Lemma : % The following can be obtained by using the fact that % if x v y = 1 and x ^ y = 0 then x = y' % a intersection b is equal to c : a ^ b = c MIN(a,b,c). % The union of d and c is equal to 1 : d v c = c1 MAX(d,c,c1). % b union d is equal to e : b v d = e MIN(b,d,e). % a union e is equal to 0 : a v e = c0 MIN(a,e,c0). % b union a2 is equal to b2 : b v a2 = b2 MAX(b,a2,b2). % a union b2 is equal to c1 : (a v b2) = c1 MAX(a,b2,c1). % a union b is equal to c2 : (a v b) = c2 MAX(a,b,c2). % a2 intersection c2 is equal to c0 : a2 ^ c2 = c0 MIN(a2,c2,c0). % d intersection a is equal to d2 : (d ^ a) = d2 MIN(d,a,d2). % a2 union d2 is equal to e2 : (a2 v d2) = e2 MAX(a2,d2,e2). % b intersection d is equal to a3 : (b ^ d) = a3 MIN(d,b,a3). % a2 union a3 is equal to b3 : (a2 v a3) = b3 MAX(a2,a3,b3). % the intersection of b3 and e2 is not equal to a2 : (b3 ^ e2) <> a2 -MIN(b3,e2,a2). end_of_list. SHAR_EOF if test -f 'SAMslemma.ver1.out' then echo shar: over-writing existing file "'SAMslemma.ver1.out'" fi cat << \SHAR_EOF > 'SAMslemma.ver1.out' % problem-set/lattices/SAMslemma.ver1.out % created : 07/09/86 % revised : 07/08/88 OTTER release 0.9, 19 May 1988 set(hyper_res). clear(back_sub). list(axioms). 1 MAX(c1,x,c1). 2 MAX(x,x,x). 3 MAX(c0,x,x). 4 MIN(c0,x,c0). 5 MIN(x,x,x). 6 MIN(c1,x,x). 7 -MIN(x,y,z) | MIN(y,x,z). 8 -MAX(x,y,z) | MAX(y,x,z). 9 -MIN(x,y,z) | MAX(x,z,x). 10 -MAX(x,y,z) | MIN(x,z,x). 11 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz). 12 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz). 13 -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(x,yz,xyz) | MAX(xy,z,xyz). 14 -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(xy,z,xyz) | MAX(x,yz,xyz). 15 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1). 16 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1). 17 -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1). 18 -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MAX(z,x1,z1) | MIN(x,y1,z1). end_of_list. list(sos). 19 MIN(a,b,c). 20 MAX(d,c,c1). 21 MIN(b,d,e). 22 MIN(a,e,c0). 23 MAX(b,a2,b2). 24 MAX(a,b2,c1). 25 MAX(a,b,c2). 26 MIN(a2,c2,c0). 27 MIN(d,a,d2). 28 MAX(a2,d2,e2). 29 MIN(d,b,a3). 30 MAX(a2,a3,b3). 31 -MIN(b3,e2,a2). end_of_list. ---------------- PROOF ---------------- 3 MAX(c0,x,x). 4 MIN(c0,x,c0). 5 MIN(x,x,x). 6 MIN(c1,x,x). 9 -MIN(x,y,z) | MAX(x,z,x). 10 -MAX(x,y,z) | MIN(x,z,x). 11 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz). 12 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz). 15 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1). 16 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1). 17 -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1). 21 MIN(b,d,e). 22 MIN(a,e,c0). 25 MAX(a,b,c2). 26 MIN(a2,c2,c0). 27 MIN(d,a,d2). 28 MAX(a2,d2,e2). 29 MIN(d,b,a3). 30 MAX(a2,a3,b3). 31 -MIN(b3,e2,a2). 39 (21,16,4,3,3) MIN(d,b,e). 54 (25,17,6,6,6) MAX(b,a,c2). 58 (25,10) MIN(a,c2,a). 61 (26,9) MAX(a2,c0,a2). 62 (27,16,4,3,3) MIN(a,d,d2). 72 (29,15,4,3,21) MAX(c0,a3,e). 76 (30,17,6,6,6) MAX(a3,a2,b3). 79 (30,10) MIN(a2,b3,a2). 89 (39,12,5,29) MIN(d,a3,e). 90 (39,12,6,29) MIN(c1,e,a3). 94 (39,11,5,29) MIN(e,b,a3). 133 (54,10) MIN(b,c2,b). 140 (58,11,27,27) MIN(d2,c2,d2). 196 (89,11,62,22) MIN(d2,a3,c0). 197 (90,17,6,72,6) MAX(a3,c0,a3). 224 (133,11,94,94) MIN(a3,c2,a3). 279 (224,16,76,26,197) MIN(c2,b3,a3). 307 (279,11,140,196) MIN(d2,b3,c0). 330 (307,16,79,28,61) MIN(b3,e2,a2). 331 (330,31) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). 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(back_sub). 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 31 clauses given 289 clauses generated 20182 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 19882 (clauses subsumed by sos) 2575 unit deletions 0 clauses kept 300 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 223.49 input time 0.41 binary_res time 0.00 hyper_res time 172.37 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 45.10 demod time 0.00 weigh time 0.06 for_sub time 36.20 unit_del time 0.00 post_process time 1.28 back_sub time 0.00 conflict time 1.22 factor time 0.00 FPA build time 0.40 IS build time 0.13 print_cl time 1.62 cl integrate time 0.15 window time 0.00 SHAR_EOF # End of shell archive exit 0