From: "Matyas Sustik A."
Subject: Wednesday talk
Date: Mon, 2 Jun 2003 15:02:51 -0500 (CDT)


This week I will talk about the proof of Dixon's lemma in ACL2.  From
the abstract of the paper submitted to the ACL2 workshop:

I present the use of the ACL2 theorem prover to formalize and
mechanically check a new proof of Dixon's lemma about monomial
sequences.  Dixon's lemma can be used to establish the termination of
the Buchberger algorithm to find the Grobner basis of a polynom ideal.
This effort is part of a larger project which aims to develop a
mechanically verified computer algebra system.

Since we had a talk about ordinals before I will only summarize the
lemmas I needed for the proof with reference to the ordinal arithmetic
book developed by Panagiotis Manolios and Daron Vroon.

The talk about the SLAM project - which was mentioned two weeks ago at
the meeting - has been postponed.

Matyas