Firstorder Proof of a Median Algebra Problem
Robert Veroff
and
William McCune
July 2005 (updated September 2006)
Introduction
This Web page contains some research notes on a problem in median algebra.
The problem was not open, but all previous proofs we know of are
higherorder, giving no clues about how to find firstorder equational
proofs. It is therefore a good challenge for equational theorem provers.
The problem came to us from
Donald Knuth,
who ran across it while working on a new volume of
The Art of Computer Programming (TAOCP).
Update: (September 2006)
Section 7.1.1 of TAOCP, Volume 4 has several pages of background
material on the theory of medians.
A prepublication version of this section ("PreFascicle 0b: Boolean Basics")
is available; see
http://wwwcsfaculty.stanford.edu/~knuth/news.html for information.
We'll focus here on the application of automated deduction methods.
The programs
Otter
and
Prover9 were used.
Median Algebras
A median algebra has one ternary operation satisfying the following axioms.
f(x,x,y) = x # label(majority).
f(x,y,z) = f(z,x,y) # label(2a).
f(x,y,z) = f(x,z,y) # label(2b).
f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity).
Notes about the axioms.
 (2a) and (2b) allow the arguments of f
to be permuted in any way (trivial).
 (2b) is dependent on the remaining three axioms, so it can be removed.
Proof:
prover9 f dependency.in > dependency.out
The remaining three are independent.
 If we permute the arguments in the associativity axiom in the right ways,
we can do without the permutativity axioms. For example, an equivalent
2basis is
f(x,x,y) = x # label(majority).
f(f(x,w,y),z,w) = f(w,x,f(w,z,y)) # label(associativity2).
We can prove this by deriving (2a) and (2b):
prover9 f 2basis.in > 2basis.out
 We shall stick with the original 4basis in the proofs below,
because it seems more natural than the shorter bases.
The Problem
The problem is to prove that median algebras (as axiomatized above)
have the following distributivity property.
f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # label(dist_long).
We note that this was first proved by M. Kolibiar
and T. Marcisova in 1974 [3],
with a roundabout (higher order) proof.
The Proofs
We first tried several searches with Prover9 and Waldmeister
[1] without success. We then turned to
the proofsketches method [6] with Otter.
Notes about our first proof.
 We ran several Otter searches with the proofsketches method.
This method builds up a (sometimes large) set of hints that is used
to guide subsequent searches.
 We observed the syntactic structure of the equations in the problem and in the searches,
and formulated a weighting strategy that prefers shallow equations to deep ones.
 We used an Otter option (lex_order_vars) that canonicalizes terms based on
variables as well as nonvariable terms.
 We used Otter's hotlist strategy, with the associativity axiom in the hot list.
This strategy emphasizes the use of clauses in the hot list.
Here is an Otter job essentially the same as the one that produced the first proof.
otter f median.in > median.out
Here is another proof, derived from the preceding one, in which all demodulation
(rewriting) steps are explicit, and the goal is derived directly.
We call this a demodfree forward proof.
(We sometimes find this kind of proof more convenient to work with.)
otter f median_df.in > median_df.out
Note that this is a proofchecking job in which the steps of the proof are
given to Otter as hints.
Our discussion of the proof focused on two points, term depth and permutability.
Term Depth
Term depth was a relatively simple and intuitive point. The goal (distlong)
is shallow, and many of the equations in the preliminary searches were deep.
We simply used Otter's weight templates to penalize deeper terms when selecting
equations for inferences. That is, given two equations of the same size,
prefer the shallower one. Neither Otter nor Prover9 had a means to
penalize deep terms in a general and convenient way, so we added a feature to do so
in Prover9.
Permutability
The second point is also intuitive but more interesting. Full permutability
of a ternary operation can be explosive when searching automatically for
proofs. This problem is similar to associativecommutative (AC) binary operations.
Our approach is to sacrifice completeness. This was done with Otter by using the ad hoc
term ordering with lex_order_vars demodulation. This gives a total
order on terms, including variables, so that rewriting with the permutability
equations essentially sorts the arguments, including variables.
This method can easily block proofs.
A similar feature (also called lex_order_vars) was added to Prover9.
Prover9 does not have ad hoc term ordering, so it was added (as an option) to
Prover9's standard orderings (i.e., KBO, LPO, RPO). It still causes
incompleteness, because the term ordering is total. In particular,
terms are rewritten to notnecessarilysmaller terms.
Although the effect is similar in many cases, we believe that Prover9's
lex_order_vars is better behaved than Otter's lex_order_vars, because
Prover9's uses the standard orderings.
This point deserves a lot of additional work, both theoretical and experimental.
Prover9's Proof
After incorporation of the depth and lex_order_vars features,
Prover9 found a proof.
prover9 f dist3.in > dist3.out
Another Distributivity Property
A shorter version of distributivity was also known to hold in median algebras.
Here it is, lined up with the long version.
f(f(x,y,z),u,w) = f(x, f(y,u,w),f(z,u,w)) # label(dist_short).
f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # label(dist_long).
Note that the proofs above contain (permuted forms of) dist_short,
for example equation 21141 near the end of the proof in dist3.out.
Here are proofs that the two forms of distributivity are
derivable from each other.
prover9 f distshortlong.in > distshortlong.out
prover9 f distlongshort.in > distlongshort.out
Further Study
After studying our original Otter proof, Knuth sent us back
a hand proof, which we in turn used for additional studies with Otter.
Click here to read more about this.
Additional Notes
 The Otter and Prover9 input languages are not quite the same.
 Prover9 proofs and Otter proofs are frequently much longer than necessary.
Acknowledgment
Thanks to Donald Knuth for bringing this problem to the attention
of the automated deduction community.
References
Note: We need to confirm that the Kolibiar reference is correct.

T. Hillenbrand et al.
Waldmeister.
(http://www.waldmeister.org)

D. Knuth.
The Art of Computer Programming.
(
http://wwwcsfaculty.stanford.edu/~knuth/taocp.html)

M. Kolibiar and T. Marcisova.
On a question of J. Hashimoto.
Mat. Casopis, 24:179185, 1974.

W. McCune.
Otter 3.0 Reference Manual and Guide.
Tech. Report ANL94/6, Argonne National Laboratory, Argonne, IL, 1994.
(
http://www.mcs.anl.gov/AR/otter/)

W. McCune.
Prover9.
(
http://www.mcs.anl.gov/~mccune/prover9/)

R. Veroff.
Solving Open Questions and Other Challenge Problems Using Proof Sketches.
J. Automated Reasoning, 27(2):157174, 2001.