|
AProVE Help System |
|
Information about the AProVE system is divided into the following main sections.
-
The AProVE system offers four different user interfaces, namely a graphical user interface,
a command line interface, a web interface, and
an applet version.
-
This section describes all the functional,
imperative, logic,
and rewriting languages accepted as inputs to the AProVE system.
-
AProVE offers a wide choice of techniques for proving and transforming
term rewrite systems, context-sensitive rewriting,
and logic programs. The main technique is the dependency pair technique
and there are many techniques working on strongly connected components of the dependency graph.
-
The AProVE system can output generated proofs in different formats (HTML, LaTeX, plain text).
These proof scripts can be used to reconstruct the proof.