Index of /users/moore/acl2/v3-4/distrib/acl2-sources/books/defexec/dag-unification

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[TXT] Makefile                17-Dec-2007 10:00  1.5K  
[   ] basic.lisp              17-Dec-2007 10:00   16K  
[   ] dag-unification-l.lisp  17-Dec-2007 10:00   17K  
[   ] dag-unification-rule..> 17-Dec-2007 10:00   56K  
[   ] dag-unification-st-e..> 17-Dec-2007 10:00  5.7K  
[   ] dag-unification-st.lisp 17-Dec-2007 10:00   40K  
[   ] dags.lisp               17-Dec-2007 10:00   46K  
[   ] list-unification-rul..> 17-Dec-2007 10:00   43K  
[   ] matching.lisp           17-Dec-2007 10:00   19K  
[   ] subsumption-subst.lisp  17-Dec-2007 10:00   22K  
[   ] subsumption.lisp        17-Dec-2007 10:00   16K  
[   ] terms-as-dag.lisp       17-Dec-2007 10:00  104K  
[   ] terms-dag-stobj.lisp    17-Dec-2007 10:00  5.9K  
[   ] terms.lisp              17-Dec-2007 10:00   43K  

This directory contains ACL2 books for the algorithm described in the paper
"Reconciling Efficient Execution in an Automated Reasoning Environment".  The
ACL2 2004 workshop contains a contribution with an updated and improved
version (of quadratic time complexity) of that algorithm.  You can find that
work by downloading and and extracting the workshops tarball, in directory
workshops/2004/ruiz-et-al/.