Nonunit Problems

With the intention of spurring research focusing on paramodulation in which nonunit clauses occur, we offer the following problems.

Problem NU1, moderate. The problem asks one to prove the following identity in modular lattices in which a 0 and 1 exist, where îs meet, v is join, and is complement.

((A v B) v ((A B) B)) ((A v B) v ((A B) Â)) = (A v B)

The following clauses can be used, the first 18 of which capture the properties of a modular lattice.

EQ(meet(0,x),0).	EQ(meet(meet(x,y),z),meet(x,meet(y,z))).
EQ(meet(x,0),0).	EQ(join(join(x,y),z),join(x,join(y,z))).
EQ(join(0,x),x).	EQ(meet(x,join(x,y)),x).
EQ(join(x,0),x).	EQ(join(x,meet(x,y)),x).
EQ(meet(1,x),x).	-EQ(meet(x,z),x) | EQ(meet(z,join(x,y)),join(x,meet(y,z))).
EQ(meet(x,1),x).	EQ(x,x).
EQ(join(1,x),1).	EQ(join(r2,meet(a,b)),1).
EQ(join(x,1),1).	EQ(meet(r2,meet(a,b)),0).
EQ(meet(x,x),x).	EQ(join(r1,join(a,b)),1).
EQ(join(x,x)x).	EQ(meet(r1,join(a,b)),0).
EQ(meet(x,y),meet(y,x)).	EQ(join(r1,meet(a,r2)),b2).
EQ(join(x,y),join(y,x)).	EQ(join(r1,meet(b,r2)),a2).
	-EQ(meet(a2,b2),r1).

Problem NU2, moderate. Prove that subgroups of index 2 are normal, using the clauses given earlier to study group theory. O(x) means that x is in the subgroup, j(x,y) is an element of the subgroup that exists if x and y are not in the subgroup (for giving the definition of index 2).

O(e).	O(x) | O(y) | EQ(prod(x,j(x,y)),y).
-O(x) | O(inv(x)).	O(b).
-O(x) | -O(y) | O(prod(x,y)).	-O(prod(a,prod(b,g(a)))).
O(x) | O(y) | O(i(x,y)).

Problem NU3, hard. In set theory, prove that if two ordered pairs are equal, then they are equal componentwise. In the following clauses, op(x,y) means the ordered pair, up(x,y) means the unordered pair, IN is set membership, and sing is the singleton set consisting of x.

EQ(x,x).	-IN(x,up(y,z)) | EQ(x,y) | EQ(x,z).
IN(x,sing(x)).	EQ(op(x,y),up(sing(x),up(x,y))).
-IN(x,sing(y)) | EQ(x,y).	EQ(op(m1,r1),op(m2,r2)).
IN(x,up(x,y)).	-EQ(m1,m2) | -EQ(r1,r2).
IN(y,up(x,y)).	EQ(op(x,y),up(sing(x),up(x,y))).