Download here - Informatik - FB3 - Uni Bremen

affect the applicability of rules.
•
The system state can be affected by setting various modes. Two examples include
a program mode, which allows the user to write programs that need not terminate
but can be used in macros, and a backchain limit for rewriting.
•
Session management commands include undoing, redoing, and querying the state.
•
Proof assistance is provided by two break/trace utilities for the rewriter; an
interactive goal manager; and a report mechanism that can show “expensive”
rules.
•
The programming interface provides features to bridge the gap between the user
and the computing engine, such as Lisp-independent trace and backtrace utilities and verifiable alternative function bodies. This interface also makes available powerful Lisp features including packages and macros. State and other
single-threaded objects are supported efficiently with an applicative semantics.
A guard mechanism provides a powerful, though less automatic, alternative to
types that is separate from the logical content of definitions.
•
Users can interactively extend the system’s capabilities by providing books of
logical definitions and theorems, as well as system utilities and even (through
trust tags) system modifications.
•
A clause-processor mechanism provides an interface through which the user connects ACL2 with another tool.
A separate question, not addressed in this talk, is how to communicate proof
results effectively to non-users. Our focus is on interface support for effective usage.
2