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:
“The truth is, the whole administration under Roosevelt was demoralized by the system of dealing directly with subordinates. It was obviated in the State Department and the War Department under [Secretary of State Elihu] Root and me [Taft was the Secretary of War], because we simply ignored the interference and went on as we chose.... The subordinates gained nothing by his assumption of authority, but it was not so in the other departments.”
—William Howard Taft (1857–1930)
“The human body is not a thing or substance, given, but a continuous creation. The human body is an energy system ... which is never a complete structure; never static; is in perpetual inner self-construction and self-destruction; we destroy in order to make it new.”
—Norman O. Brown (b. 1913)
“We now come to the grand law of the system in which we are placed, as it has been developed by the experience of our race, and that, in one word, is SACRIFICE!”
—Catherine E. Beecher (1800–1878)