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:
“Some rough political choices lie ahead. Should affirmative action be retained? Should preference be given to people on the basis of income rather than race? Should the system be—and can it be—scrapped altogether?”
—David K. Shipler (b. 1942)
“A religion so cheerless, a philosophy so sorrowful, could never have succeeded with the masses of mankind if presented only as a system of metaphysics. Buddhism owed its success to its catholic spirit and its beautiful morality.”
—W. Winwood Reade (1838–1875)
“Never expect any recognition here—the system prohibits it. The cross is not affixed to the genius, no, the genius is affixed to the cross.”
—Franz Grillparzer (1791–1872)