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:
“All who wish to hand down to their children that happy republican system bequeathed to them by their revolutionary fathers, must now take their stand against this consolidating, corrupting money power, and put it down, or their children will become hewers of wood and drawers of water to this aristocratic ragocracy.”
—Andrew Jackson (1767–1845)
“New York is more now than the sum of its people and buildings. It makes sense only as a mechanical intelligence, a transporter system for the daily absorbing and nightly redeploying of the human multitudes whose services it requires.”
—Peter Conrad (b. 1948)
“The individual protests against the world, but he doesn’t get beyond protest, he is just a single protester. When he wants to be more than that, he has to counter power with power, he has to oppose the system with another system.”
—Friedrich Dürrenmatt (1921–1990)