First-order Proof of a Median Algebra Problem

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 higher-order, giving no clues about how to find first-order 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 pre-publication version of this section ("Pre-Fascicle 0b: Boolean Basics") is available; see http://www-cs-faculty.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 2-basis 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 4-basis 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 round-about (higher order) proof.

The Proofs

We first tried several searches with Prover9 and Waldmeister [1] without success. We then turned to the proof-sketches method [6] with Otter.

Notes about our first proof.

We ran several Otter searches with the proof-sketches 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 hot-list 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 demod-free 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 proof-checking 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 (dist-long) 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 associative-commutative (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 not-necessarily-smaller 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 dist-3.in > dist-3.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 dist-3.out.

Here are proofs that the two forms of distributivity are derivable from each other.

prover9 -f dist-short-long.in > dist-short-long.out prover9 -f dist-long-short.in > dist-long-short.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://www-cs-faculty.stanford.edu/~knuth/taocp.html)
M. Kolibiar and T. Marcisova. On a question of J. Hashimoto. Mat. Casopis, 24:179-185, 1974.
W. McCune. Otter 3.0 Reference Manual and Guide. Tech. Report ANL-94/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):157-174, 2001.