E Equational Theorem Prover 0.7
The E equational theorem prover version 0.7 "Dhajea" has been
released.
E is a a purely equational theorem prover for clausal logic with
equality. Thus, you can specify a mathematical problem (e.g. a
mathematical puzzle), a (small) piece of program code or some hardware
elements in clausal logic (using rules of the form "If A and B and C
then D or E or F" in a PROLOG-like syntax), and try to have the system
prove certain properties of the described structure. Be warned that
this can consume inane (in fact, theoretically unlimited) amounts of
CPU time and memory for difficult problems.
E 0.7 has been carefully tested on all CNF problems of the TPTP
problem library, version 2.4.1, and showed no unexpected
behaviour. The prover can produce checkable proof objects, a simple
proof checker is included in the distribution.
Important changes are a much simplified rewrite engine, direct PCL2
support, a better automatic mode, and better memory control
features. In automatic mode, this version should behave exactly like
the prerelase version that participated in CASC-18. To achieve this,
we have refrained from including a couple of more recent
improvements. They will be included in E 0.71, due out in some weeks.
E is available as a source distribution for UNIX-variants. It installs
cleanly under all UNIX variants I could get my hands on: Various
versions of GNU/Linux for Intel and SPARC, SunOS (with tweaking),
Solaris and HPUX.
The system is distributed under the GNU General Public License.
You can find the source distribution and additional information at
http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Our servers are usually rebooted Monday mornings between 3:30 and 4:00
CET, and may be unavailable during this time.
Have fun!
Stephan
Please email me as schulz@informatik.tu-muenchen.de (Stephan Schulz)
_____________________________________________
AutoGen 5.4.1
AutoGen 5.4.1 has been released, and it is available from
ftp.gnu.org/gnu/autogen/ (and from mirrors of the GNU ftp site -
see www.gnu.org/order/ftp.html).
NEWS:
1. The AutoOpts option parsing component now generates an easily
configurable source tarball for inclusion in client projects.
Incorporated into it are autoconf macros that make this
fairly trivial:
1. Install the unrolled tarball into your package source tree
2. Add ''${tag}/Makefile'' to the list of configured files
3. Move libopts.m4 to your autoconf macro directory
4. Add ''AUTOOPTS_CHECK'' to your configure.ac file.
5. Add ''@LIBOPTS_DIR@'' to your subdirectory build list.
It will be empty if not needed, otherwise ''${tag}''.
where "${tag}" is "libopts" + the current version.
The included README is sed-ed to have the right tag.
2. In the generated version, usage, man page and texinfo docs,
autoopts will now insert the phrase,
please send bug reports to: <<supplied-eaddress>>
3. the ''xml2ag'' program will convert any arbitrary XML file
into AutoGen definitions. This makes it fairly trivial to
insert XML-ized information into arbitrary text docs without
having to write XML structure traversal code.
4. Templates have been added for constructing man pages and info
documentation for library procedures.
5. AutoGen invocation options can be embedded in its source files.
