Top > Science > Mathematics > E

E - Automated theorem prover

E is an equational theorem prover. You give it a mathematical specification (in clausal logic with equality) and a hypothesis; it will then try to find a proof for the hypothesis (and sometimes succeed).

E is build on top of (and by now inseparable from) CLIB, a collection of library functions for building programs the follow the basic input-processing-output paradigm, with additional support for most levels of first-order logic. The code has been used to build a couple of other applications by now.

CLIB is layered, with higher layers becoming more specialized. Lower levels take care of the scientifically uninteresting, but necessary services for production-quality efficient programs, e.g. error handling, memory management, parsing of input, etc. They should be useful for most programs. Higher level modules implement shared and unshared terms, equations, clauses and related stuff.

Obtaining

Web pagehttp://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Source tarball http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_0.81/E.tgz
Source information http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html#downloading
Version 0.81 (beta) released on 2004-01-16
Licensed under The GNU General Public License, Version 2.
This is not a GNU package.

Documentation

User guide in LaTeX format included; User guide in PostScript format available from http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.ps; User guide in PDF format available from http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.pdf; User README available in HTML format from http://www4.informatik.tu-muenchen.de/~schulz/WORK/E_DOWNLOAD/V_0.81/README
Support contacts


Project contacts

Maintainers
Developers

Related information

Interfacescommand line, library
ProgramsCLIB
Source languagesC, Awk, Shell script
Weak prerequisitesLaTeX2e

Entry information

License verified byJanet Casey <jcasey@gnu.org> on 2001-01-31
Entry compiled byJanet Casey <jcasey@gnu.org>

Categories



The copyright licensing notice below applies to this text. The software described in this text has its own copyright notice and license, which can usually be found in the distribution itself.

Copyright © 2000, 2001, 2002, 2003, 2004 Free Software Foundation, Inc.

Permission is granted to copy, distribute, and/or modify this document under the terms of the GNU Free Documentation License, Version 1.1 or any later version published by the Free Software Foundation; with no Invariant Sections, with no Front-Cover Texts, and with no Back-Cover Texts. A copy of this license is included in the file COPYING.DOC.

Please report any problems in this page to bug-directory@gnu.org, or find out how you can help fix them.

The FSF provides this directory as a service to the free software community. Please consider donating to the FSF to help support this project.