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 page http://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	Stephan Schulz <schulz@informatik.tu-muenchen.de>
Developers	Stephan Schulz <schulz@informatik.tu-muenchen.de>

Related information

Interfaces	command line, library
Programs	CLIB
Source languages	C, Awk, Shell script
Weak prerequisites	LaTeX2e

Entry information

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

Categories

Top > All Packages in Directory
Top > Science > Mathematics

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.

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.