E

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.

 2007–2009 Alexey Beshenov.
Contact: al@cadadr.org.