System
The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation), several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.
E is implemented in C and portable to most UNIX dialects and the Cygwin environment. It is available under the GNU GPL.
Read more about this topic: E Theorem Prover
Famous quotes containing the word system:
“Short of a wholesale reform of college athletics—a complete breakdown of the whole system that is now focused on money and power—the women’s programs are just as doomed as the men’s are to move further and further away from the academic mission of their colleges.... We have to decide if that’s the kind of success for women’s sports that we want.”
—Christine H. B. Grant, U.S. university athletic director. As quoted in the Chronicle of Higher Education, p. A42 (May 12, 1993)
“While the system of holding people in hostage is as old as the oldest war, a fresher note is introduced when a tyrannic state is at war with its own subjects and may hold any citizen in hostage with no law to restrain it.”
—Vladimir Nabokov (1899–1977)
“In a universe that is all gradations of matter, from gross to fine to finer, so that we end up with everything we are composed of in a lattice, a grid, a mesh, a mist, where particles or movements so small we cannot observe them are held in a strict and accurate web, that is nevertheless nonexistent to the eyes we use for ordinary living—in this system of fine and finer, where then is the substance of a thought?”
—Doris Lessing (b. 1919)