Date: Sun, 18 Jun 2006 16:30:34 -0500


Hi all,

At this week's ACL2 seminar we'll have Joe Hendrix here talking about 
his work on tree automata.  The meeting is at 4 on Wednesday in ACES 
3.116 as usual.  Joe's abstract follows.

 - Sol


This talk will present a new tree automata framework called
"Propositional Tree Automata" for reasoning about sets of terms 
that are closed modulo an equational theory.  This framework has
applications in reachability analysis and originates in work on
sufficient completeness checking modulo axioms.

Propositional Tree Automata are closed under Boolean operations.
Consequentially many decision problems such as totality and
subsumption can be reduced to checking whether the language accepted
by an automaton is empty.  This emptiness problem is undecidable in
general, but for specific theories like those with associativity,
commutativity, and identity axioms, we have developed specialized
techniques for attacking the problem.  

This work borrows ideas from tree automata, machine learning, context-
free language equations, and linear Diophantine equations.  I plan to
gradually introduce tree automata and the recent extensions we are
working on, sketch our approach to the emptiness problem, and discuss
various applications if time permits.

The talk will not require previous familiarity with tree automata.
Many of the ideas are part of joint work with Jose Meseguer, Hitoshi
Ohsaki, Mahesh Viswanathan, and myself.