Subject: This week in ACL2
Date: Mon, 09 Jun 2003 10:46:42 -0500
From: Robert Bellarmine Krug


Greetings,

This week I, Robert, will talk about some of my work with
ACL2 and arithmetic.  This talk will be divided into two
parts --- 1. New changes to ACL2, and 2. My arithmetic-4
library.

In part 1, I will describe modifications to ACL2 which
allow linear arithmetic to use the conclusions of forward-
chaining rules.  I will also describe changes which allow
type reasoning to (weakly) use linear arithmetic.  I will
also present motivational examples for both these changes.

In part 2., I will introduce my arithetic-4 library which
I have recently gotten permision to distribue.  This will
be an introductory talk, and will probably be followed by
a more comprehensive talk in a couple of weeks.

Robert