» Content »pkg://acl2_4.3.orig.tar.gz:15251431
/ info downloads
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.
These books contain some basic normalization and rewrite rules.
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
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.
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.
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
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.
This book provides several functions and utilities for the next
This book contains some meta-rules which collect "like" terms
in a sum or product.
This book contains some meta-rules which cancel "like" terms
on either side of an (in)equality.
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.
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 1Search over 15 billion files
© 1997-2017 FileWatcher.com