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!