Date: Tue, 19 Sep 2006 09:51:28 -0500
From: Sol Swords

Hi all,

At the meeting this week Ian Wehrman will give the talk.  As usual, 
we'll be in Aces 3.116 at 4 PM Wednesday.

Hope to see you there,
 - Sol


Ian's abstract:
I'll talk about automated equational theorem proving and term rewriting. 
The talk will focus on background material and motivation for an 
improved technique that I helped develop. We'll cover the word problem, 
the general approach to solving it with rewriting, how to prove any 
necessary properties of term rewriting systems (termination in 
particular), and a particular procedure for solving the word problem 
called Knuth-Bendix completion. Finally, I'll describe my variant of 
Knuth-Bendix completion which, in many circumstances, can solve problems 
in hard equational theories for which the standard procedure fails.

Many state-of-the-art automated equational provers are based on 
completion. The term rewriting theory behind completion is also widely 
applicable. So I hope the group will find the talk useful!