16 February 2001, Computational Logic Seminar

16 February 2001, Computational Logic Seminar
Title: Equational Binary Decision Diagrams
Speaker: Jaco van der Pol (CWI)
Location: ILLC, Plantage Muidergracht 24, Amsterdam, Room P.327
Date and Time: Februari 16, 2001, 13.30-14.30

Abstract:
How to decide boolean combinations of equalities? As an alternative to Shostak's congruence closure, we extended binary decision diagrams with equalities. Combined with Ackerman's function elimination this does the job. We describe how EQ-BDDs provide a "canonical enough", albeit not unique, representation of propositions over equalities. Then, using wishful thinking, we describe how to extend EQ-BDDs with algebraically defined functions.

For more information, see http://www.illc.uva.nl/~mdr/ACLG/Local/seminar01-1.html.