Re: A new proof of the wellfoundednes of the multiset ordering

• To: Tobias.Nipkow@informatik.tu-muenchen.de
• Subject: Re: A new proof of the wellfoundednes of the multiset ordering
• From: chet@watson.ibm.com
• Date: Mon, 12 Oct 1998 14:36:27 -0400
• cc: types@cis.upenn.edu
• In-reply-to: Your message of Mon, 12 Oct 1998 16:31:40 +0200. <199810121503.LAA18794@saul.cis.upenn.edu>
• Reply-To: chet@watson.ibm.com
• Sender: chet@watson.ibm.com

Didn't Steve Simpson do a bunch of proofs of orderings like this one?
And I thought that even he referenced Diana Schmidt (though perhaps I
have the name wrong) from Heidelberg?

--chet--

    TN> Attached you find a new(?) proof of the wellfoundednes of the
    TN> multiset ordering due to Wilfried Buchholz. Salient features:
    TN> - it is completely inductive and does not involve classical
    TN> reasoning (in contrast to the proof by Dershowitz and Manna);
    TN> - it is a joy for theorem provers (it takes about 40 lines in
    TN> Isabelle/HOL).

    TN> I would be interested to hear if this proof is known in the
    TN> literature.

• Prev: A new proof of the wellfoundednes of the multiset ordering
• Next: DMTCS'99 and CATS'99 Call for Participation
• Index(es):
  • Main
  • Thread