(Web Support)

May 2021

This page provides Web support for *A Wos Challenge Met*
[2]. In particular, it includes the
Prover9 [1] files used
to work toward a solution to the challenge.

x * rs(x,y) = y # label("right solvable"). rs(x, x * y) = y # label("right solution is unique"). ls(x,y) * y = x # label("left solvable"). ls(x * y, y) = x # label("left solution is unique"). 1 * x = x # label("left identity"). x * 1 = x # label("right identity").and the following 4 Moufang identities.

(x * y) * (z * x) = (x * (y * z)) * x # label("M1"). ((x * y) * z) * y = x * (y * (z * y)) # label("M2"). x * (y * (x * z)) = ((x * y) * x) * z # label("M3"). x * ((y * z) * x) = (x * y) * (z * x) # label("M4").Quoting from the newsletter ...

Your challenge (in effect, four challenges) consists in finding four proofs. You might begin by seeking a proof that, from the basic axioms with the Moufang 1 adjoined, you can deduce Moufang 2, with no constraint. Let that be your first challenge.For the next three challenges, find proofs of Moufang 3 from Moufang 2, Moufang 4 from Moufang 3, and Moufang 1 from Moufang 4, each proof with no constraint.

Then, for the more exciting set of challenges that are consistent with the questions that were open, find the given circle of proofs, but find pure proofs. In other words, the proof of the second from the first must avoid the use of Moufang 3 and Moufang 4 to be pure.

Depending on the program you use -- I had in mind that you would be using an automated reasoning program to meet the challenges -- the last line of each proof might be the so-called flip of the goal. In other words, rather than proving s = t, your program proves t = s. If such is the case, the further challenge -- and not trivial according to my research -- is to prove the various Moufang items as given.

If you have used a Knuth-Bendix approach, the final set of challenges asks for proofs that are free of demodulation and that are forward, rather than backward or bidirectional. If you succeed in finding the four proofs for the circle of pure proofs, you will discover, I feel rather sure, that their lengths differ sharply.

- M1 => M2
- M2 => M3
- M3 => M4
- M4 => M1

- Find an unconstrained proof that labels any of the undesired clauses that appear for easy identifcation.
- If not already pure, find a pure proof using the unconstrained proof as hints to help guide the search.
- Find a strictly-forward, demodulation-free (sfdf) proof using the pure proof as hints.
- If the derived goal is not equality ordered as specified in the challenge, use a syntactic trick to derive it in the desired order.

After each successful run of Prover9, we extract the resulting proof,

prooftrans -f file.out > file.pf

and hints for use in later runs.

prooftrans expand hints -f file.out > file.hints

prover9 -f 1to2a.in > 1to2a.out

M4 (actually, its flip) appears in the proof (clause 29).

Pure:

prover9 -f 1to2b.in 1to2a.hints > 1to2b.out

SFDF:

prover9 -f 1to2c.in 1to2b.hints > 1to2c.out

M2 is derived and is equality ordered as specified in the problem statement, which completes M1 => M2.

prover9 -f 2to3a.in > 2to3a.out

M4 (actually, its flip) appears in the proof (clause 20118).

Pure:

prover9 -f 2to3b.in 2to3a.hints > 2to3b.out

SFDF:

prover9 -f 2to3c.in 2to3b.hints > 2to3c.out

M3 is derived, but it is not equality ordered as specified in the problem statement. We resort to a bit of syntactic trickery to meet the challenge.

Ordered:

prover9 -f 2to3d.in 2to3c.hints > 2to3d.outThis completes M2 => M3.

For this case, it was helpful to include the additional directiveset(para_from_small).prover9 -f 3to4a.in > 3to4a.out

M1 appears in the proof (clause 22005).

Pure:

prover9 -f 3to4b.in 3to4a.hints > 3to4b.out

SFDF:

prover9 -f 3to4c.in 3to4b.hints > 3to4c.out

M4 is derived, but it is not equality ordered as specified in the problem statement.

Ordered:

prover9 -f 3to4d.in 3to4c.hints > 3to4d.outThis completes M3 => M4.

prover9 -f 4to1a.in > 4to1a.out

The resulting proof already is pure.

SFDF:

prover9 -f 4to1c.in 4to1b.hints > 4to1c.out

M1 is derived, but it is not equality ordered as specified in the problem statement.

Ordered:

prover9 -f 4to1d.in 4to1c.hints > 4to1d.outThis completes M4 => M1.

- W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
- R. Veroff. A Wos Challenge Met. In preparation.

Last Modified: April 5, 2021 by veroff@cs.unm.edu