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:
“A heresy can spring only from a system that is in full vigor.”
—Eric Hoffer (1902–1983)
“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)
“Every political system is an accumulation of habits, customs, prejudices, and principles that have survived a long process of trial and error and of ceaseless response to changing circumstances. If the system works well on the whole, it is a lucky accident—the luckiest, indeed, that can befall a society.”
—Edward C. Banfield (b. 1916)