File Search | Catalog | Content Search |

Home » Catalog » Debian » Other »
acl2_4.3.orig.tar.gz » Content »pkg://acl2_4.3.orig.tar.gz:15251431/acl2-sources/books/arithmetic-2/meta/ info *downloads*## README

1. Introduction See top.lisp for a summary of the theories contained in this library and how to use them. These books contain a port of some experimental arithmetic libraries to ACL2 v2-6. They are, I believe, superior to what had been shipped with ACL2 in the past; but they have not been extensively tested in this configuration. In particular, the original libraries depend upon some extensions to the linear-arithmetic decision procedure which has not yet been integrated into the main development branch of ACL2, and so there may be some unanticipated weaknesses. 2. Overview Basic Books: pre.lisp post.lisp These books contain some basic normalization and rewrite rules. expt.lisp This book contains some simple rules for manipulating expressions involving expt. Most of them should not require any attention from the user, but see the comment at the beginning of the book regarding strong-expt-rules. numerator-and-denominator.lisp A small book containing a few rules about numerator and denominator. This book does not pretend to be complete and should be expanded. Suggestions are welcome. mini-theories.lisp A very small book containing some rules which are occasionally useful, but which fit nowhere else. In particular, the rule rewrite-linear-equalities-to-iff should be kept in mind. integerp.lisp This book contains a set of rules about when a term is or is not an integer. The need for this book reveals a weakness in ACL2's type-prescription reasoning. non-linear.lisp This book contains some rules intended to mitigate the absence of the extensions to the linear-arithmetic decision procedure mentioned above. Most of these rules suffer from the free-variable problem, but are still useful. There is also a set of rules, gathered into the theory ratio-theory-of-1. they are occasionaly useful, but can cause thrashing of the linear-arithmetic decision procedure and so are disabled by default. Books with Meta Rules: The next four books provide a more complex set of rules for manipulating arithmetic expressions. Extensive use is made of the newly augmented meta rules. They are documented internally, but see the regular ACL2 documentaion on meta rules also. common-meta.lisp This book provides several functions and utilities for the next two books. collect-terms-meta.lisp This book contains some meta-rules which collect "like" terms in a sum or product. cancel-terms-meta.lisp This book contains some meta-rules which cancel "like" terms on either side of an (in)equality. integerp-meta.lisp This book of meta-rules does not depend on the other three books. We reccomend this as a first book to look at if you are interested in the design and writing of meta functions, rather than just there use. Although the meta rule defined here is more complex than the ones in collect-terms-meta.lisp, it is all in one book and does not use any macros to generate theorems or functions. Top: top.lisp This book gathers all the other books together into one easy to include package. It also contains a list (with descriptions) of the various theories and setting available to the user of these books and is therefore a useful starting point for exploration.

Results 1 - 1 of 1

© 1997-2017 FileWatcher.com