Index of /users/moore/acl2/books/books/defexec/dag-unification

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[TXT] Makefile                20-Jan-2006 08:45  1.5K  
[   ] basic.lisp              20-Jan-2006 08:44   16K  
[   ] dag-unification-l.lisp  11-Dec-2005 13:51   17K  
[   ] dag-unification-rule..> 12-Dec-2005 04:58   56K  
[   ] dag-unification-st-e..> 12-Dec-2005 05:38  5.7K  
[   ] dag-unification-st.lisp 12-Dec-2005 05:25   40K  
[   ] dags.lisp               07-Dec-2005 15:29   46K  
[   ] list-unification-rul..> 07-Dec-2005 15:19   43K  
[   ] matching.lisp           07-Dec-2005 14:56   19K  
[   ] subsumption-subst.lisp  25-May-2003 14:28   22K  
[   ] subsumption.lisp        07-Dec-2005 14:59   16K  
[   ] terms-as-dag.lisp       11-Dec-2005 13:47  104K  
[   ] terms-dag-stobj.lisp    22-Jan-2003 11:36  5.9K  
[   ] terms.lisp              07-Dec-2005 15:17   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/.