Date: Tue, 13 Feb 2007 09:27:05 -0600 (CST)
From: "Erik H. Reeber"
Subject: This week in ACL2

Hello Everyone,

    After the usual roundtable, this Wednesday I will be talking about my 
work with the Subclass of Unrollable List Formulas in ACL2 (SUFLA). 
SULFA is a decidable subclass of ACL2 formulas which includes the ACL2 
primitives if, car, cdr, cons, and consp, as well as a definitional 
principle.

    I have spoken about SULFA before at the ACL2 meeting a few years ago, 
as well as last year at the ACL2 workshop and at IJCAR.  In this meeting, 
however, I will give a more detailed explanation of my current translation 
algorithm from SULFA to the conjunctive normal form required as the input 
to SAT solvers.  Also, I will discuss how I added equality and 
uninterpreted functions and how I think the algorithm can be improved.

-Erik